# Documentation

Mathlib.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.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} [] (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).

Instances For
@[reducible]
def Quiver.Star.mk {U : Type u_1} [] {u : U} {v : U} (f : u v) :

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

Instances For
@[reducible]
def Quiver.Costar {U : Type u_1} [] (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).

Instances For
@[reducible]
def Quiver.Costar.mk {U : Type u_1} [] {u : U} {v : U} (f : u v) :

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

Instances For
@[simp]
theorem Prefunctor.star_snd {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
∀ (a : ), ().snd = φ.map a.snd
@[simp]
theorem Prefunctor.star_fst {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
∀ (a : ), ().fst = φ.obj a.fst
def Prefunctor.star {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
Quiver.Star (φ.obj u)

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

Instances For
@[simp]
theorem Prefunctor.costar_fst {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
∀ (a : ), ().fst = φ.obj a.fst
@[simp]
theorem Prefunctor.costar_snd {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
∀ (a : ), ().snd = φ.map a.snd
def Prefunctor.costar {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
Quiver.Costar (φ.obj u)

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

Instances For
@[simp]
theorem Prefunctor.star_apply {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) {u : U} {v : U} (e : u v) :
= Quiver.Star.mk (φ.map e)
@[simp]
theorem Prefunctor.costar_apply {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) {u : U} {v : U} (e : u v) :
= Quiver.Costar.mk (φ.map e)
theorem Prefunctor.star_comp {U : Type u_1} [] {V : Type u_3} [] (φ : U ⥤q V) {W : Type u_2} [] (ψ : V ⥤q W) (u : U) :
Prefunctor.star (φ ⋙q ψ) u = Prefunctor.star ψ (φ.obj u)
theorem Prefunctor.costar_comp {U : Type u_1} [] {V : Type u_3} [] (φ : U ⥤q V) {W : Type u_2} [] (ψ : V ⥤q W) (u : U) :
Prefunctor.costar (φ ⋙q ψ) u = Prefunctor.costar ψ (φ.obj u)
structure Prefunctor.IsCovering {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) :
• star_bijective : ∀ (u : U),
• costar_bijective : ∀ (u : U),

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

Instances For
@[simp]
theorem Prefunctor.IsCovering.map_injective {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (hφ : ) {u : U} {v : U} :
Function.Injective fun f => φ.map f
theorem Prefunctor.IsCovering.comp {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) {W : Type u_3} [] (ψ : V ⥤q W) (hφ : ) (hψ : ) :
theorem Prefunctor.IsCovering.of_comp_right {U : Type u_3} [] {V : Type u_1} [] (φ : U ⥤q V) {W : Type u_2} [] (ψ : V ⥤q W) (hψ : ) (hφψ : Prefunctor.IsCovering (φ ⋙q ψ)) :
theorem Prefunctor.IsCovering.of_comp_left {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) {W : Type u_3} [] (ψ : V ⥤q W) (hφ : ) (hφψ : Prefunctor.IsCovering (φ ⋙q ψ)) (φsur : Function.Surjective φ.obj) :
def Quiver.symmetrifyStar {U : Type u_1} [] (u : U) :
Quiver.Star (Quiver.Symmetrify.of.obj 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.

Instances For
def Quiver.symmetrifyCostar {U : Type u_1} [] (u : U) :
Quiver.Costar (Quiver.Symmetrify.of.obj 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.

Instances For
theorem Prefunctor.symmetrifyStar {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
= (Quiver.symmetrifyStar (φ.obj u)).symm Sum.map () ()
theorem Prefunctor.symmetrifyCostar {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
= (Quiver.symmetrifyCostar (φ.obj u)).symm Sum.map () ()
theorem Prefunctor.IsCovering.symmetrify {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (hφ : ) :
@[reducible]
def Quiver.PathStar {U : Type u_1} [] (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.

Instances For
@[reducible]
def Quiver.PathStar.mk {U : Type u_1} [] {u : U} {v : U} (p : ) :

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

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

A prefunctor induces a map of path stars.

Instances For
@[simp]
theorem Prefunctor.pathStar_apply {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) {u : U} {v : U} (p : ) :
theorem Prefunctor.pathStar_injective {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (hφ : ∀ (u : U), ) (u : U) :
theorem Prefunctor.pathStar_surjective {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (hφ : ∀ (u : U), ) (u : U) :
theorem Prefunctor.pathStar_bijective {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (hφ : ∀ (u : U), ) (u : U) :
theorem Prefunctor.IsCovering.pathStar_bijective {U : Type u_1} [] {V : Type u_2} [] {φ : U ⥤q V} (hφ : ) (u : U) :
@[simp]
theorem Quiver.starEquivCostar_apply_snd {U : Type u_1} [] (u : U) (e : ) :
(↑() e).snd = Quiver.reverse e.snd
@[simp]
theorem Quiver.starEquivCostar_symm_apply_snd {U : Type u_1} [] (u : U) (e : ) :
(().symm e).snd = Quiver.reverse e.snd
@[simp]
theorem Quiver.starEquivCostar_symm_apply_fst {U : Type u_1} [] (u : U) (e : ) :
(().symm e).fst = e.fst
@[simp]
theorem Quiver.starEquivCostar_apply_fst {U : Type u_1} [] (u : U) (e : ) :
(↑() e).fst = e.fst
def Quiver.starEquivCostar {U : Type u_1} [] (u : U) :

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

Instances For
@[simp]
theorem Quiver.starEquivCostar_apply {U : Type u_1} [] {u : U} {v : U} (e : u v) :
@[simp]
theorem Quiver.starEquivCostar_symm_apply {U : Type u_1} [] {u : U} {v : U} (e : u v) :
().symm () =
theorem Prefunctor.costar_conj_star {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
= ↑(Quiver.starEquivCostar (φ.obj u)) ().symm
theorem Prefunctor.bijective_costar_iff_bijective_star {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (u : U) :
theorem Prefunctor.isCovering_of_bijective_star {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (h : ∀ (u : U), ) :
theorem Prefunctor.isCovering_of_bijective_costar {U : Type u_1} [] {V : Type u_2} [] (φ : U ⥤q V) (h : ∀ (u : U), ) :