Documentation

TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.PointsFunctor

Points of the short-root type-G2 carrier over the prime field of characteristic three #

The carrier of TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Carrier is the subgroup scheme of GL₇ over 𝔽₃ generated by the reduced simple root subgroups and weight torus of the integral short-root toral closure. This file realizes its points as seven-by-seven matrices over an 𝔽₃-algebra, identifies the pinned points with the corresponding integral matrices, transports the pinning equation to them, and records functoriality in the value algebra.

Identifying the pinned points with the integral ones is what makes the carrier concrete: a numbered simple-root point is the divided-power exponential matrix 1 + t X + t² Y of the generator, and a weight-torus point is the diagonal matrix of the weight characters, exactly as over ℤ. Only the proved one-way containment between the carrier and the base change of the integral toral closure is used; no flatness is asserted.

Main definitions #

Main results #

References #

The identification of the reduced generators with the integral ones is the base-change compatibility of the Chevalley--Demazure construction; see R. W. Carter, Simple Groups of Lie Type, §4.4, and J. C. Jantzen, Representations of Algebraic Groups, II.1--2. The weight conventions follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX.

Matrix-valued points #

source
noncomputable def TauCeti.G2ShortRoot.PrimeField.points (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
Subgroup (GL (Fin 7) A)

The matrix-valued points of the short-root type-G₂ carrier over 𝔽₃.

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

    The points of the carrier are the points of the subgroup scheme generated by the reduced generators.

    source
    theorem TauCeti.G2ShortRoot.PrimeField.points_eq_hopfIdealPointsSubgroup (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
    points A = GeneralLinear.hopfIdealPointsSubgroup 7 definingIdeal A

    The points of the carrier are cut out by its defining Hopf ideal.

    source
    noncomputable def TauCeti.G2ShortRoot.PrimeField.pointsMulEquiv (A : CommAlgCat (ZMod 3)) :
    ↑(HopfAlgebra.points A) ≃* ↥(points ↑A)

    The points of the quotient coordinate Hopf algebra are the named matrix-valued carrier points.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.G2ShortRoot.PrimeField.coe_pointsMulEquiv_eq_map_carrierGenericMatrix {B : Type v} [CommRing B] [Algebra (ZMod 3) B] (q : ↑(HopfAlgebra.points ↧B)) :
      ↑↑((pointsMulEquiv ↧B) q) = carrierGenericMatrix.map ⇑q.ofConv

      The matrix of a quotient-coordinate point is the universal point carrierGenericMatrix evaluated along it.

      source
      noncomputable def TauCeti.G2ShortRoot.PrimeField.groupSchemePointMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 3) A] :
      WithConv (↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7) (CommHopfAlgCat.commonKernelHopfIdeal generator)) →ₐ[ZMod 3] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ groupScheme.X)

      Mathlib's spectrum-points equivalence for the quotient presentation of the carrier.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.G2ShortRoot.PrimeField.groupSchemePointMulEquiv_comp_coordinateMap {B : Type} [CommRing B] [Algebra (ZMod 3) B] (phi : carrierAlgebra ⟶ carrierAlgebra) (q : ↑(HopfAlgebra.points ↧B)) :
        CategoryTheory.CategoryStruct.comp ((groupSchemePointMulEquiv B) q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom groupScheme_eq_commonKernelSpec) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧(ZMod 3)).map phi.op) (CategoryTheory.eqToHom ⋯))).hom.hom = (groupSchemePointMulEquiv B) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom phi)) q)

        Composing a quotient-coordinate carrier point with the scheme morphism induced by a coordinate endomorphism of the carrier pulls the point back along that endomorphism.

        source
        noncomputable def TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 3) A] :
        ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ groupScheme.X) ≃* ↥(points A)

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

        Equations
        Instances For
          source
          theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_groupSchemePointMulEquiv (A : Type) [CommRing A] [Algebra (ZMod 3) A] (q : ↑(HopfAlgebra.points ↧A)) :
          (schemePointsMulEquiv A) ((groupSchemePointMulEquiv A) q) = (pointsMulEquiv ↧A) q

          A quotient-coordinate point gives the same named carrier point under the scheme and matrix presentations.

          source
          @[simp]
          theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_carrierι (A : Type) [CommRing A] [Algebra (ZMod 3) A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ groupScheme.X) :
          (GeneralLinear.schemePointsMulEquiv 7 A) (CategoryTheory.CategoryStruct.comp p carrierι.hom.hom) = ↑((schemePointsMulEquiv A) p)

          Composing a scheme-valued carrier point with its ambient inclusion into GL₇ gives the underlying invertible matrix of the named carrier point.

          source
          @[simp]
          theorem TauCeti.G2ShortRoot.PrimeField.mem_points_iff (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (g : GL (Fin 7) A) :
          g ∈ points A ↔ ∀ x ∈ definingIdeal, ((GeneralLinear.pointsMulEquiv 7).symm g).ofConv x = 0

          A matrix is a point of the carrier exactly when its associated convolution point kills the carrier's defining Hopf ideal.

          source
          theorem TauCeti.G2ShortRoot.PrimeField.points_le_baseChangePresentationPoints (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
          points A ≤ GeneralLinear.hopfIdealPointsSubgroup 7 (UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight (ZMod 3)) A

          Every point of the carrier is a point of the base change of the integral short-root toral closure.

          source
          noncomputable def TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
          Multiplicative A →* ↥(points A)

          The parametrized numbered simple root subgroup inside the points of the carrier.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints_gaPointsMulEquiv (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (q : ↑(HopfAlgebra.points ↧A)) :
            ↑((rootSubgroupPoints k A) (AdditiveGroup.gaPointsMulEquiv q)) = (GeneralLinear.pointsMulEquiv 7) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (generator (Sum.inl k))).app ↧A)) q)

            A numbered simple-root point of the carrier is the image of the corresponding point of 𝔾ₐ under the generating coordinate map.

            source
            @[simp]
            theorem TauCeti.G2ShortRoot.PrimeField.coe_rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (u : Multiplicative A) :
            ↑((rootSubgroupPoints k A) u) = ↑((IntegralToralClosure.rootSubgroupPoints k A) u)

            A numbered simple-root point of the carrier is the corresponding point of the integral short-root toral closure, as a matrix.

            source
            noncomputable def TauCeti.G2ShortRoot.PrimeField.weightTorusPoints (A : Type v) [CommRing A] [Algebra (ZMod 3) A] :
            (Fin 2 → Aˣ) →* ↥(points A)

            The split weight torus inside the points of the carrier.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem TauCeti.G2ShortRoot.PrimeField.coe_weightTorusPoints_pointsMulEquiv (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (q : ↑(HopfAlgebra.points ↧A)) :
              ↑((weightTorusPoints A) (SplitTorus.pointsMulEquiv q)) = (GeneralLinear.pointsMulEquiv 7) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (generator (Sum.inr ()))).app ↧A)) q)

              A weight-torus point of the carrier is the image of the corresponding point of the split torus under the generating coordinate map.

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

              The map on points induced by a numbered root-subgroup morphism is the named rootSubgroupPoints homomorphism under the additive-group and carrier point equivalences.

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

              The map on points induced by the weight-torus morphism is the named weightTorusPoints homomorphism under the split-torus and carrier point equivalences.

              source
              @[simp]
              theorem TauCeti.G2ShortRoot.PrimeField.coe_weightTorusPoints (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (s : Fin 2 → Aˣ) :
              ↑((weightTorusPoints A) s) = ↑((IntegralToralClosure.weightTorusPoints A) s)

              A weight-torus point of the carrier is the corresponding point of the integral short-root toral closure, as a matrix.

              source
              @[simp]
              theorem TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] (s : Fin 2 → Aˣ) (u : Multiplicative A) :
              (weightTorusPoints A) s * (rootSubgroupPoints k A) u * ((weightTorusPoints A) s)⁻¹ = (rootSubgroupPoints k A) (Multiplicative.ofAdd (↑(torusCharacter s (DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2 k)) * Multiplicative.toAdd u))

              The pinning equation on matrix-valued points of the carrier: conjugation by a point s of the weight torus rescales the parameter of each numbered simple root subgroup by the corresponding type-G₂ root character evaluated at s.

              source
              @[simp]
              theorem TauCeti.G2ShortRoot.PrimeField.weightTorus_conj_rootSubgroup (k : Fin 2 ⊕ Fin 2) (A : Type) [CommRing A] [Algebra (ZMod 3) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ (SplitTorus.groupScheme (ZMod 3) (Fin 2)).X) (u : A) :
              CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.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.G2.rootGeneratorWeight DynkinType.valid_G2 k)) * u))) (rootSubgroup k).hom.hom

              The torus-conjugation equation on scheme-valued points of the carrier: conjugation by a point of the weight torus rescales the parameter of each numbered simple root subgroup by the corresponding type-G₂ root character.

              Functoriality #

              source
              noncomputable def TauCeti.G2ShortRoot.PrimeField.pointsMap {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] (f : A →ₐ[ZMod 3] B) :
              ↥(points A) →* ↥(points B)

              The map on the points of the carrier induced by a homomorphism of 𝔽₃-algebras.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.G2ShortRoot.PrimeField.coe_pointsMap {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] (f : A →ₐ[ZMod 3] 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.G2ShortRoot.PrimeField.pointsMap_id {A : Type v} [CommRing A] [Algebra (ZMod 3) A] :
                pointsMap (AlgHom.id (ZMod 3) A) = MonoidHom.id ↥(points A)

                The identity algebra homomorphism induces the identity on carrier points.

                source
                @[simp]
                theorem TauCeti.G2ShortRoot.PrimeField.pointsMap_comp {A : Type u} {B : Type v} {C : Type w} [CommRing A] [CommRing B] [CommRing C] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] [Algebra (ZMod 3) C] (f : A →ₐ[ZMod 3] B) (g : B →ₐ[ZMod 3] C) :
                pointsMap (g.comp f) = (pointsMap g).comp (pointsMap f)

                The induced maps on carrier points compose.

                source
                theorem TauCeti.G2ShortRoot.PrimeField.pointsMap_injective {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] {f : A →ₐ[ZMod 3] B} (hf : Function.Injective ⇑f) :
                Function.Injective ⇑(pointsMap f)

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

                source
                @[simp]
                theorem TauCeti.G2ShortRoot.PrimeField.pointsMap_rootSubgroupPoints {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] (f : A →ₐ[ZMod 3] B) (k : Fin 2 ⊕ Fin 2) (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.G2ShortRoot.PrimeField.pointsMap_weightTorusPoints {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra (ZMod 3) A] [Algebra (ZMod 3) B] (f : A →ₐ[ZMod 3] B) (s : Fin 2 → Aˣ) :
                (pointsMap f) ((weightTorusPoints A) s) = (weightTorusPoints B) fun (i : Fin 2) => (Units.map ↑f) (s i)

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