The subgroup generated by the doubled type-E₆ roots and torus

The twelve numbered root subgroups and the weight torus of the doubled minuscule carrier specify a closed subgroup of GL₅₄. Its defining Hopf ideal is the common kernel of their coordinate maps. This module provides the generated subgroup's coordinate Hopf algebra and its basic comparison with the base-changed integral carrier.

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

The defining ideal of the subgroup generated by the numbered roots and weight torus.

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.le_generatedDefiningIdeal_iff (A : Type u) [CommRing A] (J : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 54)) : J ≤ generatedDefiningIdeal A ↔ ∀ (j : (Fin 6 ⊕ Fin 6) ⊕ 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.E6DoubledMinuscule.baseChangeDefiningIdeal_le_generatedDefiningIdeal (A : Type u) [CommRing A] : baseChangeDefiningIdeal A ≤ generatedDefiningIdeal A

The base-changed integral carrier contains the generated subgroup.

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

The coordinate Hopf algebra of the subgroup generated by the numbered roots and torus.

Equations

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

@[simp]

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

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

theorem TauCeti.E6DoubledMinuscule.existsUnique_generatorCoordinateMap_factor (A : Type u) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) : ∃! g : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 54) (generatedDefiningIdeal A) ⟶ generatorCoordinateAlgebra A j, CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 54) (generatedDefiningIdeal A)) g = generatorCoordinateMap A j

Each generator factors uniquely through the generated subgroup's coordinate quotient.