Base change of the full-weight type A carrier

The full-weight type A_r carrier is constructed over ℤ by closing its numbered root subgroups and weight torus inside GL_{r+1}. This file specializes the general base-change presentation of a toral Kostant closure to that carrier.

For every commutative ring A, TauCeti.SlStd.baseChangeDefiningIdeal is the transported integral defining ideal inside O(GL_{r+1}/A). Its quotient is canonically the scalar extension of the integral carrier coordinate ring. The numbered root-subgroup and weight-torus coordinate maps base-change with the carrier and factor through that quotient, so the pinning is transported rather than chosen again after changing the base.

This file does not identify the carrier with SL_{r+1} or assert reductivity or maximality of its torus.

Main declarations

• TauCeti.SlStd.baseChangeDefiningIdeal: the transported defining ideal in O(GL_{r+1}/A).
• TauCeti.SlStd.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.SlStd.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the base-changed carrier.
• TauCeti.SlStd.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the base-changed carrier.
• TauCeti.SlStd.baseChangeDefiningIdeal_le_commonKernel: the transported ideal lies in the common kernel of the numbered root-subgroup and weight-torus maps.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §§3--4.

This advances the base-change and pinning targets in Layer 9 of the ReductiveGroups roadmap. The specialized type A carrier is consumed by milestone L0, "pinned ambient groups", of the CFSGStatement roadmap.

noncomputable def TauCeti.SlStd.baseChangeDefiningIdeal (r : ℕ) (A : Type v) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A (r + 1))

The Hopf ideal in O(GL_{r+1}/A) obtained by transporting the defining ideal of the integral full-weight type A_r carrier along ℤ → A.

Equations

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

@[simp]

theorem TauCeti.SlStd.baseChangeDefiningIdeal_def (r : ℕ) (A : Type v) [CommRing A] : baseChangeDefiningIdeal r A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r) A

The specialized defining ideal is the general toral Kostant base-change ideal for the standard type A_r representation.

noncomputable def TauCeti.SlStd.baseChangeCoordinateIso (r : ℕ) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)))

The coordinate Hopf algebra cut out by the transported type A_r defining ideal is canonically the scalar extension of the integral carrier coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.SlStd.mkQuotient_comp_baseChangeCoordinateIso_hom (r : ℕ) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A)) (baseChangeCoordinateIso r A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (r + 1)).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (r + 1)) (UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r))))

The type A_r base-change coordinate isomorphism is compatible with the quotient presentation inside GL_{r+1}.

noncomputable def TauCeti.SlStd.rootSubgroupBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] (i : Fin r ⊕ Fin r) : GeneralLinear.coordinateHopfAlgebra A (r + 1) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base change to A of the integral root-subgroup coordinate map at the numbered root i, transported to the coordinate Hopf algebras constructed directly over A.

Equations

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

theorem TauCeti.SlStd.rootSubgroupBaseChangeCoordinateMap_def (r : ℕ) (A : Type v) [CommRing A] (i : Fin r ⊕ Fin r) : rootSubgroupBaseChangeCoordinateMap r A i = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) A i

The ambient base-changed root-subgroup map is the specialization of the general transported Kostant root-subgroup map.

noncomputable def TauCeti.SlStd.rootSubgroupToBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] (i : Fin r ⊕ Fin r) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base-changed numbered root-subgroup coordinate map factored through the transported type A_r carrier.

Equations

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

@[simp]

theorem TauCeti.SlStd.mkQuotient_comp_rootSubgroupToBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] (i : Fin r ⊕ Fin r) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A)) (rootSubgroupToBaseChangeCoordinateMap r A i) = rootSubgroupBaseChangeCoordinateMap r A i

The factored type A_r root-subgroup map recovers its ambient transported coordinate map.

noncomputable def TauCeti.SlStd.weightTorusBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A (r + 1) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin r))).obj

The base change to A of the integral type A_r weight-torus coordinate map, transported to the coordinate Hopf algebras constructed directly over A.

Equations

• TauCeti.SlStd.weightTorusBaseChangeCoordinateMap r A = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (TauCeti.SlStd.weight r)

theorem TauCeti.SlStd.weightTorusBaseChangeCoordinateMap_def (r : ℕ) (A : Type v) [CommRing A] : weightTorusBaseChangeCoordinateMap r A = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (weight r)

The ambient base-changed weight-torus map is the scalar extension of the integral weight torus, transported into the coordinate Hopf algebras constructed directly over A.

theorem TauCeti.SlStd.hom_weightTorusBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] : CommHopfAlgCat.Hom.hom (weightTorusBaseChangeCoordinateMap r A) = GeneralLinear.weightTorusCoordinateBialgHom (weight r)

The underlying bialgebra morphism of the transported type A_r weight torus is the direct diagonal representation over A with the standard-module weights.

noncomputable def TauCeti.SlStd.weightTorusToBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin r))).obj

The base-changed type A_r weight-torus coordinate map factored through the transported carrier.

Equations

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

@[simp]

theorem TauCeti.SlStd.mkQuotient_comp_weightTorusToBaseChangeCoordinateMap (r : ℕ) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (r + 1)) (baseChangeDefiningIdeal r A)) (weightTorusToBaseChangeCoordinateMap r A) = weightTorusBaseChangeCoordinateMap r A

The factored type A_r weight-torus map recovers its ambient transported coordinate map.

theorem TauCeti.SlStd.baseChangeDefiningIdeal_le_commonKernel (r : ℕ) (A : Type v) [CommRing A] : let K := fun (x : (Fin r ⊕ Fin r) ⊕ Unit) => match x with | Sum.inl val => AdditiveGroup.coordinateHopfAlgebra A | Sum.inr val => (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin r))).obj; baseChangeDefiningIdeal r A ≤ CommHopfAlgCat.commonKernelHopfIdeal fun (j : (Fin r ⊕ Fin r) ⊕ Unit) => match j with | Sum.inl i => rootSubgroupBaseChangeCoordinateMap r A i | Sum.inr val => weightTorusBaseChangeCoordinateMap r A

The transported defining ideal lies in the common kernel of the numbered root-subgroup and weight-torus maps over A.