Base change of the positive E6 minuscule subsystem

The positive subsystem of the integral type-E₆ minuscule carrier is generated by its six 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.E6Minuscule.positiveRootSubgroupIntegralCoordinateMap and TauCeti.E6Minuscule.positiveWeightTorusIntegralCoordinateMap: the integral factored generator maps.
• TauCeti.E6Minuscule.positiveSubsystemBaseChangeGroupScheme: the scheme-theoretic base change of the integral positive subsystem.
• TauCeti.E6Minuscule.positiveSubsystemBaseChangePresentationIso: its identification with the generic transported quotient presentation.
• TauCeti.E6Minuscule.positiveRootSubgroupBaseChange and TauCeti.E6Minuscule.positiveWeightTorusBaseChange: the base changes of the integral pinning morphisms.

References

• The type-E₇ base-change construction in TauCeti.Algebra.Lie.E7.Minuscule.PositiveSubsystem.BaseChange for the interface specialized here.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• B. Conrad, Reductive Group Schemes, §1.

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.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.E6Minuscule.positiveSubsystemCoordinateHopfAlgebra_eq : positiveSubsystemCoordinateHopfAlgebra = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) positiveSubsystemDefiningIdeal

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

Positive simple-root subgroups

noncomputable def TauCeti.E6Minuscule.positiveRootSubgroupIntegralCoordinateMap (i : Fin 6) : 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.E6Minuscule.mkQuotient_comp_positiveRootSubgroupIntegralCoordinateMap (i : Fin 6) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) (UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯)) (positiveRootSubgroupIntegralCoordinateMap i) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (Sum.inl i) ⋯ (coordinateLatticeBasis (Fin 27))

The integral factored positive root-subgroup map recovers its represented coordinate map in GL₂₇.

theorem TauCeti.E6Minuscule.hopfSpec_map_positiveRootSubgroupIntegralCoordinateMap_op (i : Fin 6) : (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.

The positive weight torus

noncomputable def TauCeti.E6Minuscule.positiveWeightTorusIntegralCoordinateMap : positiveSubsystemCoordinateHopfAlgebra ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 6))).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.E6Minuscule.mkQuotient_comp_positiveWeightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 27) (UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯)) positiveWeightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap weightTable.weight

The integral factored positive weight-torus map recovers its represented coordinate map in GL₂₇.

theorem TauCeti.E6Minuscule.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.

Scheme morphisms over the new base

@[reducible, inline]

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

The scheme-theoretic base change of the integral positive subsystem to B.

Equations

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

@[reducible, inline]

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

The generic transported quotient presentation of the positive subsystem over B.

Equations

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

noncomputable def TauCeti.E6Minuscule.positiveSubsystemBaseChangePresentationIso (B : Type) [CommRing B] : positiveSubsystemBaseChangeGroupScheme B ≅ positiveSubsystemBaseChangePresentation B

The scheme-theoretic base change of the positive subsystem is represented by the generic transported quotient presentation.

Equations

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

noncomputable def TauCeti.E6Minuscule.positiveRootSubgroupDomainBaseChangeIso (B : Type) [CommRing B] : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℤ B)))).mapGrp.obj (AdditiveGroup.groupScheme ℤ) ≅ AdditiveGroup.groupScheme B

The canonical comparison from the scheme-theoretic base change of the integral additive group to the additive group constructed over B.

Equations

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

noncomputable def TauCeti.E6Minuscule.positiveWeightTorusDomainBaseChangeIso (B : Type) [CommRing B] : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℤ B)))).mapGrp.obj (SplitTorus.groupScheme ℤ (Fin 6)) ≅ SplitTorus.groupScheme B (Fin 6)

The canonical comparison from the scheme-theoretic base change of the integral split torus to the split torus constructed over B.

Equations

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

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

The ith positive simple-root morphism after scheme-theoretic base change to B.

Equations

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

theorem TauCeti.E6Minuscule.positiveRootSubgroupBaseChange_comp_presentationIso (B : Type) [CommRing B] (i : Fin 6) : CategoryTheory.CategoryStruct.comp (positiveRootSubgroupDomainBaseChangeIso B).hom (CategoryTheory.CategoryStruct.comp (positiveRootSubgroupBaseChange B i) (positiveSubsystemBaseChangePresentationIso B).hom) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℤ B)))).mapGrp.map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso (AdditiveGroup.coordinateHopfAlgebra ℤ)).hom ((AlgebraicGeometry.hopfSpec ↧B).map (CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIso (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯ B).hom (CommHopfAlgCat.baseChangeMap (UniversalEnvelopingAlgebra.kostantRootSubgroupTorusSubsystemCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯ ⋯))).op))

The quotient-presentation comparison identifies the scheme-theoretic base change of the ith positive simple-root morphism with scalar extension of its integral coordinate map.

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

The positive weight-torus morphism after scheme-theoretic base change to B.

Equations

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

theorem TauCeti.E6Minuscule.positiveWeightTorusBaseChange_comp_presentationIso (B : Type) [CommRing B] : CategoryTheory.CategoryStruct.comp (positiveWeightTorusDomainBaseChangeIso B).hom (CategoryTheory.CategoryStruct.comp (positiveWeightTorusBaseChange B) (positiveSubsystemBaseChangePresentationIso B).hom) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℤ B)))).mapGrp.map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 6))).obj).hom ((AlgebraicGeometry.hopfSpec ↧B).map (CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIso (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯ B).hom (CommHopfAlgCat.baseChangeMap (UniversalEnvelopingAlgebra.kostantWeightTorusTorusSubsystemCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯))).op))

Under the quotient-presentation comparison, the base-changed positive weight torus is the generic transported factorization.