Documentation

Mathlib.Combinatorics.Quiver.Covering

Covering #

This file defines coverings of quivers as prefunctors that are bijective on the so-called stars and costars at each vertex of the domain.

Main definitions #

Main statements #

TODO #

Clean up the namespaces by renaming Prefunctor to Quiver.Prefunctor.

Tags #

Cover, covering, quiver, path, lift

@[reducible, inline]
abbrev Quiver.Star {U : Type u_1} [Quiver U] (u : U) :
Type (max u_1 u)

The Quiver.Star at a vertex is the collection of arrows whose source is the vertex. The type Quiver.Star u is defined to be Σ (v : U), (u ⟶ v).

Equations
Instances For
    @[reducible, inline]
    abbrev Quiver.Star.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (f : u v) :

    Constructor for Quiver.Star. Defined to be Sigma.mk.

    Equations
    Instances For
      @[reducible, inline]
      abbrev Quiver.Costar {U : Type u_1} [Quiver U] (v : U) :
      Type (max u_1 u)

      The Quiver.Costar at a vertex is the collection of arrows whose target is the vertex. The type Quiver.Costar v is defined to be Σ (u : U), (u ⟶ v).

      Equations
      Instances For
        @[reducible, inline]
        abbrev Quiver.Costar.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (f : u v) :

        Constructor for Quiver.Costar. Defined to be Sigma.mk.

        Equations
        Instances For
          @[simp]
          theorem Prefunctor.star_snd {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
          ∀ (a : Quiver.Star u), (φ.star u a).snd = φ.map a.snd
          @[simp]
          theorem Prefunctor.star_fst {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
          ∀ (a : Quiver.Star u), (φ.star u a).fst = φ.obj a.fst
          def Prefunctor.star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
          Quiver.Star uQuiver.Star (φ.obj u)

          A prefunctor induces a map of Quiver.Star at every vertex.

          Equations
          Instances For
            @[simp]
            theorem Prefunctor.costar_fst {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
            ∀ (a : Quiver.Costar u), (φ.costar u a).fst = φ.obj a.fst
            @[simp]
            theorem Prefunctor.costar_snd {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
            ∀ (a : Quiver.Costar u), (φ.costar u a).snd = φ.map a.snd
            def Prefunctor.costar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
            Quiver.Costar uQuiver.Costar (φ.obj u)

            A prefunctor induces a map of Quiver.Costar at every vertex.

            Equations
            Instances For
              @[simp]
              theorem Prefunctor.star_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (e : u v) :
              φ.star u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e)
              @[simp]
              theorem Prefunctor.costar_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (e : u v) :
              φ.costar v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e)
              theorem Prefunctor.star_comp {U : Type u_1} [Quiver U] {V : Type u_3} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (u : U) :
              (φ ⋙q ψ).star u = ψ.star (φ.obj u) φ.star u
              theorem Prefunctor.costar_comp {U : Type u_1} [Quiver U] {V : Type u_3} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (u : U) :
              (φ ⋙q ψ).costar u = ψ.costar (φ.obj u) φ.costar u
              structure Prefunctor.IsCovering {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) :

              A prefunctor is a covering of quivers if it defines bijections on all stars and costars.

              Instances For
                theorem Prefunctor.IsCovering.star_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {φ : U ⥤q V} (self : φ.IsCovering) (u : U) :
                Function.Bijective (φ.star u)
                theorem Prefunctor.IsCovering.costar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {φ : U ⥤q V} (self : φ.IsCovering) (u : U) :
                Function.Bijective (φ.costar u)
                @[simp]
                theorem Prefunctor.IsCovering.map_injective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : φ.IsCovering) {u : U} {v : U} :
                Function.Injective fun (f : u v) => φ.map f
                theorem Prefunctor.IsCovering.comp {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {W : Type u_3} [Quiver W] (ψ : V ⥤q W) (hφ : φ.IsCovering) (hψ : ψ.IsCovering) :
                (φ ⋙q ψ).IsCovering
                theorem Prefunctor.IsCovering.of_comp_right {U : Type u_3} [Quiver U] {V : Type u_1} [Quiver V] (φ : U ⥤q V) {W : Type u_2} [Quiver W] (ψ : V ⥤q W) (hψ : ψ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) :
                φ.IsCovering
                theorem Prefunctor.IsCovering.of_comp_left {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {W : Type u_3} [Quiver W] (ψ : V ⥤q W) (hφ : φ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) (φsur : Function.Surjective φ.obj) :
                ψ.IsCovering
                def Quiver.symmetrifyStar {U : Type u_1} [Quiver U] (u : U) :
                Quiver.Star (Quiver.Symmetrify.of.obj u) Quiver.Star u Quiver.Costar u

                The star of the symmetrification of a quiver at a vertex u is equivalent to the sum of the star and the costar at u in the original quiver.

                Equations
                Instances For
                  def Quiver.symmetrifyCostar {U : Type u_1} [Quiver U] (u : U) :
                  Quiver.Costar (Quiver.Symmetrify.of.obj u) Quiver.Costar u Quiver.Star u

                  The costar of the symmetrification of a quiver at a vertex u is equivalent to the sum of the costar and the star at u in the original quiver.

                  Equations
                  Instances For
                    theorem Prefunctor.symmetrifyStar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
                    φ.symmetrify.star u = (Quiver.symmetrifyStar (φ.obj u)).symm Sum.map (φ.star u) (φ.costar u) (Quiver.symmetrifyStar u)
                    theorem Prefunctor.symmetrifyCostar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :
                    φ.symmetrify.costar u = (Quiver.symmetrifyCostar (φ.obj u)).symm Sum.map (φ.costar u) (φ.star u) (Quiver.symmetrifyCostar u)
                    theorem Prefunctor.IsCovering.symmetrify {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : φ.IsCovering) :
                    φ.symmetrify.IsCovering
                    @[reducible, inline]
                    abbrev Quiver.PathStar {U : Type u_1} [Quiver U] (u : U) :
                    Type (max u_1 u u_1)

                    The path star at a vertex u is the type of all paths starting at u. The type Quiver.PathStar u is defined to be Σ v : U, Path u v.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Quiver.PathStar.mk {U : Type u_1} [Quiver U] {u : U} {v : U} (p : Quiver.Path u v) :

                      Constructor for Quiver.PathStar. Defined to be Sigma.mk.

                      Equations
                      Instances For
                        def Prefunctor.pathStar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (u : U) :

                        A prefunctor induces a map of path stars.

                        Equations
                        Instances For
                          @[simp]
                          theorem Prefunctor.pathStar_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u : U} {v : U} (p : Quiver.Path u v) :
                          φ.pathStar u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (φ.mapPath p)
                          theorem Prefunctor.pathStar_injective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Injective (φ.star u)) (u : U) :
                          Function.Injective (φ.pathStar u)
                          theorem Prefunctor.pathStar_surjective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Surjective (φ.star u)) (u : U) :
                          Function.Surjective (φ.pathStar u)
                          theorem Prefunctor.pathStar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (u : U), Function.Bijective (φ.star u)) (u : U) :
                          Function.Bijective (φ.pathStar u)
                          theorem Prefunctor.IsCovering.pathStar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {φ : U ⥤q V} (hφ : φ.IsCovering) (u : U) :
                          Function.Bijective (φ.pathStar u)
                          @[simp]
                          @[simp]

                          In a quiver with involutive inverses, the star and costar at every vertex are equivalent. This map is induced by Quiver.reverse.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Prefunctor.costar_conj_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [φ.MapReverse] (u : U) :
                            φ.costar u = (Quiver.starEquivCostar (φ.obj u)) φ.star u (Quiver.starEquivCostar u).symm
                            theorem Prefunctor.bijective_costar_iff_bijective_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [φ.MapReverse] (u : U) :
                            Function.Bijective (φ.costar u) Function.Bijective (φ.star u)
                            theorem Prefunctor.isCovering_of_bijective_star {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [φ.MapReverse] (h : ∀ (u : U), Function.Bijective (φ.star u)) :
                            φ.IsCovering
                            theorem Prefunctor.isCovering_of_bijective_costar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) [Quiver.HasInvolutiveReverse U] [Quiver.HasInvolutiveReverse V] [φ.MapReverse] (h : ∀ (u : U), Function.Bijective (φ.costar u)) :
                            φ.IsCovering