The positive subsystem of the E6 minuscule carrier

This file constructs the closed subgroup scheme of the type-E₆ minuscule carrier generated by the six positive simple-root subgroups and the weight torus. The explicit ordering of the twenty-seven minuscule weights puts every raising root operator above the diagonal. Consequently the positive subsystem is a closed subgroup of the standard upper-triangular group scheme, and all of its algebra-valued point groups are solvable.

This is the scheme-theoretic candidate for the Borel member of a pinning. It is not called a Borel subgroup here: smoothness, connectedness, and maximality among solvable subgroup schemes remain to be proved.

Main definitions

• TauCeti.E6Minuscule.positiveSubsystemGroupScheme: the torus-plus-positive-simple-root subgroup scheme.
• TauCeti.E6Minuscule.positiveSubsystemInclusion: its closed immersion into the full minuscule carrier.
• TauCeti.E6Minuscule.positiveRootSubgroup: a positive simple-root subgroup factored through the positive subsystem.
• TauCeti.E6Minuscule.positiveWeightTorus: the weight torus factored through the positive subsystem.
• TauCeti.E6Minuscule.positiveSubsystemToUpperTriangular: its canonical upper-triangular realization.

Main results

• TauCeti.E6Minuscule.positiveRootWeight_strict: positive simple roots strictly raise the explicit ordering of minuscule weights.
• TauCeti.E6Minuscule.isSolvable_points_positiveSubsystem: every algebra-valued point group of the positive subsystem is solvable.

References

• The type-E₇ positive subsystem construction in TauCeti.Algebra.Lie.E7.Minuscule, introduced in TauCetiProject/TauCeti#9054, for the interface and proof organization specialized here.
• J. E. Humphreys, Linear Algebraic Groups, Sections 26--28.
• R. W. Carter, Simple Groups of Lie Type, Sections 4.4 and 8.2.

The positive weight order

def TauCeti.E6Minuscule.positiveSimpleRoots : Set (Fin 6 ⊕ Fin 6)

The numbered positive simple roots among the twelve signed simple-root generators.

Equations

• TauCeti.E6Minuscule.positiveSimpleRoots = Set.range Sum.inl

@[simp]

theorem TauCeti.E6Minuscule.inl_mem_positiveSimpleRoots (i : Fin 6) : Sum.inl i ∈ positiveSimpleRoots

@[simp]

theorem TauCeti.E6Minuscule.inr_not_mem_positiveSimpleRoots (i : Fin 6) : Sum.inr i ∉ positiveSimpleRoots

theorem TauCeti.E6Minuscule.positiveRootWeight_strict (k : Fin 6 ⊕ Fin 6) (hk : k ∈ positiveSimpleRoots) {r s : Fin 27} {m : ℕ} (hm : 0 < m) (hrs : weightTable.weight r = weightTable.weight s + m • (fun (k : Fin 6 ⊕ Fin 6) (j : Fin 6) => E6.rootGeneratorWeight k j) k) : r < s

Every positive simple root strictly raises the ordered minuscule weight basis. If two weights differ by a positive multiple of a positive simple root, the raised weight occurs earlier in the explicit table.

The positive subsystem and its generators

noncomputable def TauCeti.E6Minuscule.positiveSubsystemDefiningIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 27)

The Hopf ideal cutting out the positive subsystem inside GL₂₇.

Equations

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

theorem TauCeti.E6Minuscule.positiveSubsystemDefiningIdeal_def : positiveSubsystemDefiningIdeal = UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯

The positive subsystem defining ideal is the generic torus-subsystem common-kernel ideal.

theorem TauCeti.E6Minuscule.le_positiveSubsystemDefiningIdeal_iff (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 27)) : J ≤ positiveSubsystemDefiningIdeal ↔ (∀ (i : Fin 6), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (Sum.inl i) ⋯ (coordinateLatticeBasis (Fin 27))))).toRingHom) ∧ J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap weightTable.weight))).toRingHom

