The positive subsystem of the E7 minuscule carrier

This file constructs the closed subgroup scheme of the type-E₇ minuscule carrier generated by the seven positive simple-root subgroups and the weight torus. The explicit ordering of the fifty-six 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.E7Minuscule.positiveSubsystemGroupScheme: the torus-plus-positive-simple-root subgroup scheme.
• TauCeti.E7Minuscule.positiveSubsystemInclusion: its closed immersion into the full minuscule carrier.
• TauCeti.E7Minuscule.positiveRootSubgroup: a positive simple-root subgroup factored through the positive subsystem.
• TauCeti.E7Minuscule.positiveWeightTorus: the weight torus factored through the positive subsystem.
• TauCeti.E7Minuscule.positiveSubsystemToUpperTriangular: its canonical upper-triangular realization.

Main results

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

References

• 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.E7Minuscule.positiveSimpleRoots : Set (Fin 7 ⊕ Fin 7)

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

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.inl_mem_positiveSimpleRoots (i : Fin 7) : Sum.inl i ∈ positiveSimpleRoots

@[simp]

theorem TauCeti.E7Minuscule.inr_not_mem_positiveSimpleRoots (i : Fin 7) : Sum.inr i ∉ positiveSimpleRoots

theorem TauCeti.E7Minuscule.positiveRootWeight_strict (k : Fin 7 ⊕ Fin 7) (hk : k ∈ positiveSimpleRoots) {r s : Fin 56} {m : ℕ} (hm : 0 < m) (hrs : DynkinType.e7MinusculeWeight r = DynkinType.e7MinusculeWeight s + m • (fun (k : Fin 7 ⊕ Fin 7) (j : Fin 7) => DynkinType.E7.rootGeneratorWeight DynkinType.valid_E7 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.E7Minuscule.positiveSubsystemDefiningIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 56)

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.E7Minuscule.positiveSubsystemDefiningIdeal_def : positiveSubsystemDefiningIdeal = UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯

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

theorem TauCeti.E7Minuscule.le_positiveSubsystemDefiningIdeal_iff (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 56)) : J ≤ positiveSubsystemDefiningIdeal ↔ (∀ (i : Fin 7), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice (Sum.inl i) ⋯ latticeBasis))).toRingHom) ∧ J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap DynkinType.e7MinusculeWeight))).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.E7Minuscule.positiveSubsystemGroupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

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

Equations

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

theorem TauCeti.E7Minuscule.positiveSubsystemGroupScheme_def : positiveSubsystemGroupScheme = UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯

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

theorem TauCeti.E7Minuscule.positiveSubsystemGroupScheme_eq_quotientSpec : positiveSubsystemGroupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 56) positiveSubsystemDefiningIdeal

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

noncomputable def TauCeti.E7Minuscule.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.E7Minuscule.positiveSubsystemInclusion_comp_carrierι : CategoryTheory.CategoryStruct.comp positiveSubsystemInclusion carrierι = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom positiveSubsystemGroupScheme_def) (UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupSchemeι (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯)

Including the positive subsystem into the carrier and then into GL₅₆ recovers its direct Kostant subsystem inclusion.

instance TauCeti.E7Minuscule.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.E7Minuscule.positiveSubsystemClosedSubgroup : ClosedSubgroupScheme groupScheme

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

Equations

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

@[simp]

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

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

theorem TauCeti.E7Minuscule.positiveSubsystemClosedSubgroup_eq_kostantTorusSubsystemClosedSubgroup : positiveSubsystemClosedSubgroup = UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight isNilpotent_rep_serreRootGenerator positiveSimpleRoots

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

noncomputable def TauCeti.E7Minuscule.positiveRootSubgroup (i : Fin 7) : 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.E7Minuscule.positiveRootSubgroup_def (i : Fin 7) : positiveRootSubgroup i = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯ ⋯) (CategoryTheory.eqToHom ⋯)

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

@[simp]

theorem TauCeti.E7Minuscule.positiveRootSubgroup_comp_positiveSubsystemInclusion (i : Fin 7) : 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.E7Minuscule.isClosedImmersion_positiveRootSubgroup (i : Fin 7) : 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.E7Minuscule.positiveWeightTorus : SplitTorus.groupScheme ℤ (Fin 7) ⟶ 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.E7Minuscule.positiveWeightTorus_def : positiveWeightTorus = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice latticeBasis DynkinType.e7MinusculeWeight positiveSimpleRoots ⋯) (CategoryTheory.eqToHom ⋯)

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

@[simp]

theorem TauCeti.E7Minuscule.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.E7Minuscule.isClosedImmersion_positiveWeightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left positiveWeightTorus.hom.hom)

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

theorem TauCeti.E7Minuscule.positiveSubsystemClosedSubgroup_le_iff (P : ClosedSubgroupScheme groupScheme) : positiveSubsystemClosedSubgroup ≤ P ↔ (∀ (i : Fin 7), ∃! f : AdditiveGroup.groupScheme ℤ ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = rootSubgroup (Sum.inl i)) ∧ ∃! f : SplitTorus.groupScheme ℤ (Fin 7) ⟶ 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.E7Minuscule.positiveSubsystemGroupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (φ ψ : positiveSubsystemGroupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin 7), 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.E7Minuscule.positiveSubsystemGroupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {φ ψ : positiveSubsystemGroupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : φ = ψ ↔ (∀ (i : Fin 7), 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.E7Minuscule.positiveSubsystemToUpperTriangular : positiveSubsystemGroupScheme ⟶ GeneralLinear.UpperTriangular.groupScheme ℤ 56

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.E7Minuscule.positiveSubsystemToUpperTriangular_comp_inclusion : CategoryTheory.CategoryStruct.comp positiveSubsystemToUpperTriangular (GeneralLinear.UpperTriangular.inclusion ℤ 56) = CategoryTheory.CategoryStruct.comp positiveSubsystemInclusion carrierι

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

instance TauCeti.E7Minuscule.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.E7Minuscule.isSolvable_points_positiveSubsystem (A : Type v) [CommRing A] : Group.IsSolvable ↑(HopfAlgebra.points ↧A)

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