The simply connected root datum of type Aₙ

This file constructs, uniformly in the rank n, the pinned integral root datum of type Aₙ on the character and cocharacter lattices Fin n → ℤ. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis, so the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix CartanMatrix.A n and the i-th simple coroot is the i-th standard basis vector.

The coordinates

Write e₀, …, e_n for the standard basis of the classical model ℤ ^ (n + 1), in which the roots of type Aₙ are the n * (n + 1) vectors e_a - e_b with a ≠ b and the simple roots are αᵢ = eᵢ - eᵢ₊₁. Everything below is the image of that model in the two pinned lattices: a vector of the character lattice is recorded by its pairings against the simple coroots, and a vector of the cocharacter lattice by its coordinates in the simple coroots. Although e_a itself does not lie in the coroot lattice, choose a coordinate potential for it so that differences represent coroots:

typeAWeight n a   = (⟨e_a, αₖ^∨⟩)ₖ           = ([a = k] - [a = k + 1])ₖ,
typeACoweight n a = (chosen potential at αₖ^∨)ₖ   = ([a ≤ k])ₖ.

For a ≤ b, the difference of the chosen potentials has the simple-coroot coordinates of e_a - e_b = ∑ a ≤ k < b, αₖ^∨. The root e_a - e_b and its coroot are the corresponding differences, and the whole construction is a finite calculation with these two families; typeAWeight_dotProduct_typeACoweight is the one identity it rests on.

The roots are indexed by Fin (n * (n + 1)), the ordered pairs (a, b) of distinct elements of Fin (n + 1) being enumerated by the difference b - a ≠ 0 first and the source a second. The first n indices are therefore the simple roots α₀, …, α_{n-1} in Bourbaki order, as root_typeASimpleIndex records.

Only the coroots are asked to span their lattice, and only that half is recorded, in corootSpan_typeASimplyConnectedRootDatum_eq_top. The roots span the root lattice, which sits inside the weight lattice with index n + 1 (Bourbaki, Plate I), so the datum is a RootDatum carrying no RootPairing.IsRootSystem instance. That asymmetry is what "simply connected" means here.

The graph automorphism

The Aₙ diagram is a chain, so reversing it is a symmetry, and the last part of this file realizes that symmetry on the pinned datum itself rather than only on the Cartan matrix. On the classical model the realization is e_a ↦ -e_{rev a}, whose effect on a root is

e_a - e_b ↦ e_{rev b} - e_{rev a},

and on both pinned lattices, whose coordinates are indexed by the simple nodes, it is the reversal of coordinates. So a single linear automorphism of Fin n → ℤ serves as both the character and the cocharacter map, and TauCeti.DynkinType.typeAGraphAut bundles it with the induced permutation of the n * (n + 1) root indices as an element of RootPairing.Aut. It restricts to the reversal Fin.revPerm on the Bourbaki-numbered simple roots, which is TauCeti.graphPermA n, the permutation that TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean pins for the ²Aₙ family; that module is deliberately not imported here, since only the Fin-level reversal is used.

The sign in e_a ↦ -e_{rev a} is forced: e_a ↦ e_{rev a} sends αᵢ = e_i - e_{i+1} to e_{rev i} - e_{rev (i + 1)} = -α_{rev i}, a negative root, so it does not preserve the base. The composite with the opposition -1 is the automorphism below. This is unrelated to TauCeti.opposition, which is built from the longest Weyl element and needs the root-system hypotheses this simply connected datum does not carry.

Main definitions

• TauCeti.DynkinType.typeASimplyConnectedRootDatum: the pinned root datum of type Aₙ.
• TauCeti.DynkinType.TypeAIndex and TauCeti.DynkinType.typeAIndexEquiv: the ordered pairs (a, b) of distinct classical indices, and their pinned enumeration as root indices.
• TauCeti.DynkinType.typeASimpleIndex: the first n root indices, the Bourbaki-numbered simple roots.
• TauCeti.DynkinType.typeASimplyConnectedBase: the base they form.
• TauCeti.DynkinType.typeAGraphAut: the graph automorphism of the pinned datum.

Main results

