Documentation

TauCeti.RepresentationTheory.Quiver.AffineE6.Basic

The extended Dynkin quiver of type E₆~ #

The quiver TauCeti.Quiver.AffineE6 has a centre and three arms of two vertices each: for i : Fin 3 an outer vertex outer i with one arrow into the inner vertex inner i, which has one arrow into the centre. Its underlying graph is the extended Dynkin diagram E₆~, the star with three arms of length two, on seven vertices, here with every arrow pointing towards the centre. On the root-system side this is the star TauCeti.starCartanMatrix ![2, 2, 2], whose Cartan matrix is not of finite type (TauCeti.not_isFiniteType_affineE₆).

This file carries the vertex and arrow data, and the shape of the underlying graph: it is a tree, with at most one arrow between any two vertices, because every vertex is the source of at most one arrow and every arrow points towards the centre. The representation theory, that the quiver has infinite representation type, is in TauCeti.RepresentationTheory.Quiver.AffineE6.FiniteRepType.

Main definitions #

References #

source
inductive TauCeti.Quiver.AffineE6 :
Type

The extended Dynkin quiver E₆~: a centre and three arms, each an outer vertex with an arrow into an inner vertex, which has an arrow into the centre.

  • center : AffineE6

    The centre, the head of the three inner arrows.

  • inner (i : Fin 3) : AffineE6

    The inner vertex of the arm indexed by i, adjacent to the centre.

  • outer (i : Fin 3) : AffineE6

    The outer vertex of the arm indexed by i, the tail of a single arrow.

Instances For
    source
    def TauCeti.Quiver.instDecidableEqAffineE6.decEq (x✝ x✝¹ : AffineE6) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance TauCeti.Quiver.instDecidableEqAffineE6 :
      DecidableEq AffineE6

      The seven vertices #

      source
      def TauCeti.Quiver.AffineE6.vertexEquiv :
      AffineE6 ≃ Unit ⊕ Fin 3 ⊕ Fin 3

      The vertices of TauCeti.Quiver.AffineE6 as Unit ⊕ Fin 3 ⊕ Fin 3: the centre, then the inner vertices, then the outer vertices.

      Instances For
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_center :
        vertexEquiv center = Sum.inl ()
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_inner (i : Fin 3) :
        vertexEquiv (inner i) = Sum.inr (Sum.inl i)
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_outer (i : Fin 3) :
        vertexEquiv (outer i) = Sum.inr (Sum.inr i)
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_symm_inl (u : Unit) :
        vertexEquiv.symm (Sum.inl u) = center
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_symm_inr_inl (i : Fin 3) :
        vertexEquiv.symm (Sum.inr (Sum.inl i)) = inner i
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.vertexEquiv_symm_inr_inr (i : Fin 3) :
        vertexEquiv.symm (Sum.inr (Sum.inr i)) = outer i
        source
        @[instance_reducible]
        instance TauCeti.Quiver.AffineE6.instFintype :
        Fintype AffineE6
        source
        @[simp]
        theorem TauCeti.Quiver.AffineE6.card_eq :
        Fintype.card AffineE6 = 7

        TauCeti.Quiver.AffineE6 has seven vertices, as the extended Dynkin diagram E₆~ should.

        The arrows #

        source
        @[instance_reducible]
        instance TauCeti.Quiver.AffineE6.instQuiver :
        Quiver AffineE6
        source
        def TauCeti.Quiver.AffineE6.outerArrow (i : Fin 3) :
        outer i ⟶ inner i

        The arrow from the outer vertex of the arm indexed by i to the inner vertex of that arm.

        Instances For
          source
          def TauCeti.Quiver.AffineE6.innerArrow (i : Fin 3) :
          inner i ⟶ center

          The arrow from the inner vertex of the arm indexed by i into the centre.

          Instances For
            source
            @[instance_reducible]
            instance TauCeti.Quiver.AffineE6.instUniqueHomInnerCenter (i : Fin 3) :
            Unique (inner i ⟶ center)
            source
            instance TauCeti.Quiver.AffineE6.instIsEmptyHomCenter (v : AffineE6) :
            IsEmpty (center ⟶ v)

            No arrow leaves the centre.

            source
            instance TauCeti.Quiver.AffineE6.instIsEmptyHomInner (i j : Fin 3) :
            IsEmpty (inner i ⟶ inner j)
            source
            instance TauCeti.Quiver.AffineE6.instIsEmptyHomInnerOuter (i j : Fin 3) :
            IsEmpty (inner i ⟶ outer j)
            source
            instance TauCeti.Quiver.AffineE6.instIsEmptyHomOuterCenter (i : Fin 3) :
            IsEmpty (outer i ⟶ center)
            source
            instance TauCeti.Quiver.AffineE6.instIsEmptyHomOuter (i j : Fin 3) :
            IsEmpty (outer i ⟶ outer j)
            source
            instance TauCeti.Quiver.AffineE6.instSubsingletonHom (a b : AffineE6) :
            Subsingleton (a ⟶ b)

            Between any two vertices of TauCeti.Quiver.AffineE6 there is at most one arrow.

            The underlying graph #

            source
            theorem TauCeti.Quiver.AffineE6.isAcyclic_underlyingGraph :
            (underlyingGraph AffineE6).IsAcyclic

            The underlying graph of TauCeti.Quiver.AffineE6 is acyclic, so it is the tree E₆~.

            source
            theorem TauCeti.Quiver.AffineE6.subsingleton_hom_sum (a b : AffineE6) :
            Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))

            Two vertices of TauCeti.Quiver.AffineE6 are joined by at most one arrow, counted in both directions.