Documentation

TauCeti.LinearAlgebra.RootSystem.AffineDynkinType.Basic

Affine simply-laced Dynkin diagrams #

The simply-laced affine diagrams carry one node more than the corresponding finite simply-laced diagram. Throughout this file a name such as Aₙ or E₆ refers to the affine diagram, matching the constructors below.

This file introduces the diagrams as an enumeration TauCeti.AffineDynkinType, attaches to each its node count, its underlying SimpleGraph on Fin t.nodes, and its generalized Cartan matrix, and proves the two facts every consumer needs about a valid diagram, one whose parameter is in the range of the classification: it is connected, and its vector of marks is a null vector of the Cartan matrix, positive at every node and normalized to 1 at a distinguished one. The marks span the radical of the symmetrized form; only the null-vector half of that statement is proved here.

TauCeti.DynkinType has no affine constructors, and Mathlib's CartanMatrix family names no affine type either, with one exception: the generalized CartanMatrix.E n continues the E diagram past the finite range, and CartanMatrix.E 9 is the affine E₈ matrix under a different numbering, and it is what the affine E₈ matrix below is defined to be (TauCeti.AffineDynkinType.cartanMatrix_E8_eq_submatrix_cartanMatrix_E). Tau Ceti also already carries affine matrices as obstructions inside the finite-type classification: TauCeti.doubleForkCartanMatrix n is the affine Dₘ matrix for m = n + 5, and TauCeti.starCartanMatrix at ![2, 2, 2], ![1, 3, 3] and ![1, 2, 5] is the affine E₆, E₇ and E₈ matrix. Those live on the sum and sigma index types that make the classification argument uniform rather than on Fin, and their marks are rational and unnormalized -- TauCeti.starMark ![2, 2, 2] is 9 times the marks below -- so identifying them with the diagrams of this file is a relabelling problem of its own, of a piece with the Bourbaki relabelling that the roadmap asks for and that is not proved here either. This file is the affine complement, and it is deliberately graph first, because its consumers -- zigzag and preprojective algebras, and the McKay correspondence -- start from the diagram rather than from a root system.

Conventions #

Except for A₁, an affine simply-laced diagram is a simple graph, and its generalized Cartan matrix is 2I - A for the adjacency matrix A. The exception is genuine: A₁ has the multiplicity-two matrix !![2, -2; -2, 2], which is not 2I - A for any simple graph (TauCeti.AffineDynkinType.cartanMatrix_A_one_ne_two_smul_one_sub_adjMatrix). It is carved out by TauCeti.AffineDynkinType.IsGraphical, the predicate t ≠ A 1, which every statement reading an entry of the Cartan matrix off the graph assumes; the underlying graph of A₁ is still defined, as the single edge obtained by forgetting the multiplicity, but it does not determine the matrix. The statements that survive at A₁ -- the diagonal, the symmetry, the diagram of the matrix and the null vector -- carry no such hypothesis.

The node numberings are chosen so that every node other than 0 has a neighbour with a smaller number, which reduces connectedness to a single induction. Explicitly:

Main definitions #

Main results #

References #

This is the affine simply-laced family of Layer 0 of TauCetiRoadmap/ZigzagPreprojective/README.md; the E₈ numbering below is the one that roadmap's Suggested.lean fixes in affineE8ArmRel. See V. Kac, Infinite dimensional Lie algebras, 3rd ed., Chapter 4 and Table Aff 1, for the diagrams, their marks and the null root.

source
inductive TauCeti.AffineDynkinType :
Type

The simply-laced affine Dynkin diagrams: the families Aₙ and Dₙ, whose constructors accept every natural number, together with the three exceptional diagrams. The ranges on which these are the affine simply-laced diagrams of the classification are carried by TauCeti.AffineDynkinType.Valid, not by the constructors.

