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

source

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

source

@[protected, reducible]

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

quiver.star u

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

Equations

quiver.star.mk f = ⟨v, f⟩

source

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

source

@[protected, reducible]

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

quiver.costar v

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

Equations

quiver.costar.mk f = ⟨u, f⟩

source

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

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 u), quiver.star.mk (φ.map F.snd)

source

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

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 u), quiver.costar.mk (φ.map F.snd)

source

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

source

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

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_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

source

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

source

structure prefunctor.is_covering {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) :

Prop

star_bijective : ∀ (u : U), function.bijective (φ.star u)
costar_bijective : ∀ (u : U), function.bijective (φ.costar u)

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

source

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

source

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

(φ ⋙q ψ).is_covering

source

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

φ.is_covering

source

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

ψ.is_covering

source

def quiver.symmetrify_star {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.symmetrify_star u = equiv.sigma_sum_distrib (λ (v : quiver.symmetrify U), quiver.symmetrify.of.obj u ⟶ v) (λ (v : quiver.symmetrify U), v ⟶ quiver.symmetrify.of.obj u)

source

def quiver.symmetrify_costar {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.symmetrify_costar u = equiv.sigma_sum_distrib (λ (u_1 : quiver.symmetrify U), u_1 ⟶ quiver.symmetrify.of.obj u) (λ (u_1 : quiver.symmetrify U), quiver.symmetrify.of.obj u ⟶ u_1)

source

theorem prefunctor.symmetrify_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :

φ.symmetrify.star u = ⇑((quiver.symmetrify_star (φ.obj u)).symm) ∘ sum.map (φ.star u) (φ.costar u) ∘ ⇑(quiver.symmetrify_star u)

source

@[protected]

theorem prefunctor.symmetrify_costar {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (u : U) :

φ.symmetrify.costar u = ⇑((quiver.symmetrify_costar (φ.obj u)).symm) ∘ sum.map (φ.costar u) (φ.star u) ∘ ⇑(quiver.symmetrify_costar u)

source

@[protected]

theorem prefunctor.is_covering.symmetrify {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) (hφ : φ.is_covering) :

φ.symmetrify.is_covering

source

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

quiver.path_star u = Σ (v : U), quiver.path u v

source

@[protected, reducible]

def quiver.path_star.mk {U : Type u_1} [quiver U] {u v : U} (p : quiver.path u v) :

quiver.path_star u

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

Equations

quiver.path_star.mk p = ⟨v, p⟩

source

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

quiver.path_star u → quiver.path_star (φ.obj u)

A prefunctor induces a map of path stars.

Equations

φ.path_star u = λ (p : quiver.path_star u), quiver.path_star.mk (φ.map_path p.snd)

source

@[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 : quiver.path u v) :

φ.path_star u (quiver.path_star.mk p) = quiver.path_star.mk (φ.map_path p)

source

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

function.injective (φ.path_star u)

source

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

function.surjective (φ.path_star u)

source

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

function.bijective (φ.path_star u)

source

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

function.bijective (φ.path_star u)

source

@[simp]

theorem quiver.star_equiv_costar_symm_apply_fst {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] (u : U) (e : quiver.costar u) :

(⇑((quiver.star_equiv_costar u).symm) e).fst = e.fst

source

@[simp]

theorem quiver.star_equiv_costar_symm_apply_snd {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] (u : U) (e : quiver.costar u) :

(⇑((quiver.star_equiv_costar u).symm) e).snd = quiver.reverse e.snd

source

def quiver.star_equiv_costar {U : Type u_1} [quiver U] [quiver.has_involutive_reverse 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

quiver.star_equiv_costar u = {to_fun := λ (e : quiver.star u), ⟨e.fst, quiver.reverse e.snd⟩, inv_fun := λ (e : quiver.costar u), ⟨e.fst, quiver.reverse e.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem quiver.star_equiv_costar_apply_snd {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] (u : U) (e : quiver.star u) :

(⇑(quiver.star_equiv_costar u) e).snd = quiver.reverse e.snd

source

@[simp]

theorem quiver.star_equiv_costar_apply_fst {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] (u : U) (e : quiver.star u) :

(⇑(quiver.star_equiv_costar u) e).fst = e.fst

source

@[simp]

theorem quiver.star_equiv_costar_apply {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] {u v : U} (e : u ⟶ v) :

⇑(quiver.star_equiv_costar u) (quiver.star.mk e) = quiver.costar.mk (quiver.reverse e)

source

@[simp]

theorem quiver.star_equiv_costar_symm_apply {U : Type u_1} [quiver U] [quiver.has_involutive_reverse U] {u v : U} (e : u ⟶ v) :

⇑((quiver.star_equiv_costar v).symm) (quiver.costar.mk e) = quiver.star.mk (quiver.reverse e)

source

theorem prefunctor.costar_conj_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [quiver.has_involutive_reverse U] [quiver.has_involutive_reverse V] [φ.map_reverse] (u : U) :

φ.costar u = ⇑(quiver.star_equiv_costar (φ.obj u)) ∘ φ.star u ∘ ⇑((quiver.star_equiv_costar 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.has_involutive_reverse U] [quiver.has_involutive_reverse V] [φ.map_reverse] (u : U) :

function.bijective (φ.costar u) ↔ function.bijective (φ.star u)

source

theorem prefunctor.is_covering_of_bijective_star {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [quiver.has_involutive_reverse U] [quiver.has_involutive_reverse V] [φ.map_reverse] (h : ∀ (u : U), function.bijective (φ.star u)) :

φ.is_covering

source

theorem prefunctor.is_covering_of_bijective_costar {U : Type u_1} [quiver U] {V : Type u_2} [quiver V] (φ : U ⥤q V) [quiver.has_involutive_reverse U] [quiver.has_involutive_reverse V] [φ.map_reverse] (h : ∀ (u : U), function.bijective (φ.costar u)) :

φ.is_covering