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

TauCeti.E7Minuscule.groupScheme is the explicit integral affine group scheme obtained by closing the fourteen 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 toral-closure carrier.

For every commutative ring A, TauCeti.E7Minuscule.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 numbered root-subgroup and weight-torus maps 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.E7Minuscule.baseChangeDefiningIdeal: the transported defining ideal in O(GL₅₆/A).
• TauCeti.E7Minuscule.coordinateHopfAlgebra and TauCeti.E7Minuscule.coordinateMap: the specialized carrier coordinate algebra and its ambient quotient map.
• TauCeti.E7Minuscule.finiteTypeCoordinateHopfAlgebra: the same coordinate algebra bundled with its finite-type property.
• TauCeti.E7Minuscule.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.E7Minuscule.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.E7Minuscule.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.

Main results

• TauCeti.E7Minuscule.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the quotient presentations.
• TauCeti.E7Minuscule.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap: the factored root-subgroup maps recover the transported ambient root-subgroup maps.
• pointToGeneralLinear_mapDomain_rootSubgroupToBaseChangeCoordinateMap_eq_rootSubgroupPoints: on points over any value algebra, the factored root-subgroup maps give the numbered root matrices.
• TauCeti.E7Minuscule.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.E7Minuscule.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: the numbered root-subgroup and weight-torus maps are the scalar extensions of their integral coordinate maps.
• TauCeti.E7Minuscule.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.E7Minuscule.hopfSpec_map_weightTorusIntegralCoordinateMap_op: the integral coordinate maps represent the existing numbered root-subgroup and weight-torus morphisms.
• TauCeti.E7Minuscule.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.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• B. Conrad, Reductive Group Schemes, §1.
• This formalization is adapted from TauCeti.Algebra.Lie.E6.Minuscule.BaseChange.

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

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.

@[reducible, inline]

noncomputable abbrev TauCeti.E7Minuscule.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.E7Minuscule.coordinateHopfAlgebra A = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 56) (TauCeti.E7Minuscule.baseChangeDefiningIdeal A)

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

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

Equations

• TauCeti.E7Minuscule.coordinateMap A = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 56) (TauCeti.E7Minuscule.baseChangeDefiningIdeal A)

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

The specialized carrier coordinate morphism is surjective.

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

The kernel of the specialized carrier coordinate morphism is the transported defining ideal: the morphism presents the carrier as the closed subgroup of GL₅₆ that ideal cuts out.

theorem TauCeti.E7Minuscule.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 56) (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.E7Minuscule.finiteTypeCoordinateHopfAlgebra (A : Type v) [CommRing A] : FiniteTypeCommHopfAlgCat A

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

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.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.E7Minuscule.mem_baseChangeDefiningIdeal_iff (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A 56)} : x ∈ baseChangeDefiningIdeal A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 56).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.E7Minuscule.map_tmul_mem_baseChangeDefiningIdeal_of_mem (A : Type v) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ 56)} (hy : y ∈ definingIdeal) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 56).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.E7Minuscule.baseChangeCoordinateIso (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 56) (baseChangeDefiningIdeal A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) 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.E7Minuscule.mkQuotient_comp_baseChangeCoordinateIso_hom (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 56) (baseChangeDefiningIdeal A)) (baseChangeCoordinateIso A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 56).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal))

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

The transported root subgroups

noncomputable def TauCeti.E7Minuscule.rootSubgroupIntegralCoordinateMap (k : Fin 7 ⊕ Fin 7) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) 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.E7Minuscule.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (k : Fin 7 ⊕ Fin 7) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal) (rootSubgroupIntegralCoordinateMap k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis

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

theorem TauCeti.E7Minuscule.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (k : Fin 7 ⊕ Fin 7) : (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.E7Minuscule.rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 7 ⊕ Fin 7) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 56) (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.E7Minuscule.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 7 ⊕ Fin 7) : CategoryTheory.CategoryStruct.comp (coordinateMap A) (rootSubgroupToBaseChangeCoordinateMap A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis A k

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

@[simp]

theorem TauCeti.E7Minuscule.pointToGeneralLinear_mapDomain_rootSubgroupToBaseChangeCoordinateMap_eq_rootSubgroupPoints (A : Type v) [CommRing A] (i : Fin 7 ⊕ Fin 7) (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : GeneralLinear.pointToGeneralLinear 56 ((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.E7Minuscule.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (A : Type v) [CommRing A] (k : Fin 7 ⊕ Fin 7) : 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.E7Minuscule.weightTorusIntegralCoordinateMap : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 7))).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.E7Minuscule.mkQuotient_comp_weightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal) weightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap DynkinType.e7MinusculeWeight

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

theorem TauCeti.E7Minuscule.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.E7Minuscule.weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 56) (baseChangeDefiningIdeal A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin 7))).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.E7Minuscule.coordinateMap_comp_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (coordinateMap A) (weightTorusToBaseChangeCoordinateMap A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A DynkinType.e7MinusculeWeight

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

@[simp]

theorem TauCeti.E7Minuscule.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.E7Minuscule.generatorCoordinateAlgebra (A : Type v) [CommRing A] : (Fin 7 ⊕ Fin 7) ⊕ Unit → CommHopfAlgCat A

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

Equations

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

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

@[simp]

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

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

@[simp]

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

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

theorem TauCeti.E7Minuscule.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 type-E₇ carrier.

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