Instances For
    source
    def TauCeti.instDecidableEqAffineDynkinType.decEq (x✝ x✝¹ : AffineDynkinType) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance TauCeti.instDecidableEqAffineDynkinType :
      DecidableEq AffineDynkinType
      Equations
      source
      def TauCeti.AffineDynkinType.nodes :
      AffineDynkinType → ℕ

      The number of nodes of an affine simply-laced diagram, one more than the rank of the finite type it extends. This is exposed because it appears in the type of TauCeti.AffineDynkinType.graph, so even reading E6.graph as a graph on Fin 7 needs Fin E6.nodes to reduce.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.AffineDynkinType.nodes_A (n : ℕ) :
        (A n).nodes = n + 1
        source
        @[simp]
        theorem TauCeti.AffineDynkinType.nodes_D (n : ℕ) :
        (D n).nodes = n + 1
        source
        @[simp]
        theorem TauCeti.AffineDynkinType.nodes_E6 :
        E6.nodes = 7
        source
        @[simp]
        theorem TauCeti.AffineDynkinType.nodes_E7 :
        E7.nodes = 8
        source
        @[simp]
        theorem TauCeti.AffineDynkinType.nodes_E8 :
        E8.nodes = 9
        source
        theorem TauCeti.AffineDynkinType.nodes_pos (t : AffineDynkinType) :
        0 < t.nodes
        source
        instance TauCeti.AffineDynkinType.instNeZeroNatNodes (t : AffineDynkinType) :
        NeZero t.nodes
        source
        def TauCeti.AffineDynkinType.Valid :
        AffineDynkinType → Prop

        The ranges on which the affine simply-laced diagrams are pairwise distinct. Outside them the names are degenerate or repeat one another: A₀ names no diagram, while D₃ is A₃ and D₂ is A₁ × A₁.

        Equations
        Instances For
          source
          @[instance_reducible]
          instance TauCeti.AffineDynkinType.instDecidablePredValid :
          DecidablePred Valid
          Equations
          source
          @[simp]
          theorem TauCeti.AffineDynkinType.valid_A {n : ℕ} :
          (A n).Valid ↔ 1 ≤ n
          source
          @[simp]
          theorem TauCeti.AffineDynkinType.valid_D {n : ℕ} :
          (D n).Valid ↔ 4 ≤ n
          source
          @[simp]
          theorem TauCeti.AffineDynkinType.valid_E6 :
          E6.Valid
          source
          @[simp]
          theorem TauCeti.AffineDynkinType.valid_E7 :
          E7.Valid
          source
          @[simp]
          theorem TauCeti.AffineDynkinType.valid_E8 :
          E8.Valid
          source
          def TauCeti.AffineDynkinType.IsGraphical (t : AffineDynkinType) :
          Prop

          The affine simply-laced diagrams whose generalized Cartan matrix is 2I - A for the adjacency matrix A of the underlying simple graph, namely every diagram but A₁, whose two nodes carry a double edge and whose matrix is the multiplicity-two !![2, -2; -2, 2]; see TauCeti.AffineDynkinType.cartanMatrix_A_one_ne_two_smul_one_sub_adjMatrix. This is independent of TauCeti.AffineDynkinType.Valid: the formula holds at the degenerate diagrams too, and a statement that also needs those excluded assumes Valid separately.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance TauCeti.AffineDynkinType.instDecidablePredIsGraphical :
            DecidablePred IsGraphical
            Equations
            source
            theorem TauCeti.AffineDynkinType.isGraphical_iff_ne_A_one {t : AffineDynkinType} :
            t.IsGraphical ↔ t ≠ A 1

            Graphicality unfolded: TauCeti.AffineDynkinType.IsGraphical is a def into Prop, so a consumer outside this file needs this equation to read it.

            source
            @[simp]
            theorem TauCeti.AffineDynkinType.isGraphical_A {n : ℕ} :
            (A n).IsGraphical ↔ n ≠ 1
            source
            @[simp]
            theorem TauCeti.AffineDynkinType.isGraphical_D (n : ℕ) :
            (D n).IsGraphical
            source
            @[simp]
            theorem TauCeti.AffineDynkinType.isGraphical_E6 :
            E6.IsGraphical
            source
            @[simp]
            theorem TauCeti.AffineDynkinType.isGraphical_E7 :
            E7.IsGraphical
            source
            @[simp]
            theorem TauCeti.AffineDynkinType.isGraphical_E8 :
            E8.IsGraphical

            The underlying graphs #

            source
            def TauCeti.AffineDynkinType.graph (t : AffineDynkinType) :
            SimpleGraph (Fin t.nodes)

            The underlying simple graph of an affine simply-laced diagram, on the node set Fin t.nodes.

            Only A₁ is not determined by this graph: its generalized Cartan matrix has the off-diagonal entry -2, recording a double edge, and the graph below is the single edge left after forgetting that multiplicity. Every statement reading an entry of the Cartan matrix off the graph therefore assumes TauCeti.AffineDynkinType.IsGraphical.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.AffineDynkinType.graph_A (n : ℕ) :
              (A n).graph = SimpleGraph.cycleGraph (n + 1)
              source
              @[instance_reducible]
              instance TauCeti.AffineDynkinType.instDecidableRelFinNodesAdjGraph (t : AffineDynkinType) :
              DecidableRel t.graph.Adj
              Equations
              source
              theorem TauCeti.AffineDynkinType.graph_A_adj {n : ℕ} (hn : 1 ≤ n) (i j : Fin (A n).nodes) :
              (A n).graph.Adj i j ↔ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i ∨ ↑i = 0 ∧ ↑j = n ∨ ↑j = 0 ∧ ↑i = n

              Adjacency in the cycle Ãₙ, as a condition on node numbers: consecutive numbers, together with the edge joining the two ends 0 and n.

              source
              @[simp]
              theorem TauCeti.AffineDynkinType.graph_D_adj {n : ℕ} (hn : 4 ≤ n) {i j : Fin (n + 1)} :
              (D n).graph.Adj i j ↔ ↑i + 1 = ↑j ∧ ↑j ≤ n - 2 ∨ ↑j + 1 = ↑i ∧ ↑i ≤ n - 2 ∨ ↑i = 1 ∧ ↑j = n - 1 ∨ ↑j = 1 ∧ ↑i = n - 1 ∨ ↑i = n - 3 ∧ ↑j = n ∨ ↑j = n - 3 ∧ ↑i = n

              Adjacency in Dₙ, as a condition on node numbers: consecutive numbers along the path 0 - 1 - ⋯ - (n-2), the leaf n - 1 at node 1, and the leaf n at node n - 3, each in both orientations.

              source
              @[simp]
              theorem TauCeti.AffineDynkinType.graph_E6_adj (i j : Fin E6.nodes) :
              E6.graph.Adj i j ↔ (min ↑i ↑j, max ↑i ↑j) ∈ [(0, 1), (1, 2), (0, 3), (3, 4), (0, 5), (5, 6)]

              Adjacency in E₆ = T₃,₃,₃: the six edges, listed as the pairs of node numbers they join, smaller number first.

              source
              @[simp]
              theorem TauCeti.AffineDynkinType.graph_E7_adj (i j : Fin E7.nodes) :
              E7.graph.Adj i j ↔ (min ↑i ↑j, max ↑i ↑j) ∈ [(0, 1), (0, 2), (2, 3), (3, 4), (0, 5), (5, 6), (6, 7)]

              Adjacency in E₇ = T₂,₄,₄: the seven edges, listed as the pairs of node numbers they join, smaller number first.

              source
              @[simp]
              theorem TauCeti.AffineDynkinType.graph_E8_adj (i j : Fin E8.nodes) :
              E8.graph.Adj i j ↔ (min ↑i ↑j, max ↑i ↑j) ∈ [(0, 1), (0, 2), (2, 3), (0, 4), (4, 5), (5, 6), (6, 7), (7, 8)]

              Adjacency in E₈ = T₂,₃,₆: the eight edges, listed as the pairs of node numbers they join, smaller number first.

              Connectedness #

              source
              theorem TauCeti.AffineDynkinType.graph_connected {t : AffineDynkinType} (ht : t.Valid) :
              t.graph.Connected

              Every valid affine simply-laced diagram is connected. Validity is needed: the degenerate constructors outside TauCeti.AffineDynkinType.Valid, such as D 2, are disconnected.

              source
              theorem TauCeti.AffineDynkinType.exists_adj_graph {t : AffineDynkinType} (ht : t.Valid) (i : Fin t.nodes) :
              ∃ (j : Fin t.nodes), t.graph.Adj i j

              Every node of a valid affine simply-laced diagram has a neighbour: the diagram is connected and has at least two nodes.

              The generalized Cartan matrix #

              source
              def TauCeti.AffineDynkinType.cartanMatrix (t : AffineDynkinType) :
              Matrix (Fin t.nodes) (Fin t.nodes) ℤ

              The generalized Cartan matrix of an affine simply-laced diagram: 2I - A for the adjacency matrix A of the underlying graph, except at A₁, whose two nodes carry a double edge and whose matrix is !![2, -2; -2, 2]. E₈ is not spelled out either but taken from Mathlib, as the relabelling of the generalized CartanMatrix.E 9 that exchanges the two trivalent nodes; this is the same matrix, and TauCeti.AffineDynkinType.cartanMatrix_eq_graphCartanMatrix covers it like every other diagram.

              Instances For
                source
                @[simp]
                theorem TauCeti.AffineDynkinType.cartanMatrix_A_one :
                (A 1).cartanMatrix = !![2, -2; -2, 2]
                source
                @[simp]
                theorem TauCeti.AffineDynkinType.cartanMatrix_A_one_apply (i j : Fin (A 1).nodes) :
                (A 1).cartanMatrix i j = if i = j then 2 else -2

                The entries of the A₁ Cartan matrix: 2 on the diagonal, and the multiplicity-two -2 off it. Reading the matrix literal of TauCeti.AffineDynkinType.cartanMatrix_A_one entry by entry takes a fin_cases on both indices, and the body of TauCeti.AffineDynkinType.cartanMatrix is not exposed, so decide cannot do it outside this file.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_eq_graphCartanMatrix {t : AffineDynkinType} (ht : t.IsGraphical) :
                t.cartanMatrix = t.graph.graphCartanMatrix ℤ

                Away from A₁, the generalized Cartan matrix is the matrix 2I - A of the underlying graph, the degenerate diagrams outside TauCeti.AffineDynkinType.Valid included. This is what carries the general results about SimpleGraph.graphCartanMatrix over to the diagrams. At E₈ it is where Mathlib's numbering of CartanMatrix.E 9 is matched up with the numbering of this file.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_apply {t : AffineDynkinType} (ht : t.IsGraphical) (i j : Fin t.nodes) :
                t.cartanMatrix i j = if i = j then 2 else if t.graph.Adj i j then -1 else 0

                The entries of the generalized Cartan matrix away from A₁: 2 on the diagonal, -1 at an edge and 0 otherwise.

                source
                @[simp]
                theorem TauCeti.AffineDynkinType.cartanMatrix_apply_same (t : AffineDynkinType) (i : Fin t.nodes) :
                t.cartanMatrix i i = 2

                The diagonal entries of the generalized Cartan matrix are 2, A₁ included.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_apply_of_adj {t : AffineDynkinType} (ht : t.IsGraphical) {i j : Fin t.nodes} (h : t.graph.Adj i j) :
                t.cartanMatrix i j = -1

                Away from A₁, an edge of the diagram contributes the entry -1. At A₁ the single edge contributes -2.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_apply_of_not_adj {t : AffineDynkinType} {i j : Fin t.nodes} (hij : i ≠ j) (h : ¬t.graph.Adj i j) :
                t.cartanMatrix i j = 0

                Two distinct non-adjacent nodes contribute the entry 0.

                source
                theorem TauCeti.AffineDynkinType.isSymm_cartanMatrix (t : AffineDynkinType) :
                t.cartanMatrix.IsSymm

                The generalized Cartan matrix of an affine simply-laced diagram is symmetric, A₁ included: away from A₁ the matrix is 2I - A and an adjacency matrix is symmetric, while at A₁ the explicit multiplicity-two matrix !![2, -2; -2, 2] is symmetric outright.

                source
                theorem TauCeti.AffineDynkinType.graph_eq_diagramGraph_cartanMatrix (t : AffineDynkinType) :
                t.graph = diagramGraph t.cartanMatrix

                The graph of an affine simply-laced diagram is the diagram of its generalized Cartan matrix, A₁ included: the double edge there still shows up as a pair of nonzero entries. This is what carries the general results about TauCeti.diagramGraph over to graph.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_A_one_ne_two_smul_one_sub_adjMatrix (G : SimpleGraph (Fin (A 1).nodes)) [DecidableRel G.Adj] :
                (A 1).cartanMatrix ≠ 2 • 1 - SimpleGraph.adjMatrix ℤ G

                The A₁ Cartan matrix is not 2I minus a simple-graph adjacency matrix. Its off-diagonal entry is -2, while 2I - A has off-diagonal entries 0 and -1 for the adjacency matrix A of any simple graph. This is why every statement above reading an entry of cartanMatrix off graph assumes TauCeti.AffineDynkinType.IsGraphical.

                source
                theorem TauCeti.AffineDynkinType.cartanMatrix_E8_eq_submatrix_cartanMatrix_E :
                E8.cartanMatrix = (CartanMatrix.E 9).submatrix ⇑(Equiv.swap 0 3) ⇑(Equiv.swap 0 3)

                Affine E₈ is Mathlib's CartanMatrix.E 9, whose generalized E-family continues the E diagram past the finite range: this is how TauCeti.AffineDynkinType.cartanMatrix defines it. The relabelling is the transposition exchanging the trivalent node, numbered 0 here and 3 there; the arms of 1, 2 and 5 nodes then match up.

                The marks and the null vector #

                source
                def TauCeti.AffineDynkinType.marks (t : AffineDynkinType) :
                Fin t.nodes → ℤ

                The marks of an affine simply-laced diagram: a positive integer vector δ, normalized so that δ is 1 at TauCeti.AffineDynkinType.affineNode. For a valid type it is killed by the generalized Cartan matrix (TauCeti.AffineDynkinType.cartanMatrix_mulVec_marks_eq_zero), and for a valid type away from A₁ this is the local balance condition 2 δᵢ = ∑_{j ∼ i} δⱼ at every node.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.AffineDynkinType.marks_A_apply (n : ℕ) (i : Fin (A n).nodes) :
                  (A n).marks i = 1
                  source
                  @[simp]
                  theorem TauCeti.AffineDynkinType.marks_D_apply (n : ℕ) (i : Fin (D n).nodes) :
                  (D n).marks i = if 1 ≤ ↑i ∧ ↑i ≤ n - 3 then 2 else 1

                  The marks of Dₙ node by node: 2 on the interior of the path, 1 on the four leaves.

                  source
                  @[simp]
                  theorem TauCeti.AffineDynkinType.marks_E6 :
                  E6.marks = ![3, 2, 1, 2, 1, 2, 1]
                  source
                  @[simp]
                  theorem TauCeti.AffineDynkinType.marks_E7 :
                  E7.marks = ![4, 2, 3, 2, 1, 3, 2, 1]
                  source
                  @[simp]
                  theorem TauCeti.AffineDynkinType.marks_E8 :
                  E8.marks = ![6, 3, 4, 2, 5, 4, 3, 2, 1]
                  source
                  def TauCeti.AffineDynkinType.affineNode (t : AffineDynkinType) :
                  Fin t.nodes

                  The affine node of an affine simply-laced diagram: the distinguished node at which the marks are normalized to 1 (TauCeti.AffineDynkinType.marks_affineNode).

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.affineNode_A (n : ℕ) :
                    (A n).affineNode = 0
                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.affineNode_D (n : ℕ) :
                    (D n).affineNode = 0
                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.affineNode_E6 :
                    E6.affineNode = 2
                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.affineNode_E7 :
                    E7.affineNode = 4
                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.affineNode_E8 :
                    E8.affineNode = 8
                    source
                    theorem TauCeti.AffineDynkinType.marks_pos {t : AffineDynkinType} (i : Fin t.nodes) :
                    0 < t.marks i

                    Every mark is positive.

                    source
                    @[simp]
                    theorem TauCeti.AffineDynkinType.marks_affineNode (t : AffineDynkinType) :
                    t.marks t.affineNode = 1

                    The marks are normalized to be 1 at the affine node.

                    The local balance condition #

                    source
                    theorem TauCeti.AffineDynkinType.sum_marks_neighborFinset_eq_two_mul {t : AffineDynkinType} (ht : t.Valid) (hg : t.IsGraphical) (i : Fin t.nodes) :
                    ∑ j ∈ t.graph.neighborFinset i, t.marks j = 2 * t.marks i

                    The marks satisfy the local balance condition: at every valid diagram other than A₁, twice the mark of a node is the sum of the marks of its neighbours. Validity is needed as well as graphicality here: at the degenerate A₀ the single node has no neighbour at all, while its mark is 1.

                    source
                    theorem TauCeti.AffineDynkinType.cartanMatrix_mulVec_marks_eq_zero {t : AffineDynkinType} (ht : t.Valid) :
                    t.cartanMatrix.mulVec t.marks = 0

                    The marks are a null vector of the generalized Cartan matrix: Cδ = 0. Together with TauCeti.AffineDynkinType.marks_pos and TauCeti.AffineDynkinType.marks_affineNode this exhibits the radical direction of an affine simply-laced diagram, normalized at the affine node.