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
Instances For
    Equations
    class Quiver.HasReverse (V : Type u_2) [Quiver V] :
    Type (max u_2 v)

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

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

      the map which sends an arrow to its reverse

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

      Reverse the direction of an arrow.

      Equations
      • Quiver.reverse = Quiver.HasReverse.reverse'
      Instances For
        class Quiver.HasInvolutiveReverse (V : Type u_2) [Quiver V] extends Quiver.HasReverse :
        Type (max u_2 v)

        A quiver HasInvolutiveReverse if reversing twice is the identity.

        Instances
          theorem Quiver.HasInvolutiveReverse.inv' {V : Type u_2} [Quiver V] [self : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) :

          reverse is involutive

          @[simp]
          theorem Quiver.reverse_reverse {V : Type u_2} [Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) :
          @[simp]
          theorem Quiver.reverse_inj {V : Type u_2} [Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (f : a b) (g : a b) :
          theorem Quiver.eq_reverse_iff {V : Type u_2} [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} [Quiver U] [Quiver V] [Quiver.HasReverse U] [Quiver.HasReverse V] (φ : U ⥤q V) :

          A prefunctor preserving reversal of arrows

          Instances
            theorem Prefunctor.MapReverse.map_reverse' {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] [Quiver.HasReverse U] [Quiver.HasReverse V] {φ : U ⥤q V} [self : φ.MapReverse] {u : U} {v : U} (e : u v) :
            φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)

            The image of a reverse is the reverse of the image.

            @[simp]
            theorem Prefunctor.map_reverse {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] [Quiver.HasReverse U] [Quiver.HasReverse V] (φ : U ⥤q V) [φ.MapReverse] {u : U} {v : U} (e : u v) :
            φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
            instance Prefunctor.mapReverseComp {U : Type u_1} {V : Type u_2} {W : Type u_3} [Quiver U] [Quiver V] [Quiver W] [Quiver.HasReverse U] [Quiver.HasReverse V] [Quiver.HasReverse W] (φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] :
            (φ ⋙q ψ).MapReverse
            Equations
            • =
            instance Prefunctor.mapReverseId {U : Type u_1} [Quiver U] [Quiver.HasReverse U] :
            (𝟭q U).MapReverse
            Equations
            • =
            Equations
            Equations
            @[simp]
            @[reducible, inline]
            abbrev Quiver.Hom.toPos {V : Type u_2} [Quiver V] {X : V} {Y : V} (f : X Y) :
            X Y

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

            Equations
            Instances For
              @[reducible, inline]
              abbrev Quiver.Hom.toNeg {V : Type u_2} [Quiver V] {X : V} {Y : V} (f : X Y) :
              Y X

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

              Equations
              Instances For
                def Quiver.Path.reverse {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a : V} {b : V} :

                Reverse the direction of a path.

                Equations
                • Quiver.Path.nil.reverse = Quiver.Path.nil
                • (p.cons e).reverse = (Quiver.reverse e).toPath.comp p.reverse
                Instances For
                  @[simp]
                  theorem Quiver.Path.reverse_toPath {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a : V} {b : V} (f : a b) :
                  f.toPath.reverse = (Quiver.reverse f).toPath
                  @[simp]
                  theorem Quiver.Path.reverse_comp {V : Type u_2} [Quiver V] [Quiver.HasReverse V] {a : V} {b : V} {c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) :
                  (p.comp q).reverse = q.reverse.comp p.reverse
                  @[simp]
                  theorem Quiver.Path.reverse_reverse {V : Type u_2} [Quiver V] [h : Quiver.HasInvolutiveReverse V] {a : V} {b : V} (p : Quiver.Path a b) :
                  p.reverse.reverse = p

                  The inclusion of a quiver in its symmetrification

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

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

                      @[simp]
                      theorem Prefunctor.symmetrify_obj {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) :
                      ∀ (a : U), φ.symmetrify.obj a = φ.obj a
                      @[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} (a : (X Y) (Y X)), φ.symmetrify.map a = Sum.map φ.map φ.map a
                      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
                        instance Prefunctor.symmetrify_mapReverse {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (φ : U ⥤q V) :
                        φ.symmetrify.MapReverse
                        Equations
                        • =
                        instance Quiver.Push.instHasReverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : VV') [Quiver.HasReverse V] :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        theorem Quiver.Push.of_reverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : VV') [Quiver.HasInvolutiveReverse V] (X : V) (Y : V) (f : X Y) :
                        instance Quiver.Push.ofMapReverse {V : Type u_2} [Quiver V] {V' : Type u_4} (σ : VV') [h : Quiver.HasInvolutiveReverse V] :
                        (Quiver.Push.of σ).MapReverse
                        Equations
                        • =

                        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 SimpleGraph, since a path in one direction doesn't induce one in the other.

                        Equations
                        Instances For