Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.PrimeField.SchemePoints

Scheme-valued points of the prime-field F4 carrier #

The quotient-coordinate presentation identifies scheme-valued points of the carrier with its matrix-valued points. The numbered root subgroups and weight torus agree under this equivalence. These identifications transfer equations between quotient-coordinate, matrix-valued, and scheme-valued points, so the carrier's matrix-point laws yield scheme-level statements.

source
noncomputable def TauCeti.F4ShortRoot.PrimeField.groupSchemePointMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 2) A] :
↑(HopfAlgebra.points ↧A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ groupScheme.X)

A scheme-valued F4 carrier point is a quotient-coordinate Hopf-algebra point.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 2) A] :
    ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ groupScheme.X) ≃* ↥(points A)

    Scheme-valued points of the F4 carrier are its named matrix-valued points.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv_groupSchemePointMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 2) A] (q : ↑(HopfAlgebra.points ↧A)) :
      (schemePointsMulEquiv A) ((groupSchemePointMulEquiv A) q) = (coordinatePointsEquiv A) q

      The scheme point represented by a quotient-coordinate point maps to its corresponding matrix point under the scheme-point equivalence.

      source
      @[simp]
      theorem TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv_symm_apply (A : Type) [CommRing A] [Algebra (ZMod 2) A] (g : ↥(points A)) :
      (schemePointsMulEquiv A).symm g = (groupSchemePointMulEquiv A) ((coordinatePointsEquiv A).symm g)

      The inverse comparison presents a matrix point as a quotient-coordinate scheme point.

      source
      theorem TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv_mapValue {A B : Type} [CommRing A] [CommRing B] [Algebra (ZMod 2) A] [Algebra (ZMod 2) B] (φ : A →ₐ[ZMod 2] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ groupScheme.X) :
      (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧(ZMod 2))) p) = (pointsMap φ) ((schemePointsMulEquiv A) p)

      The scheme-point comparison commutes with change of coefficient algebra.

      source
      theorem TauCeti.F4ShortRoot.PrimeField.groupSchemePointMulEquiv_comp_coordinateMap (A : Type) [CommRing A] [Algebra (ZMod 2) A] (phi : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator) ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator)) (q : ↑(HopfAlgebra.points ↧A)) :
      CategoryTheory.CategoryStruct.comp ((groupSchemePointMulEquiv A) q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧(ZMod 2)).map phi.op) (CategoryTheory.eqToHom ⋯))).hom.hom = (groupSchemePointMulEquiv A) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom phi)) q)

      A coordinate endomorphism acts on scheme-valued points by precomposition.

      source
      @[simp]
      theorem TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv_comp_rootSubgroup (k : Fin 4 ⊕ Fin 4) (A : Type) [CommRing A] [Algebra (ZMod 2) A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ (AdditiveGroup.groupScheme (ZMod 2)).X) :
      (schemePointsMulEquiv A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup k).hom.hom) = (rootSubgroupPoints k A) ((AdditiveGroup.schemePointsMulEquiv A) p)

      The public root-subgroup scheme morphism induces the named root points.

      source
      @[simp]
      theorem TauCeti.F4ShortRoot.PrimeField.schemePointsMulEquiv_comp_weightTorus (A : Type) [CommRing A] [Algebra (ZMod 2) A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ (SplitTorus.groupScheme (ZMod 2) (Fin 4)).X) :
      (schemePointsMulEquiv A) (CategoryTheory.CategoryStruct.comp p weightTorus.hom.hom) = (weightTorusPoints A) (SplitTorus.schemePointsMulEquiv p)

      The public weight-torus scheme morphism induces the named torus points.

      source
      theorem TauCeti.F4ShortRoot.PrimeField.weightTorus_conj_rootSubgroup (k : Fin 4 ⊕ Fin 4) (A : Type) [CommRing A] [Algebra (ZMod 2) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ (SplitTorus.groupScheme (ZMod 2) (Fin 4)).X) (u : A) :
      CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd u)) (rootSubgroup k).hom.hom * (CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (DynkinType.F4.rootGeneratorWeight DynkinType.valid_F4 k)) * u))) (rootSubgroup k).hom.hom

      Conjugation by the weight torus rescales every numbered root subgroup by its root character, on scheme-valued points.