All root subgroups of the type A full-weight carrier

The standard type-A_r carrier is generated by the root subgroups attached to the numbered simple raising and lowering operators. This file proves that it contains every elementary root subgroup

x_ij : G_a -> SlStd.groupScheme r, for i != j : Fin (r + 1).

The pair (i, j) represents the root epsilon_i - epsilon_j. Thus the construction covers all r * (r + 1) roots, not only the 2r simple positive and negative roots used to generate the carrier. The key input is TauCeti.SlStd.transvectionUnit_mem_points: every elementary transvection belongs to the carrier over every commutative ring. Applying this to the universal point of G_a proves that the ambient general-linear coordinate morphism kills the carrier's defining Hopf ideal, and hence factors through its quotient coordinate algebra.

The resulting morphisms retain their ambient matrix description and therefore satisfy the type-A Chevalley commutator equations on arbitrary commutative-ring-valued points.

Main definitions

• TauCeti.SlStd.rootSubgroupPointsOfPair: the elementary root subgroup on carrier points.
• TauCeti.SlStd.rootSubgroupCoordinateMapOfPair: its coordinate morphism out of the carrier's quotient coordinate Hopf algebra.
• TauCeti.SlStd.rootSubgroupOfPair: the group-scheme morphism G_a -> SlStd.groupScheme r.

Main results

• TauCeti.SlStd.rootSubgroupOfPair_comp_carrierι: inclusion in GL_(r+1) recovers the ambient root subgroup.
• TauCeti.SlStd.rootSubgroupOfPair_eq_rootSubgroup: on numbered simple roots, the all-root family agrees with the pinned family.
• TauCeti.SlStd.isClosedImmersion_rootSubgroupOfPair: every root subgroup is a closed copy of the additive group.
• TauCeti.SlStd.commute_rootSubgroupPointsOfPair and TauCeti.SlStd.commutatorElement_rootSubgroupPointsOfPair: the type-A Chevalley relations.

References

• J. S. Milne, Algebraic Groups (2017), Section 21.
• R. W. Carter, Simple Groups of Lie Type (1972), Sections 4.4, 7.1, and 11.3.
• R. Steinberg, Lectures on Chevalley Groups, Sections 3--4.

This advances the "Root subgroup maps" target in Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L0, "pinned ambient groups", of TauCetiRoadmap/CFSGStatement/README.md; milestone L1 subsequently needs the Frobenius equation on x_alpha for every root alpha.

noncomputable def TauCeti.SlStd.rootSubgroupPointsOfPair (r : ℕ) {A : Type u} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) : Multiplicative A →* ↥(points r A)

The root subgroup for epsilon_i - epsilon_j on points of the full-weight type-A_r carrier. Its value at c is the elementary transvection 1 + c E_ij.

Equations

• TauCeti.SlStd.rootSubgroupPointsOfPair r hij = (TauCeti.transvectionHom hij).codRestrict (TauCeti.SlStd.points r A) ⋯

@[simp]

theorem TauCeti.SlStd.coe_rootSubgroupPointsOfPair (r : ℕ) {A : Type u} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (c : Multiplicative A) : ↑((rootSubgroupPointsOfPair r hij) c) = transvectionUnit hij (Multiplicative.toAdd c)

A root-subgroup point indexed by a pair is its elementary transvection matrix.

theorem TauCeti.SlStd.rootSubgroupPointsOfPair_injective (r : ℕ) {A : Type u} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) : Function.Injective ⇑(rootSubgroupPointsOfPair r hij)

Every pair-indexed root subgroup is injective on points.

@[simp]

theorem TauCeti.SlStd.rootSubgroupPointsOfPair_eq_rootSubgroupPoints (r : ℕ) {A : Type u} [CommRing A] (k : Fin r ⊕ Fin r) : rootSubgroupPointsOfPair r ⋯ = rootSubgroupPoints r k A

On a numbered simple root, the pair-indexed point map is the existing pinned point map. The matrix indices are (rootTarget, rootSource), since the corresponding matrix unit sends the source basis vector to the target basis vector.

