Base change of the pinned Geck carrier

For a valid Dynkin type t, DynkinType.geckGroupScheme is the explicit integral affine group scheme obtained by closing the numbered Geck root subgroups and the Geck weight torus inside a general linear group. This file specializes the base-change construction for a general Kostant toral closure to that pinned carrier.

For every commutative ring A, geckBaseChangeDefiningIdeal is an ideal in O(GLₙ/A) whose quotient is canonically the scalar extension of the integral coordinate Hopf algebra. The transported numbered root-subgroup maps and weight-torus map factor through that quotient. Thus the explicit integral carrier and its pinned generators base-change together; none of the data is chosen anew over A.

The defining ideal transported from ℤ is contained in the common kernel of the transported generators. Equality is not asserted over an arbitrary, possibly non-flat, base: additional equations can appear after specialization. Nor does this file assert that the carrier is reductive or that the represented weight torus is maximal.

Main declarations

• TauCeti.DynkinType.geckBaseChangeDefiningIdeal: the transported defining ideal in O(GLₙ/A).
• TauCeti.DynkinType.geckBaseChangeCoordinateIso: its quotient is the scalar extension of the integral Geck coordinate Hopf algebra.
• TauCeti.DynkinType.geckBaseChangePointsMulEquiv: the points of that quotient in a commutative A-algebra are the matrix points of the integral carrier over that algebra.
• TauCeti.DynkinType.geckRootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.DynkinType.geckWeightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.
• TauCeti.DynkinType.geckGeneratorCoordinateAlgebra and TauCeti.DynkinType.geckGeneratorCoordinateMap: the transported numbered root subgroups and weight torus as one family of coordinate maps into GLₙ/A.

Main results

• TauCeti.DynkinType.geckBaseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated after base change by those maps.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• B. Conrad, Reductive Group Schemes, §1.

This advances the base-change target in Layer 9 of the ReductiveGroups roadmap. The resulting specialized pinned carrier is an input to milestone L0, "pinned ambient groups", of the CFSGStatement roadmap.

noncomputable def TauCeti.DynkinType.geckBaseChangeDefiningIdeal (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht))

The Hopf ideal in O(GLₙ/A) obtained by transporting the defining ideal of the integral Geck carrier along ℤ → A.

Equations

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

noncomputable def TauCeti.DynkinType.geckBaseChangeCoordinateIso (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht))

The coordinate Hopf algebra cut out over A by the transported Geck defining ideal is canonically the scalar extension of the integral coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.DynkinType.mkQuotient_comp_geckBaseChangeCoordinateIso_hom (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A)) (t.geckBaseChangeCoordinateIso ht A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (t.geckDim ht)).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht)))

The base-change coordinate isomorphism is compatible with the quotient presentation inside GLₙ.

Points of the base-changed carrier

noncomputable def TauCeti.DynkinType.geckBaseChangePointsMulEquiv (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (B : CommAlgCat A) : ↑(HopfAlgebra.points B) ≃* ↥(t.geckPoints ht ↑B)

The points of the base-changed Geck carrier are its matrix-valued points over the new base.

This is CommHopfAlgCat.baseChangeIsoPointsMulEquiv, read at the transport geckBaseChangeCoordinateIso, followed by the represented-points equivalence of the integral Geck carrier. Thus this definition uses the scalar extension constructed above rather than choosing a new carrier over A.

The value algebra B is an arbitrary commutative A-algebra, so this identifies the points of the specialized carrier at every value algebra rather than only at A; taking B to be CommAlgCat.of A A reads its A-points.

Equations

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

@[simp]

theorem TauCeti.DynkinType.coe_geckBaseChangePointsMulEquiv_apply (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : ↑((t.geckBaseChangePointsMulEquiv ht A B) q) = (GeneralLinear.pointsMulEquiv (t.geckDim ht)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A) B)) q)

Under geckBaseChangePointsMulEquiv, a quotient point has the same ambient invertible matrix as its composite with the quotient map over A.

@[simp]

theorem TauCeti.DynkinType.quotientPointsHom_geckBaseChangePointsMulEquiv_symm (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (B : CommAlgCat A) (g : ↥(t.geckPoints ht ↑B)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A) B)) ((t.geckBaseChangePointsMulEquiv ht A B).symm g) = (GeneralLinear.pointsMulEquiv (t.geckDim ht)).symm ↑g

Under the inverse of geckBaseChangePointsMulEquiv, the ambient point of the quotient point attached to a Geck point is the one read off its invertible matrix.

@[simp]

theorem TauCeti.DynkinType.geckBaseChangePointsMulEquiv_mapPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] {B C : CommAlgCat A} (χ : B ⟶ C) (q : ↑(HopfAlgebra.points B)) : (t.geckBaseChangePointsMulEquiv ht A C) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) q) = ((t.geckPointsPresentation ht ↑B).map (t.geckPointsPresentation ht ↑C) ↑(CommAlgCat.Hom.hom χ)) ((t.geckBaseChangePointsMulEquiv ht A B) q)

The identification of the base-changed Geck carrier's points is natural in the value algebra. A morphism χ : B ⟶ C of value A-algebras acts on the specialized carrier's points by HopfAlgebra.mapPoints and on the Geck points by the shared presentation map along the same morphism with its scalars restricted to ℤ, and the equivalence intertwines the two. A consumer can therefore use it functorially without unfolding its composite implementation.

