Base change of the positive E7 minuscule subsystem

The positive subsystem of the integral type-E₇ minuscule carrier is generated by its seven positive simple-root subgroups and its weight torus. This file transports that coordinate presentation along ℤ → A for an arbitrary commutative ring A.

The resulting quotient coordinate Hopf algebra is canonically the scalar extension of the integral positive subsystem. The factored positive root-subgroup maps and weight-torus map are transported through the same comparison, so the carrier and the data intended for its pinning base-change together.

Main definitions

• TauCeti.E7Minuscule.positiveSubsystemBaseChangeIdeal: the transported positive-subsystem defining ideal.
• TauCeti.E7Minuscule.positiveSubsystemBaseChangeIso: the coordinate comparison with scalar extension of the integral positive subsystem.
• TauCeti.E7Minuscule.positiveRootSubgroupIntegralCoordinateMap and TauCeti.E7Minuscule.positiveWeightTorusIntegralCoordinateMap: the integral factored generator maps.
• TauCeti.E7Minuscule.positiveRootSubgroupBaseChangeCoordinateMap and TauCeti.E7Minuscule.positiveWeightTorusBaseChangeCoordinateMap: their transported maps.
• TauCeti.E7Minuscule.positiveRootSubgroupBaseChange and TauCeti.E7Minuscule.positiveWeightTorusBaseChange: the corresponding scheme morphisms over the new base.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4.
• B. Conrad, Reductive Group Schemes, §1.

@[reducible, inline]

noncomputable abbrev TauCeti.E7Minuscule.positiveSubsystemCoordinateHopfAlgebra : CommHopfAlgCat ℤ

The coordinate Hopf algebra of the integral positive subsystem, in its generated-subsystem presentation.

Equations

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

theorem TauCeti.E7Minuscule.positiveSubsystemCoordinateHopfAlgebra_eq : positiveSubsystemCoordinateHopfAlgebra = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) positiveSubsystemDefiningIdeal

The generated-subsystem presentation uses the named positive-subsystem defining ideal.

noncomputable def TauCeti.E7Minuscule.positiveSubsystemBaseChangeIdeal (A : Type v) [CommRing A] : HopfIdeal A ↑(CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56))

The scalar extension to A of the defining ideal of the integral positive subsystem.

Equations

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

noncomputable def TauCeti.E7Minuscule.positiveSubsystemBaseChangeIso (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A) ≅ CommHopfAlgCat.baseChange positiveSubsystemCoordinateHopfAlgebra

Quotienting by the transported positive-subsystem ideal agrees with scalar extension of its integral coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.mkQuotient_comp_positiveSubsystemBaseChangeIso_hom (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A)) (positiveSubsystemBaseChangeIso A).hom = CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) (UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯))

The positive-subsystem base-change comparison respects the ambient quotient presentation.

Positive simple-root subgroups

noncomputable def TauCeti.E7Minuscule.positiveRootSubgroupIntegralCoordinateMap (i : Fin 7) : positiveSubsystemCoordinateHopfAlgebra ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate map of the ith positive simple-root subgroup factored through the integral positive subsystem.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.mkQuotient_comp_positiveRootSubgroupIntegralCoordinateMap (i : Fin 7) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) (UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯)) (positiveRootSubgroupIntegralCoordinateMap i) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice (Sum.inl i) ⋯ latticeBasis

The integral factored positive root-subgroup map recovers its represented coordinate map in GL₅₆.

theorem TauCeti.E7Minuscule.hopfSpec_map_positiveRootSubgroupIntegralCoordinateMap_op (i : Fin 7) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (positiveRootSubgroupIntegralCoordinateMap i).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) (CategoryTheory.eqToHom positiveSubsystemGroupScheme_def))

The integral factored coordinate map represents the existing ith positive simple-root subgroup of the positive subsystem.

noncomputable def TauCeti.E7Minuscule.positiveRootSubgroupBaseChangeCoordinateMap (A : Type v) [CommRing A] (i : Fin 7) : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A) ⟶ CommHopfAlgCat.baseChange (AdditiveGroup.coordinateHopfAlgebra ℤ)

