Base change of the full-weight type-E6 minuscule carrier

TauCeti.E6Minuscule.groupScheme is the explicit integral affine group scheme obtained by closing the twelve numbered type-E₆ root subgroups and the minuscule weight torus inside GL₂₇. This file specializes the base-change construction for a general Kostant toral closure to that pinned carrier.

For every commutative ring A, TauCeti.E6Minuscule.baseChangeDefiningIdeal 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 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 its torus is maximal, or that its root datum has been identified.

Main declarations

• TauCeti.E6Minuscule.baseChangeDefiningIdeal: the transported defining ideal in O(GL₂₇/A).
• TauCeti.E6Minuscule.coordinateHopfAlgebra and TauCeti.E6Minuscule.coordinateMap: the specialized carrier coordinate algebra and its ambient quotient map.
• TauCeti.E6Minuscule.finiteTypeCoordinateHopfAlgebra: the same coordinate algebra bundled with its finite-type property.
• TauCeti.E6Minuscule.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.E6Minuscule.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.E6Minuscule.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.
• TauCeti.E6Minuscule.generatorCoordinateMap: the transported numbered root subgroups and weight torus as one family of coordinate maps out of O(GL₂₇/A).

Main results

• TauCeti.E6Minuscule.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the quotient presentations.
• TauCeti.E6Minuscule.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.E6Minuscule.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: the pinned generators are the scalar extensions of their integral coordinate maps.
• TauCeti.E6Minuscule.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.E6Minuscule.hopfSpec_map_weightTorusIntegralCoordinateMap_op: the integral coordinate maps represent the existing pinned morphisms.

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. The resulting specialized pinned carrier is an input to milestone L0, “pinned ambient groups”, of TauCetiRoadmap/CFSGStatement/README.md.

The declaration structure specializes the formal template in TauCeti.Algebra.Lie.Symplectic.StandardCarrier.BaseChange. Every construction below uses the generic Kostant base-change API from Kostant/RootSubgroup/Scheme/ToralClosure/GeneralLinearBaseChange.lean; in particular, none of the coordinate-ring calculation is repeated here. The specialized coordinate-algebra packaging follows TauCeti.Algebra.Lie.E7.Minuscule.BaseChange.

noncomputable def TauCeti.E6Minuscule.baseChangeDefiningIdeal (A : Type v) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 27)

The Hopf ideal in O(GL₂₇/A) obtained by transporting the defining ideal of the integral full-weight type-E₆ minuscule carrier along ℤ → A.

Equations

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

theorem TauCeti.E6Minuscule.baseChangeDefiningIdeal_def (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight A

The transported defining ideal is the generic transported Kostant toral-closure presentation.

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.coordinateHopfAlgebra (A : Type v) [CommRing A] : CommHopfAlgCat A

The coordinate Hopf algebra of the full-weight type-E₆ minuscule carrier after base change to A.

Equations

• TauCeti.E6Minuscule.coordinateHopfAlgebra A = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 27) (TauCeti.E6Minuscule.baseChangeDefiningIdeal A)

noncomputable def TauCeti.E6Minuscule.coordinateMap (A : Type v) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A 27 ⟶ coordinateHopfAlgebra A

The quotient coordinate morphism O(GL₂₇) ⟶ O(carrier), representing the closed immersion of the specialized minuscule carrier into GL₂₇.

Equations

• TauCeti.E6Minuscule.coordinateMap A = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 27) (TauCeti.E6Minuscule.baseChangeDefiningIdeal A)

theorem TauCeti.E6Minuscule.coordinateMap_surjective (A : Type v) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap A))

The specialized carrier coordinate morphism is surjective.

@[simp]

theorem TauCeti.E6Minuscule.coordinateMap_ker (A : Type v) [CommRing A] : RingHom.ker ↑(CommHopfAlgCat.Hom.hom (coordinateMap A)) = (baseChangeDefiningIdeal A).toIdeal

The kernel of the specialized carrier coordinate morphism is the transported defining ideal.

theorem TauCeti.E6Minuscule.mapPointsFunctor_coordinateMap_app (A : Type v) [CommRing A] {B : Type w} [CommRing B] [Algebra A B] (g : ↑(HopfAlgebra.points ↧B)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (coordinateMap A)).app ↧B)) g = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A 27) (baseChangeDefiningIdeal A) ↧B)) g

Mapping a carrier point along the coordinate morphism gives the corresponding quotient point of the ambient general linear group.

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.finiteTypeCoordinateHopfAlgebra (A : Type v) [CommRing A] : FiniteTypeCommHopfAlgCat A

The specialized type-E₆ minuscule carrier as a finite-type commutative Hopf algebra.

Equations

• TauCeti.E6Minuscule.finiteTypeCoordinateHopfAlgebra A = TauCeti.FiniteTypeCommHopfAlgCat.of A ↑(TauCeti.E6Minuscule.coordinateHopfAlgebra A)

