# mathlib3documentation

combinatorics.quiver.symmetric

## Symmetric quivers and arrow reversal #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains constructions related to symmetric quivers:

• symmetrify V adds formal inverses to each arrow of V.
• has_reverse is the class of quivers where each arrow has an assigned formal inverse.
• has_involutive_reverse extends has_reverse by requiring that the reverse of the reverse is equal to the original arrow.
• prefunctor.preserve_reverse is the class of prefunctors mapping reverses to reverses.
• symmetrify.of, symmetrify.lift, and the associated lemmas witness the universal property of symmetrify.
@[nolint]
def quiver.symmetrify (V : Type u_1) :
Type u_1

A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow). NB: this does not work for Prop-valued quivers. It requires [quiver.{v+1} V].

Equations
Instances for quiver.symmetrify
@[protected, instance]
def quiver.symmetrify_quiver (V : Type u) [quiver V] :
Equations
@[class]
structure quiver.has_reverse (V : Type u_2) [quiver V] :
Type (max u_2 v)

A quiver has_reverse if we can reverse an arrow p from a to b to get an arrow p.reverse from b to a.

Instances of this typeclass
Instances of other typeclasses for quiver.has_reverse
• quiver.has_reverse.has_sizeof_inst
def quiver.reverse {V : Type u_1} [quiver V] {a b : V} :
(a b) (b a)

Reverse the direction of an arrow.

Equations
@[class]
structure quiver.has_involutive_reverse (V : Type u_2) [quiver V] :
Type (max u_2 v)
• to_has_reverse :
• inv' : {a b : V} (f : a b),

A quiver has_involutive_reverse if reversing twice is the identity.

Instances of this typeclass
Instances of other typeclasses for quiver.has_involutive_reverse
• quiver.has_involutive_reverse.has_sizeof_inst
@[simp]
theorem quiver.reverse_reverse {V : Type u_2} [quiver V] {a b : V} (f : a b) :
@[simp]
theorem quiver.reverse_inj {V : Type u_2} [quiver V] {a b : V} (f g : a b) :
f = g
theorem quiver.eq_reverse_iff {V : Type u_2} [quiver V] {a b : V} (f : a b) (g : b a) :
@[class]
structure prefunctor.map_reverse {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) :

A prefunctor preserving reversal of arrows

Instances of this typeclass
Instances of other typeclasses for prefunctor.map_reverse
• prefunctor.map_reverse.has_sizeof_inst
@[simp]
theorem prefunctor.map_reverse' {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) [φ.map_reverse] {u v : U} (e : u v) :
@[protected, instance]
def prefunctor.map_reverse_comp {U : Type u_1} {V : Type u_2} {W : Type u_3} [quiver U] [quiver V] [quiver W] (φ : U ⥤q V) (ψ : V ⥤q W) [φ.map_reverse] [ψ.map_reverse] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem quiver.symmetrify_reverse {V : Type u_2} [quiver V] {a b : quiver.symmetrify V} (e : a b) :
@[reducible]
def quiver.hom.to_pos {V : Type u_2} [quiver V] {X Y : V} (f : X Y) :
X Y

Shorthand for the "forward" arrow corresponding to f in symmetrify V

@[reducible]
def quiver.hom.to_neg {V : Type u_2} [quiver V] {X Y : V} (f : X Y) :
Y X

Shorthand for the "backward" arrow corresponding to f in symmetrify V

@[simp]
def quiver.path.reverse {V : Type u_2} [quiver V] {a b : V} :
b a

Reverse the direction of a path.

Equations
@[simp]
theorem quiver.path.reverse_to_path {V : Type u_2} [quiver V] {a b : V} (f : a b) :
@[simp]
theorem quiver.path.reverse_comp {V : Type u_2} [quiver V] {a b c : V} (p : b) (q : c) :
@[simp]
theorem quiver.path.reverse_reverse {V : Type u_2} [quiver V] {a b : V} (p : b) :
@[simp]
theorem quiver.symmetrify.of_map {V : Type u_2} [quiver V] (X Y : V) (f : X Y) :
def quiver.symmetrify.of {V : Type u_2} [quiver V] :

The inclusion of a quiver in its symmetrification

Equations
@[simp]
theorem quiver.symmetrify.of_obj {V : Type u_2} [quiver V] (a : V) :
def quiver.symmetrify.lift {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] (φ : V ⥤q V') :

Given a quiver V' with reversible arrows, a prefunctor to V' can be lifted to one from symmetrify V to V'

Equations
theorem quiver.symmetrify.lift_spec {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] (φ : V ⥤q V') :
theorem quiver.symmetrify.lift_reverse {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] (φ : V ⥤q V') {X Y : quiver.symmetrify V} (f : X Y) :
=
theorem quiver.symmetrify.lift_unique {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] (φ : V ⥤q V') (Φ : ⥤q V') (hΦ : = φ) [hΦrev : Φ.map_reverse] :

lift φ is the only prefunctor extending φ and preserving reverses.

@[simp]
theorem prefunctor.symmetrify_map {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) (X Y : quiver.symmetrify U) (ᾰ : (X Y) (Y X)) :
φ.symmetrify.map = φ.map
@[simp]
theorem prefunctor.symmetrify_obj {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) (ᾰ : U) :
φ.symmetrify.obj = φ.obj
def prefunctor.symmetrify {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) :

A prefunctor canonically defines a prefunctor of the symmetrifications.

Equations
Instances for prefunctor.symmetrify
@[protected, instance]
def prefunctor.symmetrify_map_reverse {U : Type u_1} {V : Type u_2} [quiver U] [quiver V] (φ : U ⥤q V) :
Equations
@[protected, instance]
def quiver.push.quiver.has_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V V')  :
Equations
• = {reverse' := λ (a b : (F : a b), quiver.push_quiver.cases_on F (λ {F_X F_Y : V} (F_f : F_X F_Y) (H_1 : a = σ F_X), eq.rec (λ (F : σ F_X b) (H_2 : b = σ F_Y), eq.rec (λ (F : σ F_X σ F_Y) (H_3 : , eq.rec _) _ F) _ F) _ _ _}
@[protected, instance]
def quiver.push.quiver.has_involutive_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V V')  :
Equations
• = {to_has_reverse := {reverse' := λ (a b : (F : a b), quiver.push_quiver.cases_on F (λ {F_X F_Y : V} (F_f : F_X F_Y) (H_1 : a = σ F_X), eq.rec (λ (F : σ F_X b) (H_2 : b = σ F_Y), eq.rec (λ (F : σ F_X σ F_Y) (H_3 : , eq.rec _) _ F) _ F) _ _ _}, inv' := _}
theorem quiver.push.of_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V V') (X Y : V) (f : X Y) :
@[protected, instance]
def quiver.push.of_map_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V V')  :
Equations
def quiver.is_preconnected (V : Type u_1) [quiver V] :
Prop

A quiver is preconnected iff there exists a path between any pair of vertices. Note that if V doesn't has_reverse, then the definition is stronger than simply having a preconnected underlying simple_graph`, since a path in one direction doesn't induce one in the other.

Equations