Documentation

TauCeti.Algebra.Lie.E6.Minuscule.Generated.Basic

The subgroup generated by the type-E₆ minuscule roots and weight torus #

The twelve numbered simple-root subgroups and the rank-six weight torus of the full-weight type-E₆ minuscule carrier are morphisms into GL₂₇ over any commutative ring. The closed subgroup they generate is cut out by the largest Hopf ideal killed by all of them, that is by the common kernel of their coordinate maps.

This file names that ideal and the resulting coordinate Hopf algebra, and records the two facts a consumer needs about them: each generator factors uniquely through the quotient, and the quotient lies inside the base change of the integral carrier.

Equality of the generated subgroup with the base change of the integral carrier is not asserted: extra equations can appear after specialization to a non-flat base. Nor is the generated subgroup identified with a pinned simply connected group scheme of type E₆.

Main declarations #

Main results #

References #

The quotient presentation of the generated subgroup and its factorization API are adapted from the parallel type-E₇ construction in TauCeti.Algebra.Lie.E7.Minuscule.Generated.Basic, added in https://github.com/TauCetiProject/TauCeti/pull/9467.

source
noncomputable def TauCeti.E6Minuscule.generatedDefiningIdeal (A : Type v) [CommRing A] :
HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 27)

The defining ideal of the subgroup generated by the numbered root subgroups and the weight torus of the type-E₆ minuscule carrier.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.E6Minuscule.generatedDefiningIdeal_def (A : Type v) [CommRing A] :
    generatedDefiningIdeal A = CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap A)

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

    source
    theorem TauCeti.E6Minuscule.le_generatedDefiningIdeal_iff (A : Type v) [CommRing A] (J : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 27)) :
    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.

    source
    theorem TauCeti.E6Minuscule.generatedDefiningIdeal_toIdeal_le_ker (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) :
    (generatedDefiningIdeal A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (generatorCoordinateMap A j))).toRingHom

    Every generator coordinate map kills the generated defining ideal.

    source
    theorem TauCeti.E6Minuscule.baseChangeDefiningIdeal_le_generatedDefiningIdeal (A : Type v) [CommRing A] :
    baseChangeDefiningIdeal A ≤ generatedDefiningIdeal A

    The base-changed integral carrier contains the generated subgroup.

    source
    noncomputable def TauCeti.E6Minuscule.generatedCoordinateHopfAlgebra (A : Type v) [CommRing A] :
    CommHopfAlgCat A

    The coordinate Hopf algebra of the subgroup generated by the numbered root subgroups and the weight torus of the type-E₆ minuscule carrier.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.E6Minuscule.generatedCoordinateHopfAlgebra_def (A : Type v) [CommRing A] :
      generatedCoordinateHopfAlgebra A = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 27) (generatedDefiningIdeal A)

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

      source
      noncomputable def TauCeti.E6Minuscule.generatedCoordinateMap (A : Type v) [CommRing A] :
      GeneralLinear.coordinateHopfAlgebra A 27 ⟶ generatedCoordinateHopfAlgebra A

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

      Equations
      Instances For
        source
        theorem TauCeti.E6Minuscule.generatedCoordinateMap_surjective (A : Type v) [CommRing A] :
        Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (generatedCoordinateMap A))

        The generated subgroup coordinate morphism is surjective.

        source
        @[simp]
        theorem TauCeti.E6Minuscule.generatedCoordinateMap_ker (A : Type v) [CommRing A] :
        RingHom.ker (CommHopfAlgCat.Hom.hom (generatedCoordinateMap A)) = (generatedDefiningIdeal A).toIdeal

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

        source
        noncomputable def TauCeti.E6Minuscule.generatedCoordinateDesc (A : Type v) [CommRing A] {B : CommHopfAlgCat A} (f : GeneralLinear.coordinateHopfAlgebra A 27 ⟶ B) (hf : (generatedDefiningIdeal A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) :
        generatedCoordinateHopfAlgebra A ⟶ B

        A coordinate morphism out of O(GL₂₇) killing the generated subgroup's defining ideal, factored through the generated subgroup.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.E6Minuscule.generatedCoordinateMap_comp_generatedCoordinateDesc (A : Type v) [CommRing A] {B : CommHopfAlgCat A} (f : GeneralLinear.coordinateHopfAlgebra A 27 ⟶ B) (hf : (generatedDefiningIdeal A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) :
          CategoryTheory.CategoryStruct.comp (generatedCoordinateMap A) (generatedCoordinateDesc A f hf) = f

          Composing the quotient coordinate morphism with the descent morphism of f recovers f.

          source
          theorem TauCeti.E6Minuscule.generatedCoordinateDesc_unique (A : Type v) [CommRing A] {B : CommHopfAlgCat A} (f : GeneralLinear.coordinateHopfAlgebra A 27 ⟶ B) (hf : (generatedDefiningIdeal A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (g : generatedCoordinateHopfAlgebra A ⟶ B) (hg : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap A) g = f) :
          g = generatedCoordinateDesc A f hf

          The descent morphism is the unique factorization of f through the generated subgroup.

          source
          noncomputable def TauCeti.E6Minuscule.generatedCoordinateLift (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) :
          generatedCoordinateHopfAlgebra A ⟶ generatorCoordinateAlgebra A j

          The jth generator coordinate map factored through the generated subgroup.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.E6Minuscule.generatedCoordinateMap_comp_generatedCoordinateLift (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ Unit) :
            CategoryTheory.CategoryStruct.comp (generatedCoordinateMap A) (generatedCoordinateLift A j) = generatorCoordinateMap A j

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

            source
            theorem TauCeti.E6Minuscule.generatedCoordinateLift_unique (A : Type v) [CommRing A] (j : (Fin 6 ⊕ Fin 6) ⊕ 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.

            source
            instance TauCeti.E6Minuscule.instFiniteTypeXGeneratedCoordinateHopfAlgebra (A : Type v) [CommRing A] :
            Algebra.FiniteType A ↑(generatedCoordinateHopfAlgebra A)

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