Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.PrimeField.PointsFunctor

Points of the short-root type-F4 prime-field carrier #

The prime-field carrier is the subgroup scheme generated by the reduced simple-root subgroups and weight torus. This file realizes its points as matrices, identifies the pinned points with the corresponding integral formulas, proves their pinning equation, and transports the generic Hopf-ideal point functor through the named carrier presentation.

Main declarations #

The carrier remains distinct from the base change of the integral toral closure: only the proven one-way ideal and point containments are used here.

References #

Matrix-valued points #

source
noncomputable def TauCeti.F4ShortRoot.PrimeField.points (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
Subgroup (GL (Fin 26) A)

The matrix-valued points of the short-root type-Fโ‚„ carrier over ๐”ฝโ‚‚.

Equations
Instances For
    source
    theorem TauCeti.F4ShortRoot.PrimeField.points_def (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
    points A = GeneralLinear.generatedPointsSubgroup 26 generator A

    The points of the carrier over ๐”ฝโ‚‚ are the points of the subgroup scheme generated by the reduced generators.

    source
    theorem TauCeti.F4ShortRoot.PrimeField.points_eq_hopfIdealPointsSubgroup (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
    points A = GeneralLinear.hopfIdealPointsSubgroup 26 definingIdeal A

    The points of the carrier over ๐”ฝโ‚‚ are cut out by its defining Hopf ideal.

    source
    @[simp]
    theorem TauCeti.F4ShortRoot.PrimeField.mem_points_iff (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (g : GL (Fin 26) A) :
    g โˆˆ points A โ†” โˆ€ x โˆˆ definingIdeal, ((GeneralLinear.pointsMulEquiv 26).symm g).ofConv x = 0

    A matrix is a point of the carrier over ๐”ฝโ‚‚ exactly when its associated convolution point kills the carrier's defining Hopf ideal.

    source
    theorem TauCeti.F4ShortRoot.PrimeField.points_le_baseChangePresentationPoints (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
    points A โ‰ค GeneralLinear.hopfIdealPointsSubgroup 26 (UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator CartanMatrix.Fโ‚„.transpose) (serreH โ„š CartanMatrix.Fโ‚„.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.f4ShortRootWeight (ZMod 2)) A

    Every point of the carrier over ๐”ฝโ‚‚ is a point of the base change of the integral short-root carrier.

    source
    noncomputable def TauCeti.F4ShortRoot.PrimeField.rootSubgroupPoints (k : Fin 4 โŠ• Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
    Multiplicative A โ†’* โ†ฅ(points A)

    The parametrized numbered simple root subgroup inside the points of the carrier over ๐”ฝโ‚‚.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.F4ShortRoot.PrimeField.coe_rootSubgroupPoints (k : Fin 4 โŠ• Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (u : Multiplicative A) :
      โ†‘((rootSubgroupPoints k A) u) = โ†‘((F4ShortRoot.rootSubgroupPoints k A) u)

      A numbered simple-root point of the carrier over ๐”ฝโ‚‚ is the corresponding point of the integral carrier, as a matrix.

      source
      theorem TauCeti.F4ShortRoot.PrimeField.coe_rootSubgroupPoints_gaPointsMulEquiv (k : Fin 4 โŠ• Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (q : โ†‘(HopfAlgebra.points โ†งA)) :
      โ†‘((rootSubgroupPoints k A) (AdditiveGroup.gaPointsMulEquiv q)) = (GeneralLinear.pointsMulEquiv 26) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (generator (Sum.inl k))).app โ†งA)) q)

      A numbered simple-root point of the carrier over ๐”ฝโ‚‚ is the image of the corresponding point of ๐”พโ‚ under the generating coordinate map.

      source
      noncomputable def TauCeti.F4ShortRoot.PrimeField.weightTorusPoints (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
      (Fin 4 โ†’ Aหฃ) โ†’* โ†ฅ(points A)

      The split weight torus inside the points of the carrier over ๐”ฝโ‚‚.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.F4ShortRoot.PrimeField.coe_weightTorusPoints (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 โ†’ Aหฃ) :
        โ†‘((weightTorusPoints A) s) = โ†‘((F4ShortRoot.weightTorusPoints A) s)

        A weight-torus point of the carrier over ๐”ฝโ‚‚ is the corresponding point of the integral carrier, as a matrix.

        source
        theorem TauCeti.F4ShortRoot.PrimeField.coe_weightTorusPoints_pointsMulEquiv (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (q : โ†‘(HopfAlgebra.points โ†งA)) :
        โ†‘((weightTorusPoints A) (SplitTorus.pointsMulEquiv q)) = (GeneralLinear.pointsMulEquiv 26) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (generator (Sum.inr ()))).app โ†งA)) q)

        A weight-torus point of the carrier over ๐”ฝโ‚‚ is the image of the corresponding point of the split torus under the generating coordinate map.

        source
        @[simp]
        theorem TauCeti.F4ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints (k : Fin 4 โŠ• Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 โ†’ Aหฃ) (u : Multiplicative A) :
        (weightTorusPoints A) s * (rootSubgroupPoints k A) u * ((weightTorusPoints A) s)โปยน = (rootSubgroupPoints k A) (Multiplicative.ofAdd (โ†‘(torusCharacter s (DynkinType.F4.rootGeneratorWeight DynkinType.valid_F4 k)) * Multiplicative.toAdd u))

        The pinning equation on matrix-valued points of the carrier over ๐”ฝโ‚‚: conjugation by a point s of the weight torus rescales the parameter of each numbered simple root subgroup by the corresponding type-Fโ‚„ root character evaluated at s.

        Functoriality #

        source
        noncomputable def TauCeti.F4ShortRoot.PrimeField.pointsMap {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (f : A โ†’โ‚[ZMod 2] B) :
        โ†ฅ(points A) โ†’* โ†ฅ(points B)

        The map on the points of the carrier over ๐”ฝโ‚‚ induced by a homomorphism of ๐”ฝโ‚‚-algebras.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.F4ShortRoot.PrimeField.coe_pointsMap {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (f : A โ†’โ‚[ZMod 2] B) (g : โ†ฅ(points A)) :
          โ†‘((pointsMap f) g) = (Matrix.GeneralLinearGroup.map โ†‘f) โ†‘g

          The induced map on points applies the algebra homomorphism entrywise.

          source
          @[simp]
          theorem TauCeti.F4ShortRoot.PrimeField.pointsMap_id {A : Type v} [CommRing A] [Algebra (ZMod 2) A] :
          pointsMap (AlgHom.id (ZMod 2) A) = MonoidHom.id โ†ฅ(points A)

          The identity algebra homomorphism induces the identity on carrier points.

          source
          theorem TauCeti.F4ShortRoot.PrimeField.pointsMap_comp {A : Type u} {B : Type v} {C : Type w} [CommRing A] [CommRing B] [CommRing C] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] [Algebra (ZMod 2) C] (f : A โ†’โ‚[ZMod 2] B) (g : B โ†’โ‚[ZMod 2] C) :
          pointsMap (g.comp f) = (pointsMap g).comp (pointsMap f)

          The induced maps on carrier points compose.

          source
          theorem TauCeti.F4ShortRoot.PrimeField.pointsMap_injective {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] {f : A โ†’โ‚[ZMod 2] B} (hf : Function.Injective โ‡‘f) :
          Function.Injective โ‡‘(pointsMap f)

          An injective algebra homomorphism induces an injective map on carrier points.

          source
          @[simp]
          theorem TauCeti.F4ShortRoot.PrimeField.pointsMap_rootSubgroupPoints {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (f : A โ†’โ‚[ZMod 2] B) (k : Fin 4 โŠ• Fin 4) (u : Multiplicative A) :
          (pointsMap f) ((rootSubgroupPoints k A) u) = (rootSubgroupPoints k B) (Multiplicative.ofAdd (f (Multiplicative.toAdd u)))

          The induced map carries a numbered root-subgroup parameter along the algebra homomorphism.

          source
          @[simp]
          theorem TauCeti.F4ShortRoot.PrimeField.pointsMap_weightTorusPoints {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (f : A โ†’โ‚[ZMod 2] B) (s : Fin 4 โ†’ Aหฃ) :
          (pointsMap f) ((weightTorusPoints A) s) = (weightTorusPoints B) fun (i : Fin 4) => (Units.map โ†‘f) (s i)

          The induced map carries a weight-torus point coordinatewise along the algebra homomorphism.

          source
          noncomputable def TauCeti.F4ShortRoot.PrimeField.coordinatePointsEquiv (A : Type v) [CommRing A] [Algebra (ZMod 2) A] :
          โ†‘(HopfAlgebra.points โ†งA) โ‰ƒ* โ†ฅ(points A)

          Quotient-coordinate points are the existing matrix-valued F4 carrier points.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.F4ShortRoot.PrimeField.coe_coordinatePointsEquiv (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (q : โ†‘(HopfAlgebra.points โ†งA)) :
            โ†‘((coordinatePointsEquiv A) q) = (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (q.ofConv.comp โ†‘(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator)))))

            The coordinate-point equivalence evaluates the ambient matrix coordinates.

            source
            @[simp]
            theorem TauCeti.F4ShortRoot.PrimeField.coordinatePointsEquiv_mapPoints {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (f : A โ†’โ‚[ZMod 2] B) (q : โ†‘(HopfAlgebra.points โ†งA)) :
            (coordinatePointsEquiv B) (WithConv.toConv (f.comp q.ofConv)) = (pointsMap f) ((coordinatePointsEquiv A) q)

            The quotient-coordinate equivalence commutes with change of coefficient algebra.