The subgroup generated by the type-E7 pinning candidates

The fourteen numbered root subgroups and the weight torus of the type-E₇ minuscule carrier generate a closed subgroup of GL₅₆. Its defining ideal is the common kernel of their coordinate maps. The integral carrier's base change contains this generated subgroup; equality with the integral carrier's fibre is a separate question.

The coordinate Hopf algebra here is the common target of the connectedness and smoothness results for the generated subgroup. Its quotient map from O(GL₅₆) and the factorizations of the generator coordinate maps through it are what its standard representation is built from.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26–27.
• J. S. Milne, Algebraic Groups (2017), §2.h.

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

The Hopf ideal defining the closed subgroup generated by the numbered root subgroups and weight torus of the type-E₇ minuscule carrier over A.

Equations

• TauCeti.E7Minuscule.generatedDefiningIdeal A = TauCeti.CommHopfAlgCat.commonKernelHopfIdeal (TauCeti.E7Minuscule.generatorCoordinateMap A)

@[simp]

theorem TauCeti.E7Minuscule.generatedDefiningIdeal_def (A : Type u) [CommRing A] : generatedDefiningIdeal A = CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap A)

The generated subgroup is defined by the common kernel of its generator maps.

theorem TauCeti.E7Minuscule.le_generatedDefiningIdeal_iff (A : Type u) [CommRing A] (J : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 56)) : J ≤ generatedDefiningIdeal A ↔ ∀ (j : (Fin 7 ⊕ Fin 7) ⊕ Unit), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (generatorCoordinateMap A j))).toRingHom

A Hopf ideal lies below the generated subgroup's defining ideal exactly when all generator coordinate maps kill it.

theorem TauCeti.E7Minuscule.baseChangeDefiningIdeal_le_generatedDefiningIdeal (A : Type u) [CommRing A] : baseChangeDefiningIdeal A ≤ generatedDefiningIdeal A

The base-changed integral carrier contains the subgroup generated by the numbered root subgroups and weight torus.

noncomputable def TauCeti.E7Minuscule.generatedCoordinateHopfAlgebra (A : Type u) [CommRing A] : CommHopfAlgCat A

The coordinate algebra of the closed subgroup generated by the numbered root subgroups and weight torus over A.

Equations

• TauCeti.E7Minuscule.generatedCoordinateHopfAlgebra A = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 56) (TauCeti.E7Minuscule.generatedDefiningIdeal A)

@[simp]

theorem TauCeti.E7Minuscule.generatedCoordinateHopfAlgebra_def (A : Type u) [CommRing A] : generatedCoordinateHopfAlgebra A = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 56) (generatedDefiningIdeal A)

The generated subgroup has the quotient coordinate Hopf algebra of its defining ideal.

noncomputable def TauCeti.E7Minuscule.generatedCoordinateMap (A : Type u) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A 56 ⟶ generatedCoordinateHopfAlgebra A

The quotient coordinate morphism O(GL₅₆) ⟶ O(generated subgroup), representing its closed immersion into GL₅₆.

Equations

• TauCeti.E7Minuscule.generatedCoordinateMap A = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 56) (TauCeti.E7Minuscule.generatedDefiningIdeal A)

theorem TauCeti.E7Minuscule.generatedCoordinateMap_surjective (A : Type u) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (generatedCoordinateMap A))

The generated subgroup coordinate morphism is surjective.

@[simp]

theorem TauCeti.E7Minuscule.generatedCoordinateMap_ker (A : Type u) [CommRing A] : RingHom.ker (CommHopfAlgCat.Hom.hom (generatedCoordinateMap A)) = (generatedDefiningIdeal A).toIdeal

The kernel of the generated subgroup coordinate morphism is its defining ideal.

theorem TauCeti.E7Minuscule.generatedDefiningIdeal_toIdeal_le_ker (A : Type u) [CommRing A] (j : (Fin 7 ⊕ Fin 7) ⊕ Unit) : (generatedDefiningIdeal A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (generatorCoordinateMap A j))).toRingHom

Every generator coordinate map kills the generated defining ideal.

noncomputable def TauCeti.E7Minuscule.generatedCoordinateLift (A : Type u) [CommRing A] (j : (Fin 7 ⊕ Fin 7) ⊕ Unit) : generatedCoordinateHopfAlgebra A ⟶ generatorCoordinateAlgebra A j

The jth generator coordinate map factored through the generated subgroup.

Equations

• TauCeti.E7Minuscule.generatedCoordinateLift A j = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.E7Minuscule.generatedDefiningIdeal A) (TauCeti.E7Minuscule.generatorCoordinateMap A j) ⋯

@[simp]

theorem TauCeti.E7Minuscule.generatedCoordinateMap_comp_generatedCoordinateLift (A : Type u) [CommRing A] (j : (Fin 7 ⊕ Fin 7) ⊕ Unit) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap A) (generatedCoordinateLift A j) = generatorCoordinateMap A j

Composing the quotient coordinate morphism with the jth lift recovers the generator.

theorem TauCeti.E7Minuscule.generatedCoordinateLift_unique (A : Type u) [CommRing A] (j : (Fin 7 ⊕ Fin 7) ⊕ Unit) (g : generatedCoordinateHopfAlgebra A ⟶ generatorCoordinateAlgebra A j) (hg : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap A) g = generatorCoordinateMap A j) : g = generatedCoordinateLift A j

The lift is the unique factorization of the jth generator coordinate map through the generated subgroup.

instance TauCeti.E7Minuscule.instFiniteTypeXGeneratedCoordinateHopfAlgebra (A : Type u) [CommRing A] : Algebra.FiniteType A ↑(generatedCoordinateHopfAlgebra A)

The generated coordinate Hopf algebra is a finite-type A-algebra.