Documentation

TauCeti.RepresentationTheory.Quiver.Kronecker.Basic

The generalized Kronecker quiver #

The generalized Kronecker quiver has two vertices, a source and a target, and one arrow from the source to the target for each element of an arrow type A. Taking A = Fin 2 gives the Kronecker quiver • ⇉ •, the smallest connected acyclic quiver that is not of Dynkin type and hence the boundary case of Gabriel's theorem; A = Fin 1 gives the A₂ quiver • → •. (Dropping acyclicity there would be wrong: the one-loop quiver of TauCeti.RepresentationTheory.Quiver.OneLoop.Basic is connected, smaller, and not of Dynkin type.)

This file constructs the quiver and classifies its paths: it is acyclic, and its only nontrivial paths are the arrows themselves. The equivalence totalPathEquivArrowSumBool identifies all indexed paths with A ⊕ Bool, supporting transport of finiteness, countability and infinitude. The same classification is carried out for the quiver reflected at its target, which is the generalized Kronecker quiver read the other way round. The dimension of its path algebra is computed in TauCeti.RepresentationTheory.Quiver.Kronecker.PathAlgebra, its Euler and Tits forms in TauCeti.RepresentationTheory.Quiver.Kronecker.EulerForm. Its representations are built in TauCeti.RepresentationTheory.Quiver.Kronecker.Representation, and its representation type -- infinite as soon as there are two arrows -- is settled in TauCeti.RepresentationTheory.Quiver.Kronecker.FiniteRepType.

Main definitions #

Main results #

References #

Derksen--Weyman, An Introduction to Quiver Representations, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.

source
inductive TauCeti.Quiver.Kronecker (A : Type v) :
Type

