Documentation

TauCeti.RepresentationTheory.Quiver.AffineE8.Basic

The extended Dynkin quiver of type E₈~ #

TauCeti.Quiver.AffineE8 is the star with arms of lengths one, two and five, with all arrows pointing towards the centre. Representations with injective arrows are configurations of a subspace, a two-step flag and a five-step flag in the centre space. This is the extended Dynkin diagram T₂,₃,₆; its infinite representation type is proved in TauCeti.RepresentationTheory.Quiver.AffineE8.FiniteRepType. The underlying graph 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.

References #

source
inductive TauCeti.Quiver.AffineE8 :
Type

The inward orientation of the extended Dynkin diagram E₈~. The subscripts on the long and medium arms record the coefficients of the minimal imaginary root.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.Quiver.instDecidableEqAffineE8 :
    DecidableEq AffineE8
    source
    @[instance_reducible]
    instance TauCeti.Quiver.AffineE8.instFintype :
    Fintype AffineE8
    source
    inductive TauCeti.Quiver.AffineE8.Arrow :
    AffineE8 → AffineE8 → Type

    The eight arrows, directed towards the centre along the three arms.

    Instances For
      source
      def TauCeti.Quiver.AffineE8.instDecidableEqArrow.decEq {a✝ a✝¹ : AffineE8} (x✝ x✝¹ : a✝.Arrow a✝¹) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance TauCeti.Quiver.AffineE8.instDecidableEqArrow {a✝ a✝¹ : AffineE8} :
        DecidableEq (a✝.Arrow a✝¹)
        source
        @[instance_reducible]
        instance TauCeti.Quiver.AffineE8.instQuiver :
        Quiver AffineE8
        source
        instance TauCeti.Quiver.AffineE8.instSubsingletonHom (a b : AffineE8) :
        Subsingleton (a ⟶ b)

        There is at most one arrow between any two vertices.

        source
        @[instance_reducible]
        noncomputable instance TauCeti.Quiver.AffineE8.instFintypeHom (a b : AffineE8) :
        Fintype (a ⟶ b)
        source
        @[reducible, inline]
        abbrev TauCeti.Quiver.AffineE8.coordinateCount :
        AffineE8 → ℕ

        The minimal imaginary-root multiplicities, used as the numbers of coordinates in the flag construction.

        Instances For
          source
          @[simp]
          theorem TauCeti.Quiver.AffineE8.card_eq :
          Fintype.card AffineE8 = 9

          The extended diagram has nine vertices.

          The underlying graph #

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

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

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

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