Coordinate universal property of the positive subsystem. A Hopf ideal is contained in the positive defining ideal exactly when every positive simple-root coordinate map and the weight torus coordinate map kill it.

noncomputable def TauCeti.E6Minuscule.positiveSubsystemGroupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The positive subsystem of the type-E₆ minuscule carrier, generated by the six positive simple-root subgroups and the represented weight torus.

Equations

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

theorem TauCeti.E6Minuscule.positiveSubsystemGroupScheme_def : positiveSubsystemGroupScheme = UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯

The positive carrier is the generic Kostant torus-subsystem for the positive simple roots.

theorem TauCeti.E6Minuscule.positiveSubsystemGroupScheme_eq_quotientSpec : positiveSubsystemGroupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 27) positiveSubsystemDefiningIdeal

The positive subsystem is the quotient spectrum cut out by its named defining ideal.

noncomputable def TauCeti.E6Minuscule.positiveSubsystemInclusion : positiveSubsystemGroupScheme ⟶ groupScheme

The canonical inclusion of the positive subsystem into the full minuscule carrier.

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.positiveSubsystemInclusion_comp_carrierι : CategoryTheory.CategoryStruct.comp positiveSubsystemInclusion carrierι = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom positiveSubsystemGroupScheme_def) (UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupSchemeι (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯)

Including the positive subsystem into the carrier and then into GL₂₇ recovers its direct Kostant subsystem inclusion.

instance TauCeti.E6Minuscule.isClosedImmersion_positiveSubsystemInclusion : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left positiveSubsystemInclusion.hom.hom)

The positive subsystem is a closed subgroup scheme of the full minuscule carrier.

noncomputable def TauCeti.E6Minuscule.positiveSubsystemClosedSubgroup : ClosedSubgroupScheme groupScheme

The positive subsystem bundled as a closed subgroup scheme of the full minuscule carrier.

Equations

• TauCeti.E6Minuscule.positiveSubsystemClosedSubgroup = TauCeti.ClosedSubgroupScheme.mk TauCeti.E6Minuscule.positiveSubsystemInclusion

@[simp]

theorem TauCeti.E6Minuscule.coe_positiveSubsystemClosedSubgroup : ↑positiveSubsystemClosedSubgroup = CategoryTheory.Subobject.mk positiveSubsystemInclusion

The underlying subobject of the positive subsystem is represented by its canonical inclusion.

theorem TauCeti.E6Minuscule.positiveSubsystemClosedSubgroup_eq_kostantTorusSubsystemClosedSubgroup : positiveSubsystemClosedSubgroup = UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight ⋯ positiveSimpleRoots

The named positive closed subgroup agrees with the generic Kostant torus subsystem.

noncomputable def TauCeti.E6Minuscule.positiveRootSubgroup (i : Fin 6) : AdditiveGroup.groupScheme ℤ ⟶ positiveSubsystemGroupScheme

The i-th positive simple-root subgroup factored through the positive subsystem.

Equations

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

theorem TauCeti.E6Minuscule.positiveRootSubgroup_def (i : Fin 6) : positiveRootSubgroup i = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯ ⋯) (CategoryTheory.eqToHom ⋯)

The positive simple-root subgroup is the corresponding generic Kostant subsystem map, transported to the named positive carrier.

@[simp]

theorem TauCeti.E6Minuscule.positiveRootSubgroup_comp_positiveSubsystemInclusion (i : Fin 6) : CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) positiveSubsystemInclusion = rootSubgroup (Sum.inl i)

Factoring a positive root subgroup through the positive subsystem and including it into the full carrier recovers the named root subgroup.

instance TauCeti.E6Minuscule.isClosedImmersion_positiveRootSubgroup (i : Fin 6) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (positiveRootSubgroup i).hom.hom)

Every positive simple-root map into the positive subsystem is a closed immersion.