The generalized Kronecker quiver on an arrow type A: two vertices, a source src and a target tgt, with one arrow src ⟶ tgt for each element of A and no other arrows. The classical Kronecker quiver • ⇉ • is the case A = Fin 2, and the A₂ quiver • → • is the case A = Fin 1.

  • src {A : Type v} : Kronecker A

    The source vertex, the tail of every arrow.

  • tgt {A : Type v} : Kronecker A

    The target vertex, the head of every arrow.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.Quiver.Kronecker.instQuiver {A : Type v} :
    Quiver (Kronecker A)
    Equations
    • One or more equations did not get rendered due to their size.

    The two vertices #

    source
    theorem TauCeti.Quiver.Kronecker.src_ne_tgt {A : Type v} :
    src ≠ tgt

    The source and the target are distinct vertices.

    source
    @[instance_reducible]
    instance TauCeti.Quiver.Kronecker.instDecidableEq {A : Type v} :
    DecidableEq (Kronecker A)
    Equations
    source
    @[instance_reducible]
    instance TauCeti.Quiver.Kronecker.instFintype {A : Type v} :
    Fintype (Kronecker A)
    Equations
    source
    theorem TauCeti.Quiver.Kronecker.univ_eq {A : Type v} :
    Finset.univ = {src, tgt}

    The vertex type is the pair {src, tgt}.

    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.card_eq_two {A : Type v} :
    Fintype.card (Kronecker A) = 2
    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.sum_univ {A : Type v} {M : Type w} [AddCommMonoid M] (f : Kronecker A → M) :
    ∑ v : Kronecker A, f v = f src + f tgt

    A sum over the two vertices is the sum of its two values.

    source
    theorem TauCeti.Quiver.Kronecker.eq_zero_iff {A : Type v} {M : Type w} [Zero M] {f : Kronecker A → M} :
    f = 0 ↔ f src = 0 ∧ f tgt = 0

    A function on the vertices vanishes exactly when both of its values do.

    source
    def TauCeti.Quiver.Kronecker.vertexEquiv {A : Type v} :
    Kronecker A ≃ Fin 2

    The two vertices as indices in Fin 2, the target first: tgt is 0 and src is 1.

    The order is the one that makes the path algebra upper triangular rather than lower triangular. In TauCeti.RepresentationTheory.Quiver.Kronecker.UpperTriangular a path is sent to the matrix unit in the row of its target and the column of its source, because an arrow acts on a left module from its source to its target; so the arrows, all of which run from src to tgt, occupy entries above the diagonal exactly when tgt comes first.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.Quiver.Kronecker.vertexEquiv_src {A : Type v} :
      vertexEquiv src = 1
      source
      @[simp]
      theorem TauCeti.Quiver.Kronecker.vertexEquiv_tgt {A : Type v} :
      vertexEquiv tgt = 0
      source
      @[simp]
      theorem TauCeti.Quiver.Kronecker.vertexEquiv_symm_zero {A : Type v} :
      vertexEquiv.symm 0 = tgt
      source
      @[simp]
      theorem TauCeti.Quiver.Kronecker.vertexEquiv_symm_one {A : Type v} :
      vertexEquiv.symm 1 = src

      The arrows #

      source
      def TauCeti.Quiver.Kronecker.arrow {A : Type v} (a : A) :
      src ⟶ tgt

      The arrow of the generalized Kronecker quiver indexed by an element of the arrow type. The arrows from the source to the target are exactly the elements of the arrow type, and the identification is definitional.

      Equations
      Instances For
        source
        theorem TauCeti.Quiver.Kronecker.arrow_def {A : Type v} (a : A) :
        arrow a = a

        The arrows from the source to the target are the elements of the arrow type, and arrow is that identification. This is not @[simp]: rewriting arrow a to a would erase the named constructor from every goal, leaving toPath_arrow and the pathEquivArrow lemmas below unable to fire.

        source
        instance TauCeti.Quiver.Kronecker.instIsEmptyHomSrc {A : Type v} :
        IsEmpty (src ⟶ src)
        source
        instance TauCeti.Quiver.Kronecker.instIsEmptyHomTgtSrc {A : Type v} :
        IsEmpty (tgt ⟶ src)
        source
        instance TauCeti.Quiver.Kronecker.instIsEmptyHomTgt {A : Type v} :
        IsEmpty (tgt ⟶ tgt)
        source
        theorem TauCeti.Quiver.Kronecker.isEmpty_hom_to_src {A : Type v} (a : Kronecker A) :
        IsEmpty (a ⟶ src)

        No arrow ends at the source vertex.

        source
        theorem TauCeti.Quiver.Kronecker.isEmpty_hom_from_tgt {A : Type v} (b : Kronecker A) :
        IsEmpty (tgt ⟶ b)

        No arrow starts at the target vertex.

        source
        theorem TauCeti.Quiver.Kronecker.isSource_src {A : Type v} :
        IsSource src

        The source vertex is a source.

        source
        theorem TauCeti.Quiver.Kronecker.isSink_tgt {A : Type v} :
        IsSink tgt

        The target vertex is a sink.

        source
        instance TauCeti.Quiver.Kronecker.instFiniteHom {A : Type v} [Finite A] (a b : Kronecker A) :
        Finite (a ⟶ b)
        source
        @[instance_reducible]
        instance TauCeti.Quiver.Kronecker.instFintypeHom {A : Type v} [Fintype A] (a b : Kronecker A) :
        Fintype (a ⟶ b)
        Equations
        source
        @[simp]
        theorem TauCeti.Quiver.Kronecker.card_hom_src_tgt {A : Type v} [Fintype A] :
        Fintype.card (src ⟶ tgt) = Fintype.card A

        There are as many arrows from the source to the target as there are elements of the arrow type.

        The paths #

        source
        theorem TauCeti.Quiver.Kronecker.path_src_src_eq_nil {A : Type v} (p : Quiver.Path src src) :
        p = Quiver.Path.nil

        The only closed path at the source vertex is the trivial one.

        source
        theorem TauCeti.Quiver.Kronecker.path_tgt_tgt_eq_nil {A : Type v} (p : Quiver.Path tgt tgt) :
        p = Quiver.Path.nil

        The only closed path at the target vertex is the trivial one.

        source
        theorem TauCeti.Quiver.Kronecker.isAcyclic {A : Type v} :
        IsAcyclic (Kronecker A)

        The generalized Kronecker quiver is acyclic: all of its arrows run the same way.

        source
        @[instance_reducible]
        instance TauCeti.Quiver.Kronecker.instUniquePathSrc {A : Type v} :
        Unique (Quiver.Path src src)
        Equations
        source
        @[instance_reducible]
        instance TauCeti.Quiver.Kronecker.instUniquePathTgt {A : Type v} :
        Unique (Quiver.Path tgt tgt)
        Equations
        source
        instance TauCeti.Quiver.Kronecker.instIsEmptyPathTgtSrc {A : Type v} :
        IsEmpty (Quiver.Path tgt src)
        source
        def TauCeti.Quiver.Kronecker.arrowPath {A : Type v} (a : A) :
        Quiver.Path src tgt

        The length-one path traced by an arrow of the generalized Kronecker quiver.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Quiver.Kronecker.toPath_arrow {A : Type v} (a : A) :
          (arrow a).toPath = arrowPath a

          The length-one path of an arrow is the path that arrow traces.

          source
          theorem TauCeti.Quiver.Kronecker.arrowPath_injective {A : Type v} :
          Function.Injective arrowPath

          Distinct arrows trace distinct paths.

          source
          theorem TauCeti.Quiver.Kronecker.arrowPath_surjective {A : Type v} :
          Function.Surjective arrowPath

          Every path from the source to the target is a single arrow.

          source
          @[instance_reducible]
          instance TauCeti.Quiver.Kronecker.instUniquePathSrcTgt {A : Type v} [Unique A] :
          Unique (Quiver.Path src tgt)

          Over the A₂ quiver there is exactly one path from the source to the target: the arrows are the paths src → tgt, and there is only one arrow.

          Equations
          source
          noncomputable def TauCeti.Quiver.Kronecker.pathEquivArrow {A : Type v} :
          Quiver.Path src tgt ≃ A

          The paths from the source to the target of the generalized Kronecker quiver are its arrows.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.Quiver.Kronecker.pathEquivArrow_symm_apply {A : Type v} (a : A) :
            pathEquivArrow.symm a = arrowPath a

            The inverse of the classification sends an arrow to the path it traces; the two are the same construction, so this holds definitionally.

            source
            @[simp]
            theorem TauCeti.Quiver.Kronecker.pathEquivArrow_arrowPath {A : Type v} (a : A) :
            pathEquivArrow (arrowPath a) = a

            The classification sends the path traced by an arrow back to that arrow.

            source
            @[simp]
            theorem TauCeti.Quiver.Kronecker.arrowPath_pathEquivArrow {A : Type v} (p : Quiver.Path src tgt) :
            arrowPath (pathEquivArrow p) = p

            Every path from the source to the target is traced by the arrow it classifies.

            source
            noncomputable def TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool {A : Type v} :
            TotalPath (Kronecker A) ≃ A ⊕ Bool

            Indexed paths are the arrows together with two trivial paths. The Boolean labels follow the vertex order: false represents the target, and true represents the source.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_arrowPath {A : Type v} (a : A) :
              totalPathEquivArrowSumBool ⟨src, ⟨tgt, arrowPath a⟩⟩ = Sum.inl a

              An arrow path is classified by the arrow it traces.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_tgt_nil {A : Type v} :
              totalPathEquivArrowSumBool ⟨tgt, ⟨tgt, Quiver.Path.nil⟩⟩ = Sum.inr false

              The trivial path at the target has Boolean label false.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_src_nil {A : Type v} :
              totalPathEquivArrowSumBool ⟨src, ⟨src, Quiver.Path.nil⟩⟩ = Sum.inr true

              The trivial path at the source has Boolean label true.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_symm_inl {A : Type v} (a : A) :
              totalPathEquivArrowSumBool.symm (Sum.inl a) = ⟨src, ⟨tgt, arrowPath a⟩⟩

              An arrow label reconstructs the path it traces.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_symm_inr_false {A : Type v} :
              totalPathEquivArrowSumBool.symm (Sum.inr false) = ⟨tgt, ⟨tgt, Quiver.Path.nil⟩⟩

              Boolean label false reconstructs the trivial path at the target.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.totalPathEquivArrowSumBool_symm_inr_true {A : Type v} :
              totalPathEquivArrowSumBool.symm (Sum.inr true) = ⟨src, ⟨src, Quiver.Path.nil⟩⟩

              Boolean label true reconstructs the trivial path at the source.

              source
              theorem TauCeti.Quiver.Kronecker.totalPath_eq_or {A : Type v} (x : TotalPath (Kronecker A)) :
              x = ⟨tgt, ⟨tgt, Quiver.Path.nil⟩⟩ ∨ (∃ (a : A), x = ⟨src, ⟨tgt, arrowPath a⟩⟩) ∨ x = ⟨src, ⟨src, Quiver.Path.nil⟩⟩

              Each path of a generalized Kronecker quiver is a trivial path at one of its two vertices, or the length-one path traced by an arrow.

              source
              @[instance_reducible]
              noncomputable instance TauCeti.Quiver.Kronecker.instFintypePath {A : Type v} [Fintype A] (a b : Kronecker A) :
              Fintype (Quiver.Path a b)
              Equations
              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.card_path_src_tgt {A : Type v} [Fintype A] :
              Fintype.card (Quiver.Path src tgt) = Fintype.card A

              There are as many paths from the source to the target as there are arrows: by pathEquivArrow, each such path is a single arrow.

              source
              @[simp]
              theorem TauCeti.Quiver.Kronecker.card_totalPath {A : Type v} [Fintype A] :
              Fintype.card (TotalPath (Kronecker A)) = Fintype.card A + 2

              The generalized Kronecker quiver on n arrows has n + 2 paths: the two trivial paths and the arrows themselves.

              The reflected quiver #

              A vertex of the quiver reflected at tgt has to be written @IsSink (Reflect (Kronecker A) tgt) _ src rather than IsSink (src : Reflect (Kronecker A) tgt): TauCeti.Quiver.Reflect is a type synonym for the vertex type, so the ascription is discharged definitionally and the quiver instance elaborated from it would be the unreflected one.

              source
              theorem TauCeti.Quiver.Kronecker.isSink_reflect_src {A : Type v} :
              IsSink src

              In the reflected quiver the source vertex is a sink. Reflecting at tgt reverses every arrow, so the generalized Kronecker quiver becomes the same quiver read the other way round.

              source
              theorem TauCeti.Quiver.Kronecker.isSource_reflect_tgt {A : Type v} :
              IsSource tgt

              In the reflected quiver the target vertex is a source, since it was a sink.

              source
              @[instance_reducible]
              instance TauCeti.Quiver.Kronecker.instUniquePathReflectTgtSrc {A : Type v} :
              Unique (Quiver.Path src src)

              The only closed path at the source of the reflected quiver is the trivial one.

              Equations
              source
              @[instance_reducible]
              instance TauCeti.Quiver.Kronecker.instUniquePathReflectTgt {A : Type v} :
              Unique (Quiver.Path tgt tgt)

              The only closed path at the target of the reflected quiver is the trivial one.

              Equations
              source
              instance TauCeti.Quiver.Kronecker.instIsEmptyPathReflectTgtSrc {A : Type v} :
              IsEmpty (Quiver.Path src tgt)

              The reflected quiver has no path from the source to the target: its arrows all run the other way.

              source
              noncomputable def TauCeti.Quiver.Kronecker.reflectArrowPath {A : Type v} (a : A) :
              Quiver.Path tgt src

              The length-one path of the reflected quiver traced by the reversed arrow attached to an element of the arrow type.

              Equations
              Instances For
                source
                theorem TauCeti.Quiver.Kronecker.reflectArrowPath_def {A : Type v} (a : A) :
                reflectArrowPath a = (reflectArrow tgt (arrow a)).toPath

                The path attached to an element of the arrow type is the one its reversed arrow traces.

                source
                def TauCeti.Quiver.Kronecker.reflectHomEquivArrow {A : Type v} :
                (tgt ⟶ src) ≃ A

                The arrows tgt ⟶ src of the reflected quiver are the elements of the arrow type, each being the reversal TauCeti.Quiver.reflectArrow of the arrow src ⟶ tgt it names. This is the arrow-level form of the path classification reflectPathEquivArrow below, and it is what reads an arrow of the reflected quiver back as an arrow of the generalized Kronecker quiver.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.Quiver.Kronecker.reflectHomEquivArrow_reflectArrow {A : Type v} (a : A) :
                  reflectHomEquivArrow (reflectArrow tgt (arrow a)) = a

                  Reading the reversal of an arrow back recovers the element of the arrow type it came from.

                  source
                  @[simp]
                  theorem TauCeti.Quiver.Kronecker.reflectArrow_arrow_reflectHomEquivArrow {A : Type v} (e : tgt ⟶ src) :
                  reflectArrow tgt (arrow (reflectHomEquivArrow e)) = e

                  Every arrow tgt ⟶ src of the reflected quiver is a reversed arrow: reversing the arrow it is read back as recovers it. This is the elimination rule that the path classification below runs on.

                  source
                  theorem TauCeti.Quiver.Kronecker.reflectArrowPath_injective {A : Type v} :
                  Function.Injective reflectArrowPath

                  Distinct arrows trace distinct paths in the reflected quiver.

                  source
                  theorem TauCeti.Quiver.Kronecker.reflectArrowPath_surjective {A : Type v} :
                  Function.Surjective reflectArrowPath

                  Every path from the target to the source of the reflected quiver is a single reversed arrow: the target is a source there and the source is a sink, so no two arrows compose.

                  source
                  noncomputable def TauCeti.Quiver.Kronecker.reflectPathEquivArrow {A : Type v} :
                  Quiver.Path tgt src ≃ A

                  The paths tgt → src of the reflected quiver are the elements of the arrow type, exactly as the paths src → tgt of the generalized Kronecker quiver are, by TauCeti.Quiver.Kronecker.pathEquivArrow.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.Quiver.Kronecker.reflectPathEquivArrow_symm_apply {A : Type v} (a : A) :
                    reflectPathEquivArrow.symm a = reflectArrowPath a

                    The inverse of the classification sends an element of the arrow type to the path its reversed arrow traces; the two are the same construction, so this holds definitionally.

                    source
                    @[simp]
                    theorem TauCeti.Quiver.Kronecker.reflectPathEquivArrow_reflectArrowPath {A : Type v} (a : A) :
                    reflectPathEquivArrow (reflectArrowPath a) = a

                    The classification sends the path traced by a reversed arrow back to the element of the arrow type it came from.

                    source
                    @[simp]
                    theorem TauCeti.Quiver.Kronecker.reflectArrowPath_reflectPathEquivArrow {A : Type v} (p : Quiver.Path tgt src) :
                    reflectArrowPath (reflectPathEquivArrow p) = p

                    Every path from the target to the source of the reflected quiver is traced by the reversed arrow it classifies.

                    source
                    @[instance_reducible]
                    noncomputable instance TauCeti.Quiver.Kronecker.instFintypeReflectPath {A : Type v} [Fintype A] (a b : Kronecker A) :
                    Fintype (Quiver.Path a b)
                    Equations
                    source
                    @[simp]
                    theorem TauCeti.Quiver.Kronecker.card_path_reflect_tgt_src {A : Type v} [Fintype A] :
                    Fintype.card (Quiver.Path tgt src) = Fintype.card A

                    The reflected quiver has as many paths from the target to the source as the generalized Kronecker quiver has arrows: by reflectPathEquivArrow, each such path is a single reversed arrow.