@[simp]

theorem TauCeti.E6Minuscule.finiteTypeCoordinateHopfAlgebra_obj (A : Type v) [CommRing A] : (finiteTypeCoordinateHopfAlgebra A).obj = coordinateHopfAlgebra A

The finite-type package has the specialized carrier coordinate Hopf algebra as its underlying object.

@[simp]

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

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

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

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

noncomputable def TauCeti.E6Minuscule.baseChangeCoordinateIso (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 27) (baseChangeDefiningIdeal A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal)

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

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

The transported root subgroups

noncomputable def TauCeti.E6Minuscule.rootSubgroupIntegralCoordinateMap (k : Fin 6 ⊕ Fin 6) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The integral kth root-subgroup coordinate map, with source expressed using the named type-E₆ defining ideal.

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal) (rootSubgroupIntegralCoordinateMap k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ k ⋯ (coordinateLatticeBasis (Fin 27))

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside GL₂₇.

theorem TauCeti.E6Minuscule.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (k : Fin 6 ⊕ Fin 6) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (rootSubgroupIntegralCoordinateMap k).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rootSubgroup k) (CategoryTheory.eqToHom groupScheme_def))

The integral factored root-subgroup coordinate map represents the carrier's kth numbered root subgroup.

noncomputable def TauCeti.E6Minuscule.rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 27) (baseChangeDefiningIdeal A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base-changed kth root-subgroup coordinate map factored through the transported type-E₆ carrier.

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (coordinateMap A) (rootSubgroupToBaseChangeCoordinateMap A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) A k

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

@[simp]

theorem TauCeti.E6Minuscule.pointToGeneralLinear_mapDomain_rootSubgroupToBaseChangeCoordinateMap_eq_rootSubgroupPoints (A : Type v) [CommRing A] (i : Fin 6 ⊕ Fin 6) (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : GeneralLinear.pointToGeneralLinear 27 ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (coordinateMap A))) (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (rootSubgroupToBaseChangeCoordinateMap A i))))) = ↑((rootSubgroupPoints i ↑B) (AdditiveGroup.gaPointsMulEquiv q))

The specialized root-subgroup coordinate map sends an additive point to the numbered minuscule root matrix with the same parameter.

@[simp]

theorem TauCeti.E6Minuscule.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupIntegralCoordinateMap k)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = rootSubgroupToBaseChangeCoordinateMap 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.E6Minuscule.weightTorusIntegralCoordinateMap : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 6))).obj

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

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.mkQuotient_comp_weightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal) weightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap weightTable.weight

The integral factored weight-torus map recovers the represented weight-torus coordinate map inside GL₂₇.

theorem TauCeti.E6Minuscule.hopfSpec_map_weightTorusIntegralCoordinateMap_op : (AlgebraicGeometry.hopfSpec ↧ℤ).map weightTorusIntegralCoordinateMap.op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp weightTorus (CategoryTheory.eqToHom groupScheme_def))

The integral factored weight-torus coordinate map represents the carrier's weight torus.

noncomputable def TauCeti.E6Minuscule.weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 27) (baseChangeDefiningIdeal A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin 6))).obj

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

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.coordinateMap_comp_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (coordinateMap A) (weightTorusToBaseChangeCoordinateMap A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A weightTable.weight

The factored weight-torus map composed with the carrier coordinate morphism recovers its ambient transported coordinate map.

@[simp]

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

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

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.generatorCoordinateAlgebra (A : Type v) [CommRing A] : (Fin 6 ⊕ Fin 6) ⊕ Unit → CommHopfAlgCat A

The coordinate algebras of the numbered root subgroups and weight torus of the type-E₆ minuscule carrier.

Equations

• TauCeti.E6Minuscule.generatorCoordinateAlgebra A (Sum.inl val) = TauCeti.AdditiveGroup.coordinateHopfAlgebra A
• TauCeti.E6Minuscule.generatorCoordinateAlgebra A (Sum.inr val) = (TauCeti.DiagonalizableGroup.coordinateRing A (TauCeti.SplitTorus.characterGroup (Fin 6))).obj

noncomputable def TauCeti.E6Minuscule.generatorCoordinateMap (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra A 27 ⟶ generatorCoordinateAlgebra A j

The coordinate maps of the numbered root subgroups and weight torus into GL₂₇.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.E6Minuscule.generatorCoordinateMap A (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A TauCeti.E6Minuscule.weightTable.weight

@[simp]

theorem TauCeti.E6Minuscule.generatorCoordinateMap_inl (A : Type v) [CommRing A] (i : Fin 6 ⊕ Fin 6) : generatorCoordinateMap A (Sum.inl i) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) A i

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

@[simp]

theorem TauCeti.E6Minuscule.generatorCoordinateMap_inr (A : Type v) [CommRing A] : generatorCoordinateMap A (Sum.inr ()) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A weightTable.weight

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