# mathlib3documentation

combinatorics.quiver.covering

# 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.is_covering φ means that φ.star u and φ.costar u are bijections for all u;
• quiver.star_path u is the type of all paths with source u;
• prefunctor.star_path u is the obvious function star_path u → star_path (φ.obj u).

## Main statements #

• prefunctor.is_covering.path_star_bijective states that if φ is a covering, then φ.star_path 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
@[protected, reducible]
def quiver.star.mk {U : Type u_1} [quiver U] {u v : U} (f : u v) :

Constructor for quiver.star. Defined to be sigma.mk.

Equations
@[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
@[protected, reducible]
def quiver.costar.mk {U : Type u_1} [quiver U] {u v : U} (f : u v) :

Constructor for quiver.costar. Defined to be sigma.mk.

Equations
@[simp]
theorem prefunctor.star_fst {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) (ᾰ : quiver.star u) :
(φ.star u ᾰ).fst = φ.obj ᾰ.fst
def prefunctor.star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :

A prefunctor induces a map of quiver.star at every vertex.

Equations
@[simp]
theorem prefunctor.star_snd {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) (ᾰ : quiver.star u) :
(φ.star u ᾰ).snd = φ.map ᾰ.snd
def prefunctor.costar {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :

A prefunctor induces a map of quiver.costar at every vertex.

Equations
@[simp]
theorem prefunctor.costar_snd {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) (ᾰ : quiver.costar u) :
(φ.costar u ᾰ).snd = φ.map ᾰ.snd
@[simp]
theorem prefunctor.costar_fst {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) (ᾰ : quiver.costar u) :
(φ.costar u ᾰ).fst = φ.obj ᾰ.fst
@[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 (φ.map e)
@[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) :
theorem prefunctor.star_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) (u : U) :
⋙q ψ).star u = ψ.star (φ.obj u) φ.star u
theorem prefunctor.costar_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) (u : U) :
⋙q ψ).costar u = ψ.costar (φ.obj u) φ.costar u
structure prefunctor.is_covering {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.

@[simp]
theorem prefunctor.is_covering.map_injective {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (hφ : φ.is_covering) {u v : U} :
function.injective (λ (f : u v), φ.map f)
theorem prefunctor.is_covering.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φ : φ.is_covering) (hψ : ψ.is_covering) :
theorem prefunctor.is_covering.of_comp_right {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ψ : ψ.is_covering) (hφψ : ⋙q ψ).is_covering) :
theorem prefunctor.is_covering.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φ : φ.is_covering) (hφψ : ⋙q ψ).is_covering) (φsur : function.surjective φ.obj) :
def quiver.symmetrify_star {U : Type u_1} [quiver U] (u : 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
def quiver.symmetrify_costar {U : Type u_1} [quiver U] (u : 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
theorem prefunctor.symmetrify_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :
@[protected]
theorem prefunctor.symmetrify_costar {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :
@[protected]
theorem prefunctor.is_covering.symmetrify {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (hφ : φ.is_covering) :
@[reducible]
def quiver.path_star {U : Type u_1} [quiver U] (u : U) :
Type (max u_1 u)

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

Equations
@[protected, reducible]
def quiver.path_star.mk {U : Type u_1} [quiver U] {u v : U} (p : v) :

Constructor for quiver.path_star. Defined to be sigma.mk.

Equations
def prefunctor.path_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :

A prefunctor induces a map of path stars.

Equations
@[simp]
theorem prefunctor.path_star_apply {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) {u v : U} (p : v) :
φ.path_star u =
theorem prefunctor.path_star_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) :
theorem prefunctor.path_star_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) :
theorem prefunctor.path_star_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) :
@[protected]
theorem prefunctor.is_covering.path_star_bijective {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] {φ : U ⥤q V} (hφ : φ.is_covering) (u : U) :
@[simp]
theorem quiver.star_equiv_costar_symm_apply_fst {U : Type u_1} [quiver U] (u : U) (e : quiver.costar u) :
(.symm) e).fst = e.fst
@[simp]
theorem quiver.star_equiv_costar_symm_apply_snd {U : Type u_1} [quiver U] (u : U) (e : quiver.costar u) :
(.symm) e).snd =
def quiver.star_equiv_costar {U : Type u_1} [quiver U] (u : U) :

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

Equations
@[simp]
theorem quiver.star_equiv_costar_apply_snd {U : Type u_1} [quiver U] (u : U) (e : quiver.star u) :
e).snd =
@[simp]
theorem quiver.star_equiv_costar_apply_fst {U : Type u_1} [quiver U] (u : U) (e : quiver.star u) :
e).fst = e.fst
@[simp]
theorem quiver.star_equiv_costar_apply {U : Type u_1} [quiver U] {u v : U} (e : u v) :
@[simp]
theorem quiver.star_equiv_costar_symm_apply {U : Type u_1} [quiver U] {u v : U} (e : u v) :
theorem prefunctor.costar_conj_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [φ.map_reverse] (u : U) :
theorem prefunctor.bijective_costar_iff_bijective_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [φ.map_reverse] (u : U) :
theorem prefunctor.is_covering_of_bijective_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [φ.map_reverse] (h : (u : U), function.bijective (φ.star u)) :
theorem prefunctor.is_covering_of_bijective_costar {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [φ.map_reverse] (h : (u : U), function.bijective (φ.costar u)) :