theorem TauCeti.SlStd.commute_rootSubgroupPointsOfPair (r : ℕ) {A : Type u} [CommRing A] {i j k l : Fin (r + 1)} (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (c d : Multiplicative A) : Commute ((rootSubgroupPointsOfPair r hij) c) ((rootSubgroupPointsOfPair r hkl) d)

Root-subgroup values at non-chaining roots commute inside the carrier.

theorem TauCeti.SlStd.commutatorElement_rootSubgroupPointsOfPair (r : ℕ) {A : Type u} [CommRing A] {i j l : Fin (r + 1)} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (c d : A) : ⁅(rootSubgroupPointsOfPair r hij) (Multiplicative.ofAdd c), (rootSubgroupPointsOfPair r hjl) (Multiplicative.ofAdd d)⁆ = (rootSubgroupPointsOfPair r hil) (Multiplicative.ofAdd (c * d))

The type-A Chevalley commutator equation inside the carrier: [x_ij(c), x_jl(d)] = x_il(cd) for three distinct indices.

theorem TauCeti.SlStd.commutatorElement_rootSubgroupPointsOfPair_reverse (r : ℕ) {A : Type u} [CommRing A] {i j k : Fin (r + 1)} (hij : i ≠ j) (hki : k ≠ i) (hkj : k ≠ j) (c d : A) : ⁅(rootSubgroupPointsOfPair r hij) (Multiplicative.ofAdd c), (rootSubgroupPointsOfPair r hki) (Multiplicative.ofAdd d)⁆ = (rootSubgroupPointsOfPair r hkj) (Multiplicative.ofAdd (-(d * c)))

The reverse-orientation type-A Chevalley commutator equation inside the carrier: [x_ij(c), x_ki(d)] = x_kj(-(dc)) for three distinct indices.

noncomputable def TauCeti.SlStd.rootSubgroupCoordinateMapOfPair (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate morphism of the root subgroup x_ij, factored through the quotient coordinate algebra of the full-weight type-A_r carrier.

Equations

• TauCeti.SlStd.rootSubgroupCoordinateMapOfPair r hij = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.SlStd.allRootDefiningIdeal✝ r) (TauCeti.GeneralLinear.rootSubgroupCoordinateMap hij) ⋯

theorem TauCeti.SlStd.rootSubgroupCoordinateMapOfPair_surjective (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMapOfPair r hij))

Every pair-indexed root coordinate morphism is surjective.

@[simp]

theorem TauCeti.SlStd.mkQuotient_comp_rootSubgroupCoordinateMapOfPair (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))) (rootSubgroupCoordinateMapOfPair r hij) = GeneralLinear.rootSubgroupCoordinateMap hij

Precomposing a pair-indexed root coordinate morphism with the carrier quotient map recovers the ambient general-linear root coordinate morphism.

@[simp]

theorem TauCeti.SlStd.rootSubgroupCoordinateMapOfPair_eq_rootSubgroupCoordinateMap (r : ℕ) (k : Fin r ⊕ Fin r) : rootSubgroupCoordinateMapOfPair r ⋯ = UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r) k

For a numbered simple root, the pair-indexed coordinate map is the coordinate map of the existing pinned root subgroup.

noncomputable def TauCeti.SlStd.rootSubgroupOfPair (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme r

The root subgroup x_ij : G_a -> SlStd.groupScheme r attached to the type-A root epsilon_i - epsilon_j.

Equations

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

theorem TauCeti.SlStd.rootSubgroupOfPair_def (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : rootSubgroupOfPair r hij = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧ℤ).map (rootSubgroupCoordinateMapOfPair r hij).op)

The pair-indexed root subgroup is relative spectrum applied contravariantly to its factored coordinate morphism.

@[simp]

theorem TauCeti.SlStd.rootSubgroupOfPair_eq_rootSubgroup (r : ℕ) (k : Fin r ⊕ Fin r) : rootSubgroupOfPair r ⋯ = rootSubgroup r k

On a numbered simple root, the pair-indexed group-scheme morphism is the existing pinned root-subgroup morphism.

instance TauCeti.SlStd.isClosedImmersion_rootSubgroupOfPair (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroupOfPair r hij).hom.hom)

Every pair-indexed root subgroup is a closed copy of the additive group.

@[simp]

theorem TauCeti.SlStd.rootSubgroupOfPair_comp_carrierι (r : ℕ) {i j : Fin (r + 1)} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (rootSubgroupOfPair r hij) (carrierι r) = GeneralLinear.rootSubgroup hij

Including x_ij in GL_(r+1) recovers the ambient root subgroup attached to epsilon_i - epsilon_j.

@[simp]

theorem TauCeti.SlStd.schemePointsMulEquiv_rootSubgroupOfPair_comp_carrierι (r : ℕ) {i j : Fin (r + 1)} {A : Type} [CommRing A] (hij : i ≠ j) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : (GeneralLinear.schemePointsMulEquiv (r + 1) A) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (rootSubgroupOfPair r hij).hom.hom (carrierι r).hom.hom)) = transvectionUnit hij (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p))

On scheme-valued points, a pair-indexed carrier root subgroup becomes the elementary transvection with the same parameter after inclusion in GL_(r+1).