• TauCeti.DynkinType.root_typeAIndexEquiv, TauCeti.DynkinType.coroot_typeAIndexEquiv, TauCeti.DynkinType.pairing_typeAIndexEquiv and TauCeti.DynkinType.typeAIndexEquiv_symm_reflectionPerm: the root and coroot e_a - e_b in coordinates, the Cartan integers, and the reflections as transpositions, all read on ordered pairs.
• TauCeti.DynkinType.root_typeASimpleIndex and TauCeti.DynkinType.coroot_typeASimpleIndex: the i-th simple root is the i-th row of CartanMatrix.A n and the i-th simple coroot is Pi.single i 1, which is what pins the two lattices as the weight and coroot lattices.
• TauCeti.DynkinType.hasCartanType_typeASimplyConnectedRootDatum: the pinned base has Cartan type A n.
• TauCeti.DynkinType.corootSpan_typeASimplyConnectedRootDatum_eq_top: the coroots span the cocharacter lattice, the simply connected condition.
• TauCeti.DynkinType.ncard_posRoots_typeASimplyConnectedRootDatum: the number of positive roots is (n + 1).choose 2, for any base.
• TauCeti.DynkinType.weightMap_typeAGraphAut_apply and TauCeti.DynkinType.coweightMap_typeAGraphAut_apply: the graph automorphism reverses the coordinates of both lattices.
• TauCeti.DynkinType.indexEquiv_typeAGraphAut_typeASimpleIndex: on the Bourbaki-numbered simple roots it is the chain reversal.
• TauCeti.DynkinType.typeAGraphAut_sq and TauCeti.DynkinType.typeAGraphAut_ne_one: it is an involution, and is nontrivial as soon as the chain has two nodes.
• TauCeti.DynkinType.support_map_typeASimplyConnectedBase_typeAGraphAut: it preserves the pinned base.

References

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate I, and Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1. This is the Aₙ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The positive-root count is the corresponding clause of the Aₙ worked example in the "Worked examples (acceptance criteria)" section of that README; it agrees with the count in Bourbaki, Plate I.

The graph automorphism is the root-datum input to the isomorphism theorem for pinned groups in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is the graph-twisted Steinberg map of milestone L1 of TauCetiRoadmap/CFSGStatement/README.md. The description of the type-A diagram automorphism as X ↦ -J Xᵀ J on sl_{n+1}, of which the map below is the root-datum shadow, is in R. W. Carter, Simple Groups of Lie Type, §12.2.

The two coordinate families

The roots and coroots indexed by ordered pairs

@[reducible, inline]

abbrev TauCeti.DynkinType.TypeAIndex (n : ℕ) : Type

The ordered pairs of distinct elements of Fin (n + 1), indexing the roots e_a - e_b of type Aₙ before they are enumerated by Fin (n * (n + 1)).

Equations

• TauCeti.DynkinType.TypeAIndex n = { p : Fin (n + 1) × Fin (n + 1) // p.1 ≠ p.2 }

The Bourbaki enumeration of the roots

def TauCeti.DynkinType.typeAIndexEquiv (n : ℕ) : TypeAIndex n ≃ Fin (n * (n + 1))

The pinned enumeration of the roots of type Aₙ by Fin (n * (n + 1)): by the difference b - a ≠ 0 first and the source a second (finDistinctPairsEquiv), which puts the simple roots at the first n indices.

Equations

• TauCeti.DynkinType.typeAIndexEquiv n = (TauCeti.finDistinctPairsEquiv (n + 1)).trans finProdFinEquiv

def TauCeti.DynkinType.typeASimplyConnectedRootDatum (n : ℕ) : RootDatum (Fin (n * (n + 1))) (Fin n → ℤ) (Fin n → ℤ)

The pinned simply connected root datum of type Aₙ.

Both lattices are Fin n → ℤ: the character lattice in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. The n * (n + 1) roots are the classical e_a - e_b with a ≠ b, enumerated with the simple roots first; see TauCeti.DynkinType.root_typeASimpleIndex.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.toLinearMap_typeASimplyConnectedRootDatum {n : ℕ} (x y : Fin n → ℤ) : ((typeASimplyConnectedRootDatum n).toLinearMap x) y = x ⬝ᵥ y

The pinned pairing of type Aₙ is the dot product of the two lattices.

@[simp]

theorem TauCeti.DynkinType.root_typeAIndexEquiv {n : ℕ} (p : TypeAIndex n) (k : Fin n) : (typeASimplyConnectedRootDatum n).root ((typeAIndexEquiv n) p) k = ((if (↑p).1 = k.castSucc then 1 else 0) - if (↑p).1 = k.succ then 1 else 0) - ((if (↑p).2 = k.castSucc then 1 else 0) - if (↑p).2 = k.succ then 1 else 0)

The root indexed by the ordered pair (a, b) is e_a - e_b. In the fundamental-weight coordinates, e_c has k-th entry ⟨e_c, αₖ^∨⟩ = [c = k] - [c = k + 1].

@[simp]

theorem TauCeti.DynkinType.coroot_typeAIndexEquiv {n : ℕ} (p : TypeAIndex n) (k : Fin n) : (typeASimplyConnectedRootDatum n).coroot ((typeAIndexEquiv n) p) k = (if (↑p).1 ≤ k.castSucc then 1 else 0) - if (↑p).2 ≤ k.castSucc then 1 else 0

The coroot indexed by the ordered pair (a, b) is e_a - e_b. In the simple-coroot coordinates, e_a - e_b has k-th entry [a ≤ k] - [b ≤ k].

theorem TauCeti.DynkinType.pairing_typeASimplyConnectedRootDatum_comm {n : ℕ} (k l : Fin (n * (n + 1))) : RootPairing.pairing (typeASimplyConnectedRootDatum n) k l = RootPairing.pairing (typeASimplyConnectedRootDatum n) l k

The root--coroot pairing of the pinned type A datum is symmetric.

@[simp]

theorem TauCeti.DynkinType.pairing_typeAIndexEquiv {n : ℕ} (p q : TypeAIndex n) : RootPairing.pairing (typeASimplyConnectedRootDatum n) ((typeAIndexEquiv n) p) ((typeAIndexEquiv n) q) = ((if (↑p).1 = (↑q).1 then 1 else 0) - if (↑p).1 = (↑q).2 then 1 else 0) - ((if (↑p).2 = (↑q).1 then 1 else 0) - if (↑p).2 = (↑q).2 then 1 else 0)

The Cartan integers of type Aₙ on ordered pairs. The pairing of e_a - e_b with the coroot e_c - e_d is [a = c] - [a = d] - ([b = c] - [b = d]).

theorem TauCeti.DynkinType.typeAIndexEquiv_symm_reflectionPerm {n : ℕ} (p q : TypeAIndex n) : ↑((typeAIndexEquiv n).symm (((typeASimplyConnectedRootDatum n).reflectionPerm ((typeAIndexEquiv n) p)) ((typeAIndexEquiv n) q))) = ((Equiv.swap (↑p).1 (↑p).2) (↑q).1, (Equiv.swap (↑p).1 (↑p).2) (↑q).2)

Reflections of type Aₙ transpose the entries of ordered pairs. The reflection in e_a - e_b sends the root e_c - e_d to e_{s c} - e_{s d}, where s is the transposition of a and b.

def TauCeti.DynkinType.typeASimpleIndex (n : ℕ) (i : Fin n) : Fin (n * (n + 1))

The i-th simple root of type Aₙ sits at root index i, the Bourbaki node i + 1.

Equations

• TauCeti.DynkinType.typeASimpleIndex n i = Fin.castLE ⋯ i

@[simp]

theorem TauCeti.DynkinType.typeASimpleIndex_val {n : ℕ} (i : Fin n) : ↑(typeASimpleIndex n i) = ↑i

theorem TauCeti.DynkinType.typeASimpleIndex_injective {n : ℕ} : Function.Injective (typeASimpleIndex n)

@[simp]

theorem TauCeti.DynkinType.typeAIndexEquiv_symm_typeASimpleIndex {n : ℕ} (i : Fin n) : (typeAIndexEquiv n).symm (typeASimpleIndex n i) = ⟨(⟨↑i, ⋯⟩, ⟨↑i + 1, ⋯⟩), ⋯⟩

The Bourbaki simple index corresponds to the consecutive pair of matrix indices.

@[simp]

theorem TauCeti.DynkinType.root_typeASimpleIndex {n : ℕ} (i : Fin n) : (typeASimplyConnectedRootDatum n).root (typeASimpleIndex n i) = fun (k : Fin n) => CartanMatrix.A n i k

The simple roots are the rows of the Cartan matrix. In the fundamental-weight basis the i-th simple root of the pinned type Aₙ datum is the i-th row of CartanMatrix.A n, which is what pins the character lattice as the weight lattice.

@[simp]

theorem TauCeti.DynkinType.coroot_typeASimpleIndex {n : ℕ} (i : Fin n) : (typeASimplyConnectedRootDatum n).coroot (typeASimpleIndex n i) = Pi.single i 1

The simple coroots are the standard basis. This is what pins the cocharacter lattice as the coroot lattice, so that the datum is the simply connected one.

The pinned base

def TauCeti.DynkinType.typeASimplyConnectedBase (n : ℕ) : RootPairing.Base (typeASimplyConnectedRootDatum n)

The Bourbaki-numbered base of the pinned simply connected root datum of type Aₙ. Its support is the set of the first n root indices, carrying the simple roots in Bourbaki order.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.mem_typeASimplyConnectedBase_support {n : ℕ} {k : Fin (n * (n + 1))} : k ∈ (typeASimplyConnectedBase n).support ↔ ↑k < n

Membership in the pinned base support is exactly membership among the first n root indices.

theorem TauCeti.DynkinType.hasCartanType_typeASimplyConnectedRootDatum (n : ℕ) : HasCartanType (typeASimplyConnectedRootDatum n) (typeASimplyConnectedBase n) (A n)

The pinned datum of type Aₙ has Cartan type A n. Its Bourbaki-numbered base realizes the standard Cartan matrix CartanMatrix.A n, with the node numbering of TauCeti.DynkinType.

theorem TauCeti.DynkinType.corootSpan_typeASimplyConnectedRootDatum_eq_top (n : ℕ) : RootPairing.corootSpan (typeASimplyConnectedRootDatum n) ℤ = ⊤

The coroots of the pinned type Aₙ datum span the cocharacter lattice. This is the simply connected lattice condition required by the pinned Chevalley--Demazure construction. Its counterpart for the roots is deliberately absent: they span the root lattice, which sits inside the weight lattice with index n + 1 (Bourbaki, Plate I).

@[simp]

theorem TauCeti.DynkinType.ncard_posRoots_typeASimplyConnectedRootDatum (n : ℕ) (b : RootPairing.Base (typeASimplyConnectedRootDatum n)) : (posRoots (typeASimplyConnectedRootDatum n) b).ncard = (n + 1).choose 2

The pinned root datum of type Aₙ has (n + 1).choose 2 positive roots. Exactly half of its n * (n + 1) roots are positive, for any base.

The graph automorphism

def TauCeti.DynkinType.typeAGraphAut (n : ℕ) : RootPairing.Aut (typeASimplyConnectedRootDatum n)

The graph automorphism of the pinned simply connected root datum of type Aₙ. It reverses the coordinates of the character and cocharacter lattices, which on the classical model is e_a ↦ -e_{rev a}, and permutes the roots accordingly. It is the root-datum shadow of the diagram automorphism of sl_{n + 1}, and the Fin-level datum a pinned group automorphism of the ²Aₙ family is built from.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.weightMap_typeAGraphAut_apply {n : ℕ} (x : Fin n → ℤ) (k : Fin n) : (↑(typeAGraphAut n)).weightMap x k = x k.rev

The graph automorphism reverses the fundamental-weight coordinates of a character.

@[simp]

theorem TauCeti.DynkinType.coweightMap_typeAGraphAut_apply {n : ℕ} (x : Fin n → ℤ) (k : Fin n) : (↑(typeAGraphAut n)).coweightMap x k = x k.rev

The graph automorphism reverses the simple-coroot coordinates of a cocharacter.

@[simp]

theorem TauCeti.DynkinType.indexEquiv_typeAGraphAut_typeASimpleIndex {n : ℕ} (i : Fin n) : (↑(typeAGraphAut n)).indexEquiv (typeASimpleIndex n i) = typeASimpleIndex n i.rev

The graph automorphism reverses the Bourbaki-numbered chain. On the first n root indices, the simple roots in Bourbaki order, the induced permutation is Fin.revPerm, which is TauCeti.graphPermA n.

@[simp]

theorem TauCeti.DynkinType.typeAGraphAut_sq (n : ℕ) : typeAGraphAut n ^ 2 = 1

The type Aₙ graph automorphism is an involution. It is the automorphism attached to the order-two symmetry of the Aₙ diagram, so a Steinberg endomorphism of the ²Aₙ family built from it composes with the field Frobenius to something whose square is an ordinary Frobenius.

theorem TauCeti.DynkinType.typeAGraphAut_ne_one {n : ℕ} (hn : 2 ≤ n) : typeAGraphAut n ≠ 1

The type Aₙ graph automorphism is nontrivial once the chain has two nodes. The bound is the one carried by TauCeti.graphPermA_ne_one: on fewer nodes the reversal of Fin n is the identity, and there is nothing to prove nontrivial.

@[simp]

theorem TauCeti.DynkinType.support_map_typeASimplyConnectedBase_typeAGraphAut (n : ℕ) : Finset.image (⇑(↑(typeAGraphAut n)).indexEquiv) (typeASimplyConnectedBase n).support = (typeASimplyConnectedBase n).support

The graph automorphism preserves the pinned base. Its permutation of root indices maps the first n indices onto themselves, so the automorphism is a symmetry of the pinning and not merely of the root system.