Documentation

Mathlib.Combinatorics.Quiver.Symmetric

Symmetric quivers and arrow reversal #

This file contains constructions related to symmetric quivers:

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
Equations
class Quiver.HasReverse (V : Type u_1) [inst : Quiver V] :
Type (maxu_1v)
  • the map which sends an arrow to its reverse

    reverse' : {a b : V} → (a b) → (b a)

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

Instances
    def Quiver.reverse {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} :
    (a b) → (b a)

    Reverse the direction of an arrow.

    Equations
    • Quiver.reverse = Quiver.HasReverse.reverse'
    class Quiver.HasInvolutiveReverse (V : Type u_1) [inst : Quiver V] extends Quiver.HasReverse :
    Type (maxu_1v)

    A quiver HasInvolutiveReverse if reversing twice is the identity.`

    Instances
      @[simp]
      theorem Quiver.reverse_reverse {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) :
      @[simp]
      theorem Quiver.reverse_inj {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) (g : a b) :
      theorem Quiver.eq_reverse_iff {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) (g : b a) :
      class Prefunctor.MapReverse {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst : Quiver V] [inst : Quiver.HasReverse U] [inst : Quiver.HasReverse V] (φ : U ⥤q V) :

      A prefunctor preserving reversal of arrows

      Instances
        @[simp]
        theorem Prefunctor.map_reverse {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst : Quiver V] [inst : Quiver.HasReverse U] [inst : Quiver.HasReverse V] (φ : U ⥤q V) [inst : Prefunctor.MapReverse φ] {u : U} {v : U} (e : u v) :
        instance Prefunctor.mapReverseComp {U : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Quiver U] [inst : Quiver V] [inst : Quiver W] [inst : Quiver.HasReverse U] [inst : Quiver.HasReverse V] [inst : Quiver.HasReverse W] (φ : U ⥤q V) (ψ : V ⥤q W) [inst : Prefunctor.MapReverse φ] [inst : Prefunctor.MapReverse ψ] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance Prefunctor.mapReverseId {U : Type u_1} [inst : Quiver U] [inst : Quiver.HasReverse U] :
        Equations
        Equations
        • Quiver.instHasReverseSymmetrifySymmetrifyQuiver = { reverse' := fun {a b} e => Sum.swap e }
        Equations
        @[simp]
        theorem Quiver.symmetrify_reverse {V : Type u_1} [inst : Quiver V] {a : Quiver.Symmetrify V} {b : Quiver.Symmetrify V} (e : a b) :
        @[inline]
        abbrev Quiver.Hom.toPos {V : Type u_1} [inst : Quiver V] {X : V} {Y : V} (f : X Y) :
        X Y

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

        Equations
        @[inline]
        abbrev Quiver.Hom.toNeg {V : Type u_1} [inst : Quiver V] {X : V} {Y : V} (f : X Y) :
        Y X

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

        Equations
        def Quiver.Path.reverse {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} :

        Reverse the direction of a path.

        Equations
        @[simp]
        theorem Quiver.Path.reverse_toPath {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} (f : a b) :
        @[simp]
        theorem Quiver.Path.reverse_comp {V : Type u_1} [inst : Quiver V] [inst : Quiver.HasReverse V] {a : V} {b : V} {c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) :
        @[simp]
        theorem Quiver.Path.reverse_reverse {V : Type u_1} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (p : Quiver.Path a b) :
        def Quiver.Symmetrify.of {V : Type u_1} [inst : Quiver V] :

        The inclusion of a quiver in its symmetrification

        Equations
        • Quiver.Symmetrify.of = { obj := id, map := fun {X Y} => Sum.inl }
        def Quiver.Symmetrify.lift {V : Type u_1} [inst : Quiver V] {V' : Type u_2} [inst : Quiver V'] [inst : Quiver.HasReverse 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} [inst : Quiver V] {V' : Type u_1} [inst : Quiver V'] [inst : Quiver.HasReverse V'] (φ : V ⥤q V') :
        Quiver.Symmetrify.of ⋙q Quiver.Symmetrify.lift φ = φ
        theorem Quiver.Symmetrify.lift_unique {V : Type u_2} [inst : Quiver V] {V' : Type u_1} [inst : Quiver V'] [inst : Quiver.HasReverse V'] (φ : V ⥤q V') (Φ : Quiver.Symmetrify V ⥤q V') (hΦ : Quiver.Symmetrify.of ⋙q Φ = φ) (hΦinv : ∀ {X Y : Quiver.Symmetrify V} (f : X Y), Prefunctor.map Φ (Quiver.reverse f) = Quiver.reverse (Prefunctor.map Φ f)) :

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

        instance Quiver.Push.instHasReversePushInstQuiverPush {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : VV') [inst : Quiver.HasReverse V] :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Quiver.Push.of_reverse {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : VV') [inst : Quiver.HasInvolutiveReverse V] (X : V) (Y : V) (f : X Y) :
        instance Quiver.Push.ofMapReverse {V : Type u_1} [inst : Quiver V] {V' : Type u_2} (σ : VV') [h : Quiver.HasInvolutiveReverse V] :
        Equations
        • One or more equations did not get rendered due to their size.
        def Quiver.IsPreconnected (V : Type u_1) [inst : Quiver V] :

        A quiver is preconnected iff there exists a path between any pair of vertices. Note that if V doesn't HasReverse, 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