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

TauCeti.E6DoubledMinuscule.groupScheme is the explicit integral affine group scheme obtained by closing the twelve numbered type-E₆ root subgroups and the fifty-four-weight torus of V(ϖ₁) ⊕ V(ϖ₆) 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.E6DoubledMinuscule.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, that its root datum has been identified, or that the E₆ diagram symmetry the doubled index set was assembled to carry acts on it.

Main declarations

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

Main results

• TauCeti.E6DoubledMinuscule.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the quotient presentations.
• TauCeti.E6DoubledMinuscule.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.E6DoubledMinuscule.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: the pinned generators are the scalar extensions of their integral coordinate maps.
• TauCeti.E6DoubledMinuscule.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.E6DoubledMinuscule.hopfSpec_map_weightTorusIntegralCoordinateMap_op: the integral coordinate maps represent the existing pinned morphisms.
• TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated after base change by the transported maps.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 12.2.
• 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, on the branch ²E₆(q) that the doubled carrier serves.

The declaration structure specializes the formal template in TauCeti.Algebra.Lie.E6.Minuscule.BaseChange, itself following 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.

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

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

Equations

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

theorem TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal_def (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight A

The transported defining ideal is the ideal supplied by the generic Kostant toral-closure base change.

@[simp]

theorem TauCeti.E6DoubledMinuscule.mem_baseChangeDefiningIdeal_iff (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A 54)} : x ∈ baseChangeDefiningIdeal A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 54).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.E6DoubledMinuscule.map_tmul_mem_baseChangeDefiningIdeal_of_mem (A : Type v) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ 54)} (hy : y ∈ definingIdeal) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 54).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.E6DoubledMinuscule.baseChangeCoordinateIso (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 54) (baseChangeDefiningIdeal A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) definingIdeal)

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

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

The transported root subgroups

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

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

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) definingIdeal) (rootSubgroupIntegralCoordinateMap k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ matrixBasis

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside GL₅₄.

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 54) (baseChangeDefiningIdeal A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

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

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.mkQuotient_comp_rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 54) (baseChangeDefiningIdeal A)) (rootSubgroupToBaseChangeCoordinateMap A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis A k

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.weightTorusIntegralCoordinateMap : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) definingIdeal ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 6))).obj

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

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.mkQuotient_comp_weightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 54) definingIdeal) weightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap matrixWeight

The integral factored weight-torus map recovers the represented weight-torus coordinate map inside GL₅₄.

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 54) (baseChangeDefiningIdeal A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin 6))).obj

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

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.mkQuotient_comp_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 54) (baseChangeDefiningIdeal A)) (weightTorusToBaseChangeCoordinateMap A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A matrixWeight

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.coordinateHopfAlgebra (A : Type v) [CommRing A] : CommHopfAlgCat A

The coordinate Hopf algebra of the doubled minuscule carrier after base change to A.

Equations

• TauCeti.E6DoubledMinuscule.coordinateHopfAlgebra A = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 54) (TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal A)

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

The quotient coordinate morphism representing the carrier's closed immersion into GL₅₄.

Equations

• TauCeti.E6DoubledMinuscule.coordinateMap A = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 54) (TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal A)

@[simp]

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

The quotient coordinate morphism followed by the weight-torus restriction recovers the ambient weight-torus morphism.

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

The carrier coordinate morphism is surjective.

@[simp]

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

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

@[reducible, inline]

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

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

Equations

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

@[simp]

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

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.mapPointsFunctor_coordinateMap_app (A : Type v) [CommRing A] {B : Type u_1} [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 54) (baseChangeDefiningIdeal A) ↧B)) g

Mapping a carrier point along its coordinate morphism gives the ambient quotient point.

@[reducible, inline]

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

The coordinate algebras of the numbered root subgroups and weight torus.

Equations

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

noncomputable def TauCeti.E6DoubledMinuscule.generatorCoordinateMap (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra A 54 ⟶ 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.E6DoubledMinuscule.generatorCoordinateMap A (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A TauCeti.E6DoubledMinuscule.matrixWeight

@[simp]

theorem TauCeti.E6DoubledMinuscule.generatorCoordinateMap_inl (A : Type v) [CommRing A] (i : Fin 6 ⊕ Fin 6) : generatorCoordinateMap A (Sum.inl i) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis A i

The root branch of the generator family is the transported root-subgroup map.

@[simp]

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

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

theorem TauCeti.E6DoubledMinuscule.baseChangeDefiningIdeal_le_commonKernel (A : Type v) [CommRing A] : baseChangeDefiningIdeal A ≤ CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap A)

The closed subgroup of GL₅₄/A generated by the transported numbered root subgroups and weight torus lies in the base change of the integral doubled type-E₆ carrier.

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