Documentation

TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.SpecialIsogeny

The special isogeny of the short-root type-G2 carrier #

The matrix Matrix.g2SpecialIsogeny of signed two-by-two minors is multiplicative on matrices preserving the type-Gā‚‚ cross product and its invariant dual form. The universal point of the short-root carrier over š”½ā‚ƒ preserves both tensors, so the formula determines an endomorphism of the carrier. Its action exchanges the two numbered simple roots, cubes the parameter at the short root, and sends a torus point (sā‚€, sā‚) to (sā‚, sā‚€Ā³).

The square is the prime-field Frobenius of TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Frobenius, on the coordinate Hopf algebra, on the carrier group scheme, and on points.

The carrier is not identified here with the pinned simply connected group scheme of type Gā‚‚; the construction transfers to that group scheme only along such an identification.

Main definitions #

Main results #

References #

Equations on the generators #

source
def TauCeti.G2ShortRoot.PrimeField.specialIsogenyRootIndex :
Equiv.Perm (Fin 2 āŠ• Fin 2)

The special isogeny's length-exchanging permutation on positive and negative numbered simple root subgroups.

Equations
Instances For
    source
    def TauCeti.G2ShortRoot.PrimeField.specialIsogenyExponent :
    Fin 2 āŠ• Fin 2 ā†’ ā„•

    The parameter exponent of the special isogeny: three at either short root and one at either long root.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyRootIndex_inl (i : Fin 2) :
      specialIsogenyRootIndex (Sum.inl i) = Sum.inl ((Equiv.swap 0 1) i)

      The special isogeny swaps the two positive numbered simple roots.

      source
      @[simp]
      theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyRootIndex_inr (i : Fin 2) :
      specialIsogenyRootIndex (Sum.inr i) = Sum.inr ((Equiv.swap 0 1) i)

      The special isogeny swaps the two negative numbered simple roots.

      source
      @[simp]
      theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyRootIndex_apply_self (k : Fin 2 āŠ• Fin 2) :
      specialIsogenyRootIndex (specialIsogenyRootIndex k) = k

      Exchanging the lengths of a numbered simple root twice returns the original root.

      source
      @[simp]
      theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyExponent_inl (i : Fin 2) :
      specialIsogenyExponent (Sum.inl i) = if i = 0 then 3 else 1

      On a positive numbered root, the parameter is cubed at the short node and unchanged at the long node.

      source
      @[simp]
      theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyExponent_inr (i : Fin 2) :
      specialIsogenyExponent (Sum.inr i) = if i = 0 then 3 else 1

      On a negative numbered root, the parameter is cubed at the short node and unchanged at the long node.

      source
      noncomputable def TauCeti.G2ShortRoot.PrimeField.specialIsogenyCoordinateMap :
      carrierAlgebra āŸ¶ carrierAlgebra

      The special isogeny's endomorphism of the carrier coordinate Hopf algebra.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.G2ShortRoot.PrimeField.specialIsogenyHom :
        groupScheme āŸ¶ groupScheme

        The special isogeny as an endomorphism of the short-root type-Gā‚‚ carrier over š”½ā‚ƒ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyHom_eq_map_specialIsogenyCoordinateMap :
          specialIsogenyHom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom groupScheme_eq_commonKernelSpec) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ā†§(ZMod 3)).map specialIsogenyCoordinateMap.op) (CategoryTheory.eqToHom ā‹Æ))

          The comorphism of the carrier special isogeny is specialIsogenyCoordinateMap.

          The endomorphism on points #

          source
          noncomputable def TauCeti.G2ShortRoot.PrimeField.specialIsogeny (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
          ā†„(points A) ā†’* ā†„(points A)

          The special isogeny on matrix-valued points of the carrier, functorially over every š”½ā‚ƒ-algebra.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.coe_specialIsogeny {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (g : ā†„(points A)) :
            ā†‘ā†‘((specialIsogeny A) g) = (ā†‘ā†‘g).g2SpecialIsogeny

            The special isogeny is the signed-minor formula on the underlying matrix.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogeny_rootSubgroupPoints {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (k : Fin 2 āŠ• Fin 2) (t : A) :
            (specialIsogeny A) ((rootSubgroupPoints k A) (Multiplicative.ofAdd t)) = (rootSubgroupPoints (specialIsogenyRootIndex k) A) (Multiplicative.ofAdd (t ^ specialIsogenyExponent k))

            The pinning equation on all four numbered simple root subgroups.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogeny_weightTorusPoints {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (s : Fin 2 ā†’ AĖ£) :
            (specialIsogeny A) ((weightTorusPoints A) s) = (weightTorusPoints A) ![s 1, s 0 ^ 3]

            The special isogeny sends a torus point (sā‚€, sā‚) to (sā‚, sā‚€Ā³).

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.pointsMap_specialIsogeny {A : Type v} [CommRing A] [Algebra (ZMod 3) A] {B : Type w} [CommRing B] [Algebra (ZMod 3) B] (f : A ā†’ā‚[ZMod 3] B) (g : ā†„(points A)) :
            (pointsMap f) ((specialIsogeny A) g) = (specialIsogeny B) ((pointsMap f) g)

            The special isogeny commutes with extension of the value algebra.

            The Frobenius square relation #

            source
            theorem TauCeti.G2ShortRoot.PrimeField.map_carrierGenericMatrix_specialIsogenyCoordinateMap :
            carrierGenericMatrix.map ā‡‘ā†‘(CommHopfAlgCat.Hom.hom specialIsogenyCoordinateMap) = carrierGenericMatrix.g2SpecialIsogeny

            The special isogeny's coordinate map sends the universal point of the carrier to its signed-minor image: this is the defining equation of specialIsogenyCoordinateMap.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_specialIsogenyHom (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ā†§B).asOver (AlgebraicGeometry.Spec ā†§(ZMod 3)) āŸ¶ groupScheme.X) :
            (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p specialIsogenyHom.hom.hom) = (specialIsogeny B) ((schemePointsMulEquiv B) p)

            The action induced by specialIsogenyHom on scheme-valued carrier points is the named matrix-valued special isogeny.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyCoordinateMap_comp_self :
            CategoryTheory.CategoryStruct.comp specialIsogenyCoordinateMap specialIsogenyCoordinateMap = frobeniusCoordinateMap

            The special isogeny squared is the prime-field Frobenius on the carrier coordinate ring.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_rootSubgroup_comp_specialIsogenyHom (k : Fin 2 āŠ• Fin 2) (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ā†§B).asOver (AlgebraicGeometry.Spec ā†§(ZMod 3)) āŸ¶ (AdditiveGroup.groupScheme (ZMod 3)).X) :
            (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (rootSubgroup k).hom.hom specialIsogenyHom.hom.hom)) = (rootSubgroupPoints (specialIsogenyRootIndex k) B) (Multiplicative.ofAdd (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv B) p) ^ specialIsogenyExponent k))

            On scheme-valued points, composing a numbered root subgroup with the carrier special isogeny exchanges the root lengths and applies the prescribed parameter exponent.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_weightTorus_comp_specialIsogenyHom (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ā†§B).asOver (AlgebraicGeometry.Spec ā†§(ZMod 3)) āŸ¶ (SplitTorus.groupScheme (ZMod 3) (Fin 2)).X) :
            (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp weightTorus.hom.hom specialIsogenyHom.hom.hom)) = (weightTorusPoints B) (SplitTorus.schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (DynkinType.g2SpecialTorusEnd (ZMod 3)).hom.hom))

            On scheme-valued points, composing the weight torus with the carrier special isogeny sends (sā‚€, sā‚) to (sā‚, sā‚€Ā³).

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogenyHom_comp_self :
            CategoryTheory.CategoryStruct.comp specialIsogenyHom specialIsogenyHom = frobeniusHom

            The special isogeny squared is the cubic Frobenius as a carrier morphism.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogeny_specialIsogeny {A : Type v} [CommRing A] [Algebra (ZMod 3) A] (g : ā†„(points A)) :
            (specialIsogeny A) ((specialIsogeny A) g) = (frobenius 1 A) g

            The special isogeny of the carrier squares pointwise to the cubic Frobenius.

            source
            theorem TauCeti.G2ShortRoot.PrimeField.specialIsogeny_comp_specialIsogeny {A : Type v} [CommRing A] [Algebra (ZMod 3) A] :
            (specialIsogeny A).comp (specialIsogeny A) = frobenius 1 A

            The special isogeny squared is the cubic Frobenius on matrix-valued points.