noncomputable def TauCeti.DynkinType.geckRootSubgroupIntegralCoordinateMap (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The integral ith root-subgroup coordinate map, with source expressed using the named Geck defining ideal.

Equations

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

theorem TauCeti.DynkinType.geckRootSubgroupIntegralCoordinateMap_def (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : t.geckRootSubgroupIntegralCoordinateMap ht i = UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht) i

The named integral Geck root-subgroup map is the generic Kostant toral factorization.

noncomputable def TauCeti.DynkinType.geckRootSubgroupBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht) ⟶ AdditiveGroup.coordinateHopfAlgebra A

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

Equations

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

noncomputable def TauCeti.DynkinType.geckRootSubgroupToBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base-changed ith Geck root-subgroup coordinate map factored through the transported Geck carrier.

Equations

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

@[simp]

theorem TauCeti.DynkinType.mkQuotient_comp_geckRootSubgroupToBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A)) (t.geckRootSubgroupToBaseChangeCoordinateMap ht A i) = t.geckRootSubgroupBaseChangeCoordinateMap ht A i

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

@[simp]

theorem TauCeti.DynkinType.geckBaseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : CategoryTheory.CategoryStruct.comp (t.geckBaseChangeCoordinateIso ht A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (t.geckRootSubgroupIntegralCoordinateMap ht i)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = t.geckRootSubgroupToBaseChangeCoordinateMap ht A i

Under the Geck coordinate isomorphism, the factored ith root-subgroup map is the scalar extension of its integral coordinate map.

noncomputable def TauCeti.DynkinType.geckWeightTorusBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin t.rank))).obj

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

Equations

• t.geckWeightTorusBaseChangeCoordinateMap ht A = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (t.geckWeightFin ht)

noncomputable def TauCeti.DynkinType.geckWeightTorusIntegralCoordinateMap (t : DynkinType) (ht : t.Valid) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht) ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin t.rank))).obj

The integral weight-torus coordinate map, with source expressed using the named Geck defining ideal.

Equations

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

theorem TauCeti.DynkinType.geckWeightTorusIntegralCoordinateMap_def (t : DynkinType) (ht : t.Valid) : t.geckWeightTorusIntegralCoordinateMap ht = UniversalEnvelopingAlgebra.kostantWeightTorusToralCoordinateMap (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht)

The named integral Geck weight-torus map is the generic Kostant toral factorization.

noncomputable def TauCeti.DynkinType.geckWeightTorusToBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin t.rank))).obj

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

Equations

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

@[simp]

theorem TauCeti.DynkinType.mkQuotient_comp_geckWeightTorusToBaseChangeCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht)) (t.geckBaseChangeDefiningIdeal ht A)) (t.geckWeightTorusToBaseChangeCoordinateMap ht A) = t.geckWeightTorusBaseChangeCoordinateMap ht A

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

@[simp]

theorem TauCeti.DynkinType.geckBaseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (t.geckBaseChangeCoordinateIso ht A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (t.geckWeightTorusIntegralCoordinateMap ht)) (CommHopfAlgCat.ofHom ↑(MonoidAlgebra.scalarTensorBialgEquiv ℤ A))) = t.geckWeightTorusToBaseChangeCoordinateMap ht A

Under the Geck coordinate isomorphism, the factored weight-torus map is the scalar extension of its integral coordinate map.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckGeneratorCoordinateAlgebra (t : DynkinType) (A : Type v) [CommRing A] : (Fin t.rank ⊕ Fin t.rank) ⊕ Unit → CommHopfAlgCat A

The coordinate algebras of the transported numbered Geck root subgroups and the transported Geck weight torus: an affine line for each numbered root subgroup, and the split torus of rank t.rank.

Equations

• t.geckGeneratorCoordinateAlgebra A (Sum.inl val) = TauCeti.AdditiveGroup.coordinateHopfAlgebra A
• t.geckGeneratorCoordinateAlgebra A (Sum.inr val) = (TauCeti.DiagonalizableGroup.coordinateRing A (TauCeti.SplitTorus.characterGroup (Fin t.rank))).obj

noncomputable def TauCeti.DynkinType.geckGeneratorCoordinateMap (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (j : (Fin t.rank ⊕ Fin t.rank) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra A (t.geckDim ht) ⟶ t.geckGeneratorCoordinateAlgebra A j

The coordinate maps of the transported numbered Geck root subgroups and the transported Geck weight torus into GLₙ/A, as one family.

Equations

• t.geckGeneratorCoordinateMap ht A (Sum.inl val) = t.geckRootSubgroupBaseChangeCoordinateMap ht A val
• t.geckGeneratorCoordinateMap ht A (Sum.inr val) = t.geckWeightTorusBaseChangeCoordinateMap ht A

@[simp]

theorem TauCeti.DynkinType.geckGeneratorCoordinateMap_inl (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : t.geckGeneratorCoordinateMap ht A (Sum.inl i) = t.geckRootSubgroupBaseChangeCoordinateMap ht A i

The numbered branches of the generator family are the transported root-subgroup maps.

@[simp]

theorem TauCeti.DynkinType.geckGeneratorCoordinateMap_inr (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : t.geckGeneratorCoordinateMap ht A (Sum.inr ()) = t.geckWeightTorusBaseChangeCoordinateMap ht A

The remaining branch of the generator family is the transported weight-torus map.

theorem TauCeti.DynkinType.geckBaseChangeDefiningIdeal_le_commonKernel (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : t.geckBaseChangeDefiningIdeal ht A ≤ CommHopfAlgCat.commonKernelHopfIdeal (t.geckGeneratorCoordinateMap ht A)

The closed subgroup of GLₙ/A generated by the transported numbered Geck root subgroups and the transported weight torus lies in the base change of the integral Geck carrier.

The reverse inclusion is not asserted over an arbitrary base ring.