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

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

quiver.symmetrify V = V

Instances for quiver.symmetrify

source

@[protected, instance]

def quiver.symmetrify_quiver (V : Type u) [quiver V] :

quiver (quiver.symmetrify V)

Equations

quiver.symmetrify_quiver V = {hom := λ (a b : V), (a ⟶ b) ⊕ (b ⟶ a)}

source

@[class]

structure quiver.has_reverse (V : Type u_2) [quiver V] :

Type (max u_2 v)

reverse' : Π {a b : V}, (a ⟶ b) → (b ⟶ a)

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

source

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

quiver.reverse = quiver.has_reverse.reverse'

source

@[class]

structure quiver.has_involutive_reverse (V : Type u_2) [quiver V] :

Type (max u_2 v)

to_has_reverse : quiver.has_reverse V
inv' : ∀ {a b : V} (f : a ⟶ b), quiver.reverse (quiver.reverse f) = f

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

source

@[simp]

theorem quiver.reverse_reverse {V : Type u_2} [quiver V] [h : quiver.has_involutive_reverse V] {a b : V} (f : a ⟶ b) :

quiver.reverse (quiver.reverse f) = f

source

@[simp]

theorem quiver.reverse_inj {V : Type u_2} [quiver V] [quiver.has_involutive_reverse V] {a b : V} (f g : a ⟶ b) :

quiver.reverse f = quiver.reverse g ↔ f = g

source

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

f = quiver.reverse g ↔ quiver.reverse f = g

source

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

Type

map_reverse' : ∀ {u v : U} (e : u ⟶ v), φ.map (quiver.reverse e) = quiver.reverse (φ.map e)

A prefunctor preserving reversal of arrows

Instances of this typeclass

Instances of other typeclasses for prefunctor.map_reverse

prefunctor.map_reverse.has_sizeof_inst

source

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

φ.map (quiver.reverse e) = quiver.reverse (φ.map e)

source

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

(φ ⋙q ψ).map_reverse

Equations

φ.map_reverse_comp ψ = {map_reverse' := _}

source

@[protected, instance]

def prefunctor.map_reverse_id {U : Type u_1} [quiver U] [quiver.has_reverse U] :

(𝟭q U).map_reverse

Equations

prefunctor.map_reverse_id = {map_reverse' := _}

source

@[protected, instance]

def quiver.symmetrify.has_reverse {V : Type u_2} [quiver V] :

quiver.has_reverse (quiver.symmetrify V)

Equations

quiver.symmetrify.has_reverse = {reverse' := λ (a b : quiver.symmetrify V) (e : a ⟶ b), sum.swap e}

source

@[protected, instance]

def quiver.symmetrify.has_involutive_reverse {V : Type u_2} [quiver V] :

quiver.has_involutive_reverse (quiver.symmetrify V)

Equations

quiver.symmetrify.has_involutive_reverse = {to_has_reverse := {reverse' := λ (_x _x_1 : quiver.symmetrify V) (e : _x ⟶ _x_1), sum.swap e}, inv' := _}

source

@[simp]

theorem quiver.symmetrify_reverse {V : Type u_2} [quiver V] {a b : quiver.symmetrify V} (e : a ⟶ b) :

quiver.reverse e = sum.swap e

source

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

source

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

source

@[simp]

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

quiver.path a b → quiver.path b a

Reverse the direction of a path.

Equations

(p.cons e).reverse = (quiver.reverse e).to_path.comp p.reverse
quiver.path.nil.reverse = quiver.path.nil

source

@[simp]

theorem quiver.path.reverse_to_path {V : Type u_2} [quiver V] [quiver.has_reverse V] {a b : V} (f : a ⟶ b) :

f.to_path.reverse = (quiver.reverse f).to_path

source

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

(p.comp q).reverse = q.reverse.comp p.reverse

source

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

p.reverse.reverse = p

source

@[simp]

theorem quiver.symmetrify.of_map {V : Type u_2} [quiver V] (X Y : V) (f : X ⟶ Y) :

quiver.symmetrify.of.map f = sum.inl f

source

def quiver.symmetrify.of {V : Type u_2} [quiver V] :

V ⥤q quiver.symmetrify V

The inclusion of a quiver in its symmetrification

Equations

quiver.symmetrify.of = {obj := id V, map := λ (X Y : V) (f : X ⟶ Y), sum.inl f}

source

@[simp]

theorem quiver.symmetrify.of_obj {V : Type u_2} [quiver V] (a : V) :

quiver.symmetrify.of.obj a = id a

source

def quiver.symmetrify.lift {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] [quiver.has_reverse V'] (φ : V ⥤q V') :

quiver.symmetrify 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

quiver.symmetrify.lift φ = {obj := φ.obj, map := λ (X Y : quiver.symmetrify V) (f : X ⟶ Y), sum.rec (λ (fwd : X ⟶ Y), φ.map fwd) (λ (bwd : Y ⟶ X), quiver.reverse (φ.map bwd)) f}

source

theorem quiver.symmetrify.lift_spec {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] [quiver.has_reverse V'] (φ : V ⥤q V') :

quiver.symmetrify.of ⋙q quiver.symmetrify.lift φ = φ

source

theorem quiver.symmetrify.lift_reverse {V : Type u_2} [quiver V] {V' : Type u_4} [quiver V'] [h : quiver.has_involutive_reverse V'] (φ : V ⥤q V') {X Y : quiver.symmetrify V} (f : X ⟶ Y) :

(quiver.symmetrify.lift φ).map (quiver.reverse f) = quiver.reverse ((quiver.symmetrify.lift φ).map f)

source

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

Φ = quiver.symmetrify.lift φ

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

source

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

source

@[simp]

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

φ.symmetrify.obj ᾰ = φ.obj ᾰ

source

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

quiver.symmetrify U ⥤q quiver.symmetrify V

A prefunctor canonically defines a prefunctor of the symmetrifications.

Equations

φ.symmetrify = {obj := φ.obj, map := λ (X Y : quiver.symmetrify U), sum.map φ.map φ.map}

Instances for prefunctor.symmetrify

prefunctor.symmetrify_map_reverse

source

@[protected, instance]

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

φ.symmetrify.map_reverse

Equations

φ.symmetrify_map_reverse = {map_reverse' := _}

source

@[protected, instance]

def quiver.push.quiver.has_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V → V') [quiver.has_reverse V] :

quiver.has_reverse (quiver.push σ)

Equations

quiver.push.quiver.has_reverse σ = {reverse' := λ (a b : quiver.push σ) (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 : F == quiver.push_quiver.arrow F_f), eq.rec (quiver.push_quiver.arrow (quiver.reverse F_f)) _) _ F) _ F) _ _ _}

source

@[protected, instance]

def quiver.push.quiver.has_involutive_reverse {V : Type u_2} [quiver V] {V' : Type u_4} (σ : V → V') [quiver.has_involutive_reverse V] :

quiver.has_involutive_reverse (quiver.push σ)

Equations

quiver.push.quiver.has_involutive_reverse σ = {to_has_reverse := {reverse' := λ (a b : quiver.push σ) (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 : F == quiver.push_quiver.arrow F_f), eq.rec (quiver.push_quiver.arrow (quiver.reverse F_f)) _) _ F) _ F) _ _ _}, inv' := _}

source

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

quiver.reverse ((quiver.push.of σ).map f) = (quiver.push.of σ).map (quiver.reverse f)

source

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

(quiver.push.of σ).map_reverse

Equations

quiver.push.of_map_reverse σ = {map_reverse' := _}

source

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

quiver.is_preconnected V = ∀ (X Y : V), nonempty (quiver.path X Y)