Covering

This file defines coverings of quivers as prefunctors that are bijective on the so-called stars and costars at each vertex of the domain.

Main definitions

• Quiver.Star u is the type of all arrows with source u;
• Quiver.Costar u is the type of all arrows with target u;
• Prefunctor.star φ u is the obvious function star u → star (φ.obj u);
• Prefunctor.costar φ u is the obvious function costar u → costar (φ.obj u);
• Prefunctor.IsCovering φ means that φ.star u and φ.costar u are bijections for all u;
• Quiver.PathStar u is the type of all paths with source u;
• Prefunctor.pathStar u is the obvious function PathStar u → PathStar (φ.obj u).

Main statements

• Prefunctor.IsCovering.pathStar_bijective states that if φ is a covering, then φ.pathStar u is a bijection for all u. In other words, every path in the codomain of φ lifts uniquely to its domain.

TODO

Clean up the namespaces by renaming Prefunctor to Quiver.Prefunctor.

Tags

Cover, covering, quiver, path, lift

@[reducible]

def Quiver.Star {U : Type u_1} [Quiver U] (u : U) : Type (max u_1 u)

The Quiver.Star at a vertex is the collection of arrows whose source is the vertex. The type Quiver.Star u is defined to be Σ (v : U), (u ⟶ v).

Equations

• Quiver.Star u = ((v : U) × (u ⟶ v))

@[reducible]

def Quiver.Star.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (f : u ⟶ v) : Quiver.Star u

Constructor for Quiver.Star. Defined to be Sigma.mk.

Equations

• Quiver.Star.mk f = { fst := v, snd := f }

@[reducible]

def Quiver.Costar {U : Type u_1} [Quiver U] (v : U) : Type (max u_1 u)

The Quiver.Costar at a vertex is the collection of arrows whose target is the vertex. The type Quiver.Costar v is defined to be Σ (u : U), (u ⟶ v).

Equations

• Quiver.Costar v = ((u : U) × (u ⟶ v))

@[reducible]

def Quiver.Costar.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (f : u ⟶ v) : Quiver.Costar v

Constructor for Quiver.Costar. Defined to be Sigma.mk.

Equations

• Quiver.Costar.mk f = { fst := u, snd := f }

@[simp]

theorem Prefunctor.star_snd {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : ∀ (a : Quiver.Star u), (Prefunctor.star φ u a).snd = φ.map a.snd

@[simp]

theorem Prefunctor.star_fst {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : ∀ (a : Quiver.Star u), (Prefunctor.star φ u a).fst = φ.obj a.fst

def Prefunctor.star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : Quiver.Star u → Quiver.Star (φ.obj u)

A prefunctor induces a map of Quiver.Star at every vertex.

Equations

• Prefunctor.star φ u F = Quiver.Star.mk (φ.map F.snd)

@[simp]

theorem Prefunctor.costar_snd {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : ∀ (a : Quiver.Costar u), (Prefunctor.costar φ u a).snd = φ.map a.snd

@[simp]

theorem Prefunctor.costar_fst {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : ∀ (a : Quiver.Costar u), (Prefunctor.costar φ u a).fst = φ.obj a.fst

def Prefunctor.costar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : Quiver.Costar u → Quiver.Costar (φ.obj u)

A prefunctor induces a map of Quiver.Costar at every vertex.

Equations

• Prefunctor.costar φ u F = Quiver.Costar.mk (φ.map F.snd)

@[simp]

theorem Prefunctor.star_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (e : u ⟶ v) : Prefunctor.star φ u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e)

@[simp]

theorem Prefunctor.costar_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (e : u ⟶ v) : Prefunctor.costar φ v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e)

theorem Prefunctor.star_comp {U : Type u_1} [Quiver U] {V : Type u_3} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (u : U) : Prefunctor.star (φ ⋙q ψ) u = Prefunctor.star ψ (φ.obj u) ∘ Prefunctor.star φ u

theorem Prefunctor.costar_comp {U : Type u_1} [Quiver U] {V : Type u_3} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (u : U) : Prefunctor.costar (φ ⋙q ψ) u = Prefunctor.costar ψ (φ.obj u) ∘ Prefunctor.costar φ u

structure Prefunctor.IsCovering {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) : Prop

A prefunctor is a covering of quivers if it defines bijections on all stars and costars.

• star_bijective : ∀ (u : U), Function.Bijective (Prefunctor.star φ u)
• costar_bijective : ∀ (u : U), Function.Bijective (Prefunctor.costar φ u)

@[simp]

theorem Prefunctor.IsCovering.map_injective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : Prefunctor.IsCovering φ) {u : U} {v : U} : Function.Injective fun (f : u ⟶ v) => φ.map f

theorem Prefunctor.IsCovering.comp {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {W : Type u_3} [Quiver W] (ψ : V ⥤q W) (hφ : Prefunctor.IsCovering φ) (hψ : Prefunctor.IsCovering ψ) : Prefunctor.IsCovering (φ ⋙q ψ)

theorem Prefunctor.IsCovering.of_comp_right {U : Type u_3} [Quiver U] {V : Type u_1} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (hψ : Prefunctor.IsCovering ψ) (hφψ : Prefunctor.IsCovering (φ ⋙q ψ)) : Prefunctor.IsCovering φ

theorem Prefunctor.IsCovering.of_comp_left {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {W : Type u_3} [Quiver W] (ψ : V ⥤q W) (hφ : Prefunctor.IsCovering φ) (hφψ : Prefunctor.IsCovering (φ ⋙q ψ)) (φsur : Function.Surjective φ.obj) : Prefunctor.IsCovering ψ

def Quiver.symmetrifyStar {U : Type u_1} [Quiver U] (u : U) : Quiver.Star (Quiver.Symmetrify.of.obj u) ≃ Quiver.Star u ⊕ Quiver.Costar u

The star of the symmetrification of a quiver at a vertex u is equivalent to the sum of the star and the costar at u in the original quiver.

Equations

• Quiver.symmetrifyStar u = Equiv.sigmaSumDistrib (fun (v : Quiver.Symmetrify U) => Quiver.Symmetrify.of.obj u ⟶ v) fun (v : Quiver.Symmetrify U) => v ⟶ Quiver.Symmetrify.of.obj u

def Quiver.symmetrifyCostar {U : Type u_1} [Quiver U] (u : U) : Quiver.Costar (Quiver.Symmetrify.of.obj u) ≃ Quiver.Costar u ⊕ Quiver.Star u

The costar of the symmetrification of a quiver at a vertex u is equivalent to the sum of the costar and the star at u in the original quiver.

Equations

• Quiver.symmetrifyCostar u = Equiv.sigmaSumDistrib (fun (u_1 : Quiver.Symmetrify U) => u_1 ⟶ Quiver.Symmetrify.of.obj u) fun (u_1 : Quiver.Symmetrify U) => Quiver.Symmetrify.of.obj u ⟶ u_1

theorem Prefunctor.symmetrifyStar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : Prefunctor.star (Prefunctor.symmetrify φ) u = ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (Prefunctor.star φ u) (Prefunctor.costar φ u) ∘ ⇑(Quiver.symmetrifyStar u)

theorem Prefunctor.symmetrifyCostar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : Prefunctor.costar (Prefunctor.symmetrify φ) u = ⇑(Quiver.symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (Prefunctor.costar φ u) (Prefunctor.star φ u) ∘ ⇑(Quiver.symmetrifyCostar u)

theorem Prefunctor.IsCovering.symmetrify {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : Prefunctor.IsCovering φ) : Prefunctor.IsCovering (Prefunctor.symmetrify φ)

@[reducible]

def Quiver.PathStar {U : Type u_1} [Quiver U] (u : U) : Type (max u_1 u u_1)

The path star at a vertex u is the type of all paths starting at u. The type Quiver.PathStar u is defined to be Σ v : U, Path u v.

Equations

• Quiver.PathStar u = ((v : U) × Quiver.Path u v)

@[reducible]

def Quiver.PathStar.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (p : Quiver.Path u v) : Quiver.PathStar u

Constructor for Quiver.PathStar. Defined to be Sigma.mk.

Equations

• Quiver.PathStar.mk p = { fst := v, snd := p }

def Prefunctor.pathStar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) : Quiver.PathStar u → Quiver.PathStar (φ.obj u)

A prefunctor induces a map of path stars.

Equations

• Prefunctor.pathStar φ u p = Quiver.PathStar.mk (Prefunctor.mapPath φ p.snd)

@[simp]

theorem Prefunctor.pathStar_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (p : Quiver.Path u v) : Prefunctor.pathStar φ u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (Prefunctor.mapPath φ p)

theorem Prefunctor.pathStar_injective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Injective (Prefunctor.star φ u)) (u : U) : Function.Injective (Prefunctor.pathStar φ u)

theorem Prefunctor.pathStar_surjective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Surjective (Prefunctor.star φ u)) (u : U) : Function.Surjective (Prefunctor.pathStar φ u)

theorem Prefunctor.pathStar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Bijective (Prefunctor.star φ u)) (u : U) : Function.Bijective (Prefunctor.pathStar φ u)

theorem Prefunctor.IsCovering.pathStar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {φ : U ⥤q V} (hφ : Prefunctor.IsCovering φ) (u : U) : Function.Bijective (Prefunctor.pathStar φ u)

@[simp]

theorem Quiver.starEquivCostar_apply_snd {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Star u) : ((Quiver.starEquivCostar u) e).snd = Quiver.reverse e.snd

@[simp]

theorem Quiver.starEquivCostar_symm_apply_snd {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Costar u) : ((Quiver.starEquivCostar u).symm e).snd = Quiver.reverse e.snd

@[simp]

theorem Quiver.starEquivCostar_symm_apply_fst {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Costar u) : ((Quiver.starEquivCostar u).symm e).fst = e.fst

@[simp]

theorem Quiver.starEquivCostar_apply_fst {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Star u) : ((Quiver.starEquivCostar u) e).fst = e.fst

def Quiver.starEquivCostar {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] (u : U) : Quiver.Star u ≃ Quiver.Costar u

In a quiver with involutive inverses, the star and costar at every vertex are equivalent. This map is induced by Quiver.reverse.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quiver.starEquivCostar_apply {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] {u : U} {v : U} (e : u ⟶ v) : (Quiver.starEquivCostar u) (Quiver.Star.mk e) = Quiver.Costar.mk (Quiver.reverse e)

@[simp]

theorem Quiver.starEquivCostar_symm_apply {U : Type u_1} [Quiver U] [Quiver.HasInvolutiveReverse U] {u : U} {v : U} (e : u ⟶ v) : (Quiver.starEquivCostar v).symm (Quiver.Costar.mk e) = Quiver.Star.mk (Quiver.reverse e)

theorem Prefunctor.costar_conj_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [Prefunctor.MapReverse φ] (u : U) : Prefunctor.costar φ u = ⇑(Quiver.starEquivCostar (φ.obj u)) ∘ Prefunctor.star φ u ∘ ⇑(Quiver.starEquivCostar u).symm

theorem Prefunctor.bijective_costar_iff_bijective_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [Prefunctor.MapReverse φ] (u : U) : Function.Bijective (Prefunctor.costar φ u) ↔ Function.Bijective (Prefunctor.star φ u)

theorem Prefunctor.isCovering_of_bijective_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [Prefunctor.MapReverse φ] (h : ∀ (u : U), Function.Bijective (Prefunctor.star φ u)) : Prefunctor.IsCovering φ

theorem Prefunctor.isCovering_of_bijective_costar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [Prefunctor.MapReverse φ] (h : ∀ (u : U), Function.Bijective (Prefunctor.costar φ u)) : Prefunctor.IsCovering φ