The coordinate map of the ith positive simple-root subgroup after base change to A.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.mkQuotient_comp_positiveRootSubgroupBaseChangeCoordinateMap (A : Type v) [CommRing A] (i : Fin 7) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A)) (positiveRootSubgroupBaseChangeCoordinateMap A i) = CommHopfAlgCat.baseChangeMap (UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice (Sum.inl i) ⋯ latticeBasis)

The transported positive root-subgroup factorization recovers the scalar extension of its ambient integral coordinate map.

The positive weight torus

noncomputable def TauCeti.E7Minuscule.positiveWeightTorusIntegralCoordinateMap : positiveSubsystemCoordinateHopfAlgebra ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 7))).obj

The coordinate map of the weight torus factored through the integral positive subsystem.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.mkQuotient_comp_positiveWeightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) (UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯)) positiveWeightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap DynkinType.e7MinusculeWeight

The integral factored positive weight-torus map recovers its represented coordinate map in GL₅₆.

theorem TauCeti.E7Minuscule.hopfSpec_map_positiveWeightTorusIntegralCoordinateMap_op : (AlgebraicGeometry.hopfSpec ↧ℤ).map positiveWeightTorusIntegralCoordinateMap.op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp positiveWeightTorus (CategoryTheory.eqToHom positiveSubsystemGroupScheme_def))

The integral factored coordinate map represents the existing weight torus of the positive subsystem.

noncomputable def TauCeti.E7Minuscule.positiveWeightTorusBaseChangeCoordinateMap (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A) ⟶ CommHopfAlgCat.baseChange (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 7))).obj

The coordinate map of the positive subsystem's weight torus after base change to A.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.mkQuotient_comp_positiveWeightTorusBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ 56)) (positiveSubsystemBaseChangeIdeal A)) (positiveWeightTorusBaseChangeCoordinateMap A) = CommHopfAlgCat.baseChangeMap (GeneralLinear.weightTorusCoordinateMap DynkinType.e7MinusculeWeight)

The transported positive weight-torus factorization recovers the scalar extension of its ambient integral coordinate map.

Scheme morphisms over the new base

@[reducible, inline]

noncomputable abbrev TauCeti.E7Minuscule.positiveSubsystemBaseChangeGroupScheme (B : Type) [CommRing B] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧B))

The positive subsystem after base change, in its transported quotient presentation.

Equations

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

noncomputable def TauCeti.E7Minuscule.positiveRootSubgroupBaseChange (B : Type) [CommRing B] (i : Fin 7) : AdditiveGroup.groupScheme B ⟶ positiveSubsystemBaseChangeGroupScheme B

The ith transported positive simple-root morphism from the named additive group over A. Its coordinate map is the transported factorization followed by the canonical identification of the scalar extension of O(𝔾ₐ) with O(𝔾ₐ/A).

Equations

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

theorem TauCeti.E7Minuscule.hopfSpec_map_positiveRootSubgroupBaseChangeCoordinateMap_op (B : Type) [CommRing B] (i : Fin 7) : (AlgebraicGeometry.hopfSpec ↧B).map (CategoryTheory.CategoryStruct.comp (positiveRootSubgroupBaseChangeCoordinateMap B i) (AdditiveGroup.coordinateHopfAlgebraBaseChangeIso ℤ B).hom).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (positiveRootSubgroupBaseChange B i)

The coordinate map underlying the transported positive simple-root scheme morphism is the transported factorization, followed by the standard additive-group base-change comparison.

noncomputable def TauCeti.E7Minuscule.positiveWeightTorusBaseChange (B : Type) [CommRing B] : SplitTorus.groupScheme B (Fin 7) ⟶ positiveSubsystemBaseChangeGroupScheme B

The transported positive weight-torus morphism from the named split torus over A. Its coordinate map is the transported factorization followed by the canonical diagonalizable-group base-change comparison.

Equations

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

theorem TauCeti.E7Minuscule.hopfSpec_map_positiveWeightTorusBaseChangeCoordinateMap_op (B : Type) [CommRing B] : (AlgebraicGeometry.hopfSpec ↧B).map (CategoryTheory.CategoryStruct.comp (positiveWeightTorusBaseChangeCoordinateMap B) (DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso ℤ B (SplitTorus.characterGroup (Fin 7))).hom).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (positiveWeightTorusBaseChange B)

The coordinate map underlying the transported positive weight-torus scheme morphism is the transported factorization, followed by the standard diagonalizable-group base-change comparison.