noncomputable def TauCeti.E6Minuscule.positiveWeightTorus : SplitTorus.groupScheme ℤ (Fin 6) ⟶ positiveSubsystemGroupScheme

The represented weight torus factored through the positive subsystem.

Equations

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

theorem TauCeti.E6Minuscule.positiveWeightTorus_def : positiveWeightTorus = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight positiveSimpleRoots ⋯) (CategoryTheory.eqToHom ⋯)

The positive weight torus is the generic Kostant subsystem torus map, transported to the named positive carrier.

@[simp]

theorem TauCeti.E6Minuscule.positiveWeightTorus_comp_positiveSubsystemInclusion : CategoryTheory.CategoryStruct.comp positiveWeightTorus positiveSubsystemInclusion = weightTorus

Factoring the weight torus through the positive subsystem and including it into the full carrier recovers the named weight torus.

instance TauCeti.E6Minuscule.isClosedImmersion_positiveWeightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left positiveWeightTorus.hom.hom)

The weight torus is a closed subgroup of the positive subsystem.

theorem TauCeti.E6Minuscule.positiveSubsystemClosedSubgroup_le_iff (P : ClosedSubgroupScheme groupScheme) : positiveSubsystemClosedSubgroup ≤ P ↔ (∀ (i : Fin 6), ∃! f : AdditiveGroup.groupScheme ℤ ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = rootSubgroup (Sum.inl i)) ∧ ∃! f : SplitTorus.groupScheme ℤ (Fin 6) ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = weightTorus

Universal property of the positive subsystem. It is the smallest closed subgroup scheme of the full minuscule carrier through which every positive simple-root subgroup and the weight torus factor.

theorem TauCeti.E6Minuscule.positiveSubsystemGroupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (φ ψ : positiveSubsystemGroupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin 6), CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) φ = CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) ψ) (htorus : CategoryTheory.CategoryStruct.comp positiveWeightTorus φ = CategoryTheory.CategoryStruct.comp positiveWeightTorus ψ) : φ = ψ

Rigidity of the positive subsystem. Two homomorphisms from it into an affine group scheme represented by a commutative Hopf algebra are equal if they agree on every positive simple-root subgroup and on the weight torus.

theorem TauCeti.E6Minuscule.positiveSubsystemGroupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {φ ψ : positiveSubsystemGroupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : φ = ψ ↔ (∀ (i : Fin 6), CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) φ = CategoryTheory.CategoryStruct.comp (positiveRootSubgroup i) ψ) ∧ CategoryTheory.CategoryStruct.comp positiveWeightTorus φ = CategoryTheory.CategoryStruct.comp positiveWeightTorus ψ

Upper-triangularity and solvability

noncomputable def TauCeti.E6Minuscule.positiveSubsystemToUpperTriangular : positiveSubsystemGroupScheme ⟶ GeneralLinear.UpperTriangular.groupScheme ℤ 27

The canonical closed immersion of the positive subsystem into the standard upper-triangular group scheme.

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.positiveSubsystemToUpperTriangular_comp_inclusion : CategoryTheory.CategoryStruct.comp positiveSubsystemToUpperTriangular (GeneralLinear.UpperTriangular.inclusion ℤ 27) = CategoryTheory.CategoryStruct.comp positiveSubsystemInclusion carrierι

The positive subsystem's upper-triangular realization recovers its direct inclusion into GL₂₇.

instance TauCeti.E6Minuscule.isClosedImmersion_positiveSubsystemToUpperTriangular : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left positiveSubsystemToUpperTriangular.hom.hom)

The positive subsystem is a closed subgroup scheme of the standard upper-triangular group.

theorem TauCeti.E6Minuscule.isSolvable_points_positiveSubsystem (A : Type v) [CommRing A] : Group.IsSolvable ↑(HopfAlgebra.points ↧A)

Every algebra-valued point group of the positive subsystem is solvable.