mathlib3 documentation

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:

@[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]
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] [quiver.has_reverse 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)

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] [h : quiver.has_involutive_reverse V] {a b : V} (f : a b) :
@[simp]
theorem quiver.reverse_inj {V : Type u_2} [quiver V] [quiver.has_involutive_reverse V] {a b : V} (f g : a b) :
theorem quiver.eq_reverse_iff {V : Type u_2} [quiver V] [quiver.has_involutive_reverse 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] [quiver.has_reverse U] [quiver.has_reverse 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] [quiver.has_reverse U] [quiver.has_reverse 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] [quiver.has_reverse U] [quiver.has_reverse V] [quiver.has_reverse W] (φ : U ⥤q V) (ψ : V ⥤q W) [φ.map_reverse] [ψ.map_reverse] :
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] [quiver.has_reverse V] {a b : V} :

Reverse the direction of a path.

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

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'] [quiver.has_reverse 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_unique {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] [quiver.has_reverse V'] (φ : V ⥤q V') (Φ : quiver.symmetrify V ⥤q V') (hΦ : quiver.symmetrify.of ⋙q Φ = φ) [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 = sum.map φ.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]
Equations
@[protected, instance]
Equations
theorem quiver.push.of_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V V') [h : quiver.has_involutive_reverse 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') [h : quiver.has_involutive_reverse 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