Base change of the full-weight type-C carrier

For n : ℕ, TauCeti.SpStd.groupScheme is the explicit integral affine group scheme obtained by closing the numbered standard type-C_(n+1) root subgroups and the standard weight torus inside GL_(2n+2). This file specializes the base-change construction for a general Kostant toral closure to that pinned carrier.

For every commutative ring A, TauCeti.SpStd.baseChangeDefiningIdeal is an ideal in O(GL_(2n+2)/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, that the represented weight torus is maximal, or that the carrier is the separately constructed symplectic group scheme.

Main declarations

• TauCeti.SpStd.baseChangeDefiningIdeal: the transported defining ideal in O(GL_(2n+2)/A).
• TauCeti.SpStd.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.SpStd.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.SpStd.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.

Main results

• TauCeti.SpStd.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the two quotient presentations.
• TauCeti.SpStd.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.SpStd.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: each factored generator is the scalar extension of its integral coordinate map.
• TauCeti.SpStd.mkQuotient_comp_rootSubgroupIntegralCoordinateMap and TauCeti.SpStd.mkQuotient_comp_weightTorusIntegralCoordinateMap: over ℤ, each integral generator map recovers the coordinate map it factors, and so is determined by it.
• TauCeti.SpStd.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.SpStd.hopfSpec_map_weightTorusIntegralCoordinateMap_op: those integral generator maps represent the carrier's existing pinning morphisms TauCeti.SpStd.rootSubgroup and TauCeti.SpStd.weightTorus.
• TauCeti.SpStd.baseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated after base change by those maps.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• B. Conrad, Reductive Group Schemes, §1.

This advances the base-change target in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, "Base change along ℤ → k for any commutative ring k, and the compatibility of the pinning with it". The resulting specialized pinned carrier is an input to milestone L0, "pinned ambient groups", of TauCetiRoadmap/CFSGStatement/README.md, which reads the carrier of a finite group of Lie type off the points of a pinned Chevalley--Demazure group over an algebraic closure. The declaration structure follows the sibling specialization for the pinned Geck carrier in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.BaseChange. Every declaration below is the corresponding generic Kostant declaration at this carrier's data; the transport reading the generic base-change presentation through a named integral defining ideal is the ...OfEq family of Kostant/RootSubgroup/Scheme/ToralClosure/GeneralLinearBaseChange.lean, so nothing of that calculation is repeated here.

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

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

Equations

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

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

The transported defining ideal is the one supplied by the generic Kostant toral-closure base change. The module system does not expose a definition's body outside its own module, so this is the form in which downstream files rewrite with the definition.

@[simp]

theorem TauCeti.SpStd.mem_baseChangeDefiningIdeal_iff (n : ℕ) (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A (n + 1 + (n + 1)))} : x ∈ baseChangeDefiningIdeal n A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (n + 1 + (n + 1))).inv) x ∈ CommHopfAlgCat.baseChangeHopfIdeal (definingIdeal n)

Membership in the transported defining ideal is membership of the corresponding element in the base change of the named integral defining ideal.

theorem TauCeti.SpStd.map_tmul_mem_baseChangeDefiningIdeal_of_mem (n : ℕ) (A : Type v) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1)))} (hy : y ∈ definingIdeal n) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (n + 1 + (n + 1))).hom) (s ⊗ₜ[ℤ] y) ∈ baseChangeDefiningIdeal n A

Transporting a pure tensor of a scalar and an integral defining equation produces an equation in the transported defining ideal.

noncomputable def TauCeti.SpStd.baseChangeCoordinateIso (n : ℕ) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (n + 1 + (n + 1))) (baseChangeDefiningIdeal n A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n))

The coordinate Hopf algebra cut out over A by the transported type-C_(n+1) 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.SpStd.mkQuotient_comp_baseChangeCoordinateIso_hom (n : ℕ) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (n + 1 + (n + 1))) (baseChangeDefiningIdeal n A)) (baseChangeCoordinateIso n A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (n + 1 + (n + 1))).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n)))

The base-change coordinate isomorphism is compatible with the quotient presentation inside GL_(2n+2).

The transported root subgroups

noncomputable def TauCeti.SpStd.rootSubgroupIntegralCoordinateMap (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The integral kth root-subgroup coordinate map, with source expressed using the named type-C_(n+1) defining ideal.

Equations

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

theorem TauCeti.SpStd.rootSubgroupIntegralCoordinateMap_def (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : rootSubgroupIntegralCoordinateMap n k = UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMapOfEq (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯ k

The integral root-subgroup coordinate map is the generic Kostant one, read through the named type-C_(n+1) defining ideal.

@[simp]

theorem TauCeti.SpStd.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n)) (rootSubgroupIntegralCoordinateMap n k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside GL_(2n+2), and so determines it.

theorem TauCeti.SpStd.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).map (rootSubgroupIntegralCoordinateMap n k).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rootSubgroup n k) (CategoryTheory.eqToHom ⋯))

The integral factored root-subgroup coordinate map represents the carrier's kth numbered root subgroup: its spectrum is TauCeti.SpStd.rootSubgroup, read through the quotient-spectrum presentation of the carrier.

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

The base-changed kth root-subgroup coordinate map factored through the transported type-C_(n+1) carrier.

Equations

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

@[simp]

theorem TauCeti.SpStd.mkQuotient_comp_rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (n + 1 + (n + 1))) (baseChangeDefiningIdeal n A)) (rootSubgroupToBaseChangeCoordinateMap n A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

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

Since CommHopfAlgCat.mkQuotient is an epimorphism this determines the factored map, which is why no separate defining equation for it is stated: its source is spelled with TauCeti.SpStd.baseChangeDefiningIdeal, so such an equation would need an eqToHom transport.

@[simp]

theorem TauCeti.SpStd.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso n A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupIntegralCoordinateMap n k)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = rootSubgroupToBaseChangeCoordinateMap n A k

Under the base-change coordinate isomorphism, the factored kth root-subgroup map is the scalar extension of its integral coordinate map.

The transported weight torus

noncomputable def TauCeti.SpStd.weightTorusIntegralCoordinateMap (n : ℕ) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n) ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin (n + 1)))).obj

The integral weight-torus coordinate map, with source expressed using the named type-C_(n+1) defining ideal.

Equations

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

theorem TauCeti.SpStd.weightTorusIntegralCoordinateMap_def (n : ℕ) : weightTorusIntegralCoordinateMap n = UniversalEnvelopingAlgebra.kostantWeightTorusToralCoordinateMapOfEq (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯

The integral weight-torus coordinate map is the generic Kostant one, read through the named type-C_(n+1) defining ideal.

@[simp]

theorem TauCeti.SpStd.mkQuotient_comp_weightTorusIntegralCoordinateMap (n : ℕ) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (n + 1 + (n + 1))) (definingIdeal n)) (weightTorusIntegralCoordinateMap n) = GeneralLinear.weightTorusCoordinateMap (basisWeight n)

The integral factored weight-torus map recovers the weight-torus coordinate map inside GL_(2n+2), and so determines it.

theorem TauCeti.SpStd.hopfSpec_map_weightTorusIntegralCoordinateMap_op (n : ℕ) : (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).map (weightTorusIntegralCoordinateMap n).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (weightTorus n) (CategoryTheory.eqToHom ⋯))

The integral factored weight-torus coordinate map represents the carrier's weight torus: its spectrum is TauCeti.SpStd.weightTorus, read through the quotient-spectrum presentation of the carrier.

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

The base-changed weight-torus coordinate map factored through the transported type-C_(n+1) carrier.

Equations

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

@[simp]

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

The factored weight-torus map recovers its ambient transported coordinate map, and so determines it.

@[simp]

theorem TauCeti.SpStd.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap (n : ℕ) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso n A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (weightTorusIntegralCoordinateMap n)) (CommHopfAlgCat.ofHom ↑(MonoidAlgebra.scalarTensorBialgEquiv ℤ A))) = weightTorusToBaseChangeCoordinateMap n A

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

theorem TauCeti.SpStd.baseChangeDefiningIdeal_le_commonKernel (n : ℕ) (A : Type v) [CommRing A] : let K := fun (x : (Fin (n + 1) ⊕ Fin (n + 1)) ⊕ Unit) => match x with | Sum.inl val => AdditiveGroup.coordinateHopfAlgebra A | Sum.inr val => (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin (n + 1)))).obj; baseChangeDefiningIdeal n A ≤ CommHopfAlgCat.commonKernelHopfIdeal fun (j : (Fin (n + 1) ⊕ Fin (n + 1)) ⊕ Unit) => match j with | Sum.inl k => UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (rootGenerator n) (cartanGenerator n) (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k | Sum.inr val => GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (basisWeight n)

The closed subgroup of GL_(2n+2)/A generated by the transported numbered root subgroups and the transported weight torus lies in the base change of the integral type-C_(n+1) carrier.

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