Documentation

TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.RootDatum

The type A carrier is pinned by its named root datum #

TauCeti.SlStd.groupScheme is the full-weight Chevalley carrier of type A_r: the closed subgroup scheme of GL_{r+1} over ℤ generated by the divided-power exponential root subgroups of the Bourbaki-numbered Chevalley generators of sl_{r+1} together with the weight torus of the standard lattice. Its pinning data — the numbered root subgroups and the split torus — are so far described by the rows of CartanMatrix.A r, which is a table rather than a root datum.

This file replaces that table by the pinned datum itself. TauCeti.typeASimplyConnectedRootDatum r is the simply connected root datum of type A_r, written on the character and cocharacter lattices Fin r → ℤ, which are the lattices the carrier's split torus SplitTorus.groupScheme ℤ (Fin r) is built on. The results below say that the root of the i-th numbered raising subgroup is the i-th simple root of that datum, that the lowering subgroup sits at its negative, and that the pinning equation t(s) x_i(u) t(s)⁻¹ = α_i(s) u is therefore an equation about the named simple root rather than about a matrix entry. The same statements are given against TauCeti.DynkinType.simplyConnectedRootDatum, the uniform dispatcher a consumer reaches through a Dynkin type; the two differ only in how the datum is named, and the dispatcher form carries the validity hypothesis that naming it needs.

The last result is about the graph automorphism. TauCeti.SlStd.graphAutomorphism permutes the numbered root subgroups by TauCeti.SlStd.graphRootPerm, the reversal on each of the raising and lowering families, while TauCeti.typeAGraphAut r is the automorphism of the pinned datum that reverses the fundamental-weight coordinates. TauCeti.SlStd.rootGeneratorWeight_graphRootPerm says these two agree: the subgroup the carrier's graph automorphism moves x_k to is the one whose root is the image of the root of x_k under the datum's graph automorphism. That is what makes the carrier automorphism the one attached to the diagram symmetry, rather than an unrelated automorphism that happens to reverse an index.

Nothing here asserts that the carrier is reductive, that its torus is maximal, or that it is isomorphic to the special linear group scheme, and no group below is claimed to be finite or simple.

Main results #

References #

This advances the "Pinnings" and "Root subgroup maps" targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, the second of which asks for "the equations pinning them against the pinning" and adds that downstream work states its conventions against those equations, so that they are part of the interface. Nothing below is the separate "isomorphism theorem for pinned groups", which asserts a uniqueness this file does not prove. Its consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, which requires each carrier to be traceable to DynkinType.simplyConnectedRootDatum reached through ValidLieTypeIndex.dynkinType, and milestone L1, whose graph-twisted branches take γ to be the automorphism attached to the numbered diagram permutation.

The numbered root subgroups sit at the pinned simple roots #

None of the identifications below is a simp lemma. Both sides are already simp-normal: the carrier's TauCeti.SlStd.rootGeneratorWeight_inl and the datum's TauCeti.root_typeASimpleIndex both rewrite to entries of CartanMatrix.A r, and orienting the identification either way would undo one of them.

source
theorem TauCeti.SlStd.rootGeneratorWeight_inl_eq_root_typeASimpleIndex (r : ℕ) (i : Fin r) :
rootGeneratorWeight r (Sum.inl i) = (DynkinType.typeASimplyConnectedRootDatum r).root (DynkinType.typeASimpleIndex r i)

The i-th numbered raising subgroup sits at the i-th pinned simple root. The root character by which the split torus of the type A_r carrier rescales the parameter of the raising subgroup at i is the i-th simple root of TauCeti.typeASimplyConnectedRootDatum r.

source
theorem TauCeti.SlStd.rootGeneratorWeight_inr_eq_neg_root_typeASimpleIndex (r : ℕ) (i : Fin r) :
rootGeneratorWeight r (Sum.inr i) = -(DynkinType.typeASimplyConnectedRootDatum r).root (DynkinType.typeASimpleIndex r i)

The i-th numbered lowering subgroup sits at the negative of the i-th pinned simple root.

source
theorem TauCeti.SlStd.rootGeneratorWeight_inl_eq_root_simpleIndex (r : ℕ) (ht : (DynkinType.A r).Valid) (i : Fin r) :
rootGeneratorWeight r (Sum.inl i) = ((DynkinType.A r).simplyConnectedRootDatum ht).root ((DynkinType.A r).simpleIndex ht i)

The i-th numbered raising subgroup sits at the i-th simple root of the pinned datum of its Dynkin type. This is the form in which the milestone that builds ambient groups from a Dynkin type reads the pinning; TauCeti.SlStd.rootGeneratorWeight_inl_eq_root_typeASimpleIndex is the same statement with the datum named directly, and needs no validity hypothesis.

source
theorem TauCeti.SlStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex (r : ℕ) (ht : (DynkinType.A r).Valid) (i : Fin r) :
rootGeneratorWeight r (Sum.inr i) = -((DynkinType.A r).simplyConnectedRootDatum ht).root ((DynkinType.A r).simpleIndex ht i)

The i-th numbered lowering subgroup sits at the negative of the i-th simple root of the pinned datum of its Dynkin type.

The pinning equation against the named simple roots #

source
theorem TauCeti.SlStd.torusPoints_conj_rootSubgroupParam_root_simpleIndex (r : ℕ) (ht : (DynkinType.A r).Valid) (i : Fin r) (B : CommAlgCat ℤ) (s : Fin r → (↑B)ˣ) (u : Multiplicative ↑B) :
(torusPoints r B) s * (rootSubgroupParam r (Sum.inl i) B) u * ((torusPoints r B) s)⁻¹ = (rootSubgroupParam r (Sum.inl i) B) (Multiplicative.ofAdd (↑(torusCharacter s (((DynkinType.A r).simplyConnectedRootDatum ht).root ((DynkinType.A r).simpleIndex ht i))) * Multiplicative.toAdd u))

The pinning equation of the type A_r carrier, at a named simple root. A split-torus point s conjugates the raising subgroup element of parameter u at the numbered index i into the one of parameter α_i(s) u, where α_i is the i-th simple root of the pinned simply connected root datum of the Dynkin type A r.

source
theorem TauCeti.SlStd.torusPoints_conj_rootSubgroupParam_neg_root_simpleIndex (r : ℕ) (ht : (DynkinType.A r).Valid) (i : Fin r) (B : CommAlgCat ℤ) (s : Fin r → (↑B)ˣ) (u : Multiplicative ↑B) :
(torusPoints r B) s * (rootSubgroupParam r (Sum.inr i) B) u * ((torusPoints r B) s)⁻¹ = (rootSubgroupParam r (Sum.inr i) B) (Multiplicative.ofAdd (↑(torusCharacter s (-((DynkinType.A r).simplyConnectedRootDatum ht).root ((DynkinType.A r).simpleIndex ht i))) * Multiplicative.toAdd u))

The pinning equation of the type A_r carrier, at the negative of a named simple root.

The graph automorphism realizes the one of the pinned datum #

source
theorem TauCeti.SlStd.rootGeneratorWeight_graphRootPerm (r : ℕ) (k : Fin r ⊕ Fin r) :
rootGeneratorWeight r ((graphRootPerm r) k) = (↑(DynkinType.typeAGraphAut r)).weightMap (rootGeneratorWeight r k)

The carrier's graph automorphism realizes the graph automorphism of its pinned root datum. The numbered subgroup that TauCeti.SlStd.graphAutomorphism moves x_k to is the one whose root is the image, under TauCeti.typeAGraphAut, of the root of x_k.

Together with TauCeti.SlStd.rootSubgroup_comp_graphAutomorphism_hom, which says the automorphism carries x_k to x_{γ k} without touching its parameter, this is the equation γ (x_α(t)) = x_{γ α}(t) on the numbered simple root subgroups.