Documentation

TauCeti.Algebra.Lie.D4.Tripled.GeneratedConnected

Connectedness of the subgroup generated by the tripled type-D₄ roots and torus #

Over a commutative ring, the eight numbered root subgroups and the rank-four weight torus of the tripled type-D₄ carrier define a closed subgroup of GL₂₄ by a common-kernel quotient of its coordinate Hopf algebra. Over an algebraically closed field, this subgroup is connected. The base-changed integral carrier contains it; equality of the two closed subgroups is a separate question.

Connectedness is one geometric input to identifying this explicit generated group with a pinned split reductive group, alongside the comparison with the integral carrier.

References #

source
noncomputable def TauCeti.D4Tripled.generatedDefiningIdeal (k : Type u) [CommRing k] :
HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 24)

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

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.D4Tripled.generatedDefiningIdeal_def (k : Type u) [CommRing k] :
    generatedDefiningIdeal k = CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap k)

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

    source
    theorem TauCeti.D4Tripled.le_generatedDefiningIdeal_iff (k : Type u) [CommRing k] (J : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 24)) :
    J ≤ generatedDefiningIdeal k ↔ ∀ (j : (Fin 4 ⊕ Fin 4) ⊕ Unit), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (generatorCoordinateMap k j))).toRingHom

    A Hopf ideal lies below the generated subgroup's defining ideal exactly when every generator coordinate map kills it.

    source
    theorem TauCeti.D4Tripled.baseChangeDefiningIdeal_le_generatedDefiningIdeal (k : Type u) [CommRing k] :
    baseChangeDefiningIdeal k ≤ generatedDefiningIdeal k

    The generated subgroup is contained in the base change of the integral carrier.

    source
    noncomputable def TauCeti.D4Tripled.generatedCoordinateHopfAlgebra (k : Type u) [CommRing k] :
    CommHopfAlgCat k

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

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.D4Tripled.generatedCoordinateHopfAlgebra_def (k : Type u) [CommRing k] :
      generatedCoordinateHopfAlgebra k = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k 24) (generatedDefiningIdeal k)

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

      source
      theorem TauCeti.D4Tripled.existsUnique_generatorCoordinateMap_factor (k : Type u) [CommRing k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) :
      ∃! g : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k 24) (generatedDefiningIdeal k) ⟶ generatorCoordinateAlgebra k j, CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k 24) (generatedDefiningIdeal k)) g = generatorCoordinateMap k j

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

      source
      theorem TauCeti.D4Tripled.geometricallyConnectedCommHopfAlgProperty_generatedCoordinateHopfAlgebra (k : Type u) [Field k] [IsAlgClosed k] :
      geometricallyConnectedCommHopfAlgProperty k (generatedCoordinateHopfAlgebra k)

      The generated closed subgroup is geometrically connected over an algebraically closed field.