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

source

@[reducible, inline]

abbrev 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))

source

@[reducible, inline]

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

Star u

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

Equations

Quiver.Star.mk f = ⟨v, f⟩

source

@[reducible, inline]

abbrev 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))

source

@[reducible, inline]

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

Costar v

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

Equations

Quiver.Costar.mk f = ⟨u, f⟩

source

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

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

source

@[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) :

(φ.star u a✝).fst = φ.obj a✝.fst

source

@[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) :

(φ.star u a✝).snd = φ.map a✝.snd

source

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

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

source

@[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) :

(φ.costar u a✝).fst = φ.obj a✝.fst

source

@[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) :

(φ.costar u a✝).snd = φ.map a✝.snd

source

@[simp]

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

φ.star u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e)

source

@[simp]

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

φ.costar v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e)

source

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) :

(φ ⋙q ψ).star u = ψ.star (φ.obj u) ∘ φ.star u

source

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) :

(φ ⋙q ψ).costar u = ψ.costar (φ.obj u) ∘ φ.costar u

source

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 (φ.star u)
costar_bijective (u : U) : Function.Bijective (φ.costar u)

source

@[simp]

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

Function.Injective fun (f : u ⟶ v) => φ.map f

source

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φ : φ.IsCovering) (hψ : ψ.IsCovering) :

(φ ⋙q ψ).IsCovering

source

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ψ : ψ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) :

φ.IsCovering

source

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φ : φ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) (φsur : Function.Surjective φ.obj) :

ψ.IsCovering

source

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

Star (Symmetrify.of.obj u) ≃ Star u ⊕ 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 (Quiver.Hom (Quiver.Symmetrify.of.obj u)) fun (v : Quiver.Symmetrify U) => v ⟶ Quiver.Symmetrify.of.obj u

source

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

Costar (Symmetrify.of.obj u) ≃ Costar u ⊕ 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) (Quiver.Hom (Quiver.Symmetrify.of.obj u))

source

theorem Prefunctor.symmetrifyStar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :

φ.symmetrify.star u = ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

source

theorem Prefunctor.symmetrifyCostar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :

φ.symmetrify.costar u = ⇑(Quiver.symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(Quiver.symmetrifyCostar u)

source

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

φ.symmetrify.IsCovering

source

@[reducible, inline]

abbrev 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)

source

@[reducible, inline]

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

PathStar u

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

Equations

Quiver.PathStar.mk p = ⟨v, p⟩

source

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

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

source

@[simp]

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

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

source

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

Function.Injective (φ.pathStar u)

source

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

Function.Surjective (φ.pathStar u)

source

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

Function.Bijective (φ.pathStar u)

source

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

Function.Bijective (φ.pathStar u)

source

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

Star u ≃ 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.

source

@[simp]

theorem Quiver.starEquivCostar_symm_apply_snd {U : Type u_1} [Quiver U] [HasInvolutiveReverse U] (u : U) (e : Costar u) :

((starEquivCostar u).symm e).snd = reverse e.snd

source

@[simp]

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

((starEquivCostar u) e).fst = e.fst

source

@[simp]

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

((starEquivCostar u).symm e).fst = e.fst

source

@[simp]

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

((starEquivCostar u) e).snd = reverse e.snd

source

@[simp]

theorem Quiver.starEquivCostar_apply {U : Type u_1} [Quiver U] [HasInvolutiveReverse U] {u v : U} (e : u ⟶ v) :

(starEquivCostar u) (Star.mk e) = Costar.mk (reverse e)

source

@[simp]

theorem Quiver.starEquivCostar_symm_apply {U : Type u_1} [Quiver U] [HasInvolutiveReverse U] {u v : U} (e : u ⟶ v) :

(starEquivCostar v).symm (Costar.mk e) = Star.mk (reverse e)

source

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] [φ.MapReverse] (u : U) :

φ.costar u = ⇑(Quiver.starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(Quiver.starEquivCostar u).symm

source

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] [φ.MapReverse] (u : U) :

Function.Bijective (φ.costar u) ↔ Function.Bijective (φ.star u)

source

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] [φ.MapReverse] (h : ∀ (u : U), Function.Bijective (φ.star u)) :

φ.IsCovering

source

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] [φ.MapReverse] (h : ∀ (u : U), Function.Bijective (φ.costar u)) :

φ.IsCovering

Documentation

Mathlib.Combinatorics.Quiver.Covering

Covering #

Main definitions #

Main statements #

TODO #

Tags #