Documentation

TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Frobenius

The Frobenius endomorphism of the additive group #

Over a base commutative semiring R of exponential characteristic p, the additive group 𝔾ₐ = Spec R[x] (here x = ι R R 1 in SymmetricAlgebra R R) carries the Frobenius endomorphism F : 𝔾ₐ → 𝔾ₐ, which on every commutative R-algebra A raises a point to its p-th power, a ↦ aᵖ. This is a homomorphism of additive-monoid-valued functors precisely because of the freshman's dream: raising to the p-th power is additive in exponential characteristic p. Contravariantly it is induced by the bialgebra endomorphism of the coordinate bialgebra R[x] sending the primitive generator x to xᵖ (again primitive, Δ(xᵖ) = xᵖ ⊗ 1 + 1 ⊗ xᵖ).

The exponential-characteristic hypothesis [ExpChar R p] covers both the interesting case of prime characteristic p (where F is the genuine Frobenius) and the degenerate case p = 1 (characteristic zero, where F is the identity), so the API applies verbatim to the Frobenius kernel group scheme αₚ of TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.Basic, where R has prime characteristic p.

Main declarations #

References #

The additive-group points dictionary TauCeti.AdditiveGroup.gaPointsMulEquiv and the coordinate-bialgebra functoriality TauCeti.AlgHom.mapDomain are Tau Ceti's. The freshman's dream add_pow_expChar, the symmetric-algebra bialgebra structure, and the bialgebra-hom constructor BialgHom.ofAlgHom are Mathlib's.

source
theorem TauCeti.AdditiveGroup.comul_ι_pow (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] :
CoalgebraStruct.comul ((SymmetricAlgebra.ι R R) 1 ^ p) = ((SymmetricAlgebra.ι R R) 1 ^ p) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ((SymmetricAlgebra.ι R R) 1 ^ p)

The Frobenius power xᵖ is primitive. In exponential characteristic p the comultiplication of xᵖ is xᵖ ⊗ 1 + 1 ⊗ xᵖ, by the freshman's dream applied to the primitive generator x.

source
noncomputable def TauCeti.AdditiveGroup.frobeniusBialgHom (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] :
SymmetricAlgebra R R →ₐc[R] SymmetricAlgebra R R

The Frobenius bialgebra endomorphism x ↦ xᵖ of the coordinate bialgebra of 𝔾ₐ. In exponential characteristic p the generator x is primitive, hence so is xᵖ (Δ(xᵖ) = xᵖ ⊗ 1 + 1 ⊗ xᵖ by the freshman's dream), and the counit still vanishes on xᵖ, so the algebra endomorphism x ↦ xᵖ is a bialgebra endomorphism. It induces the Frobenius endomorphism of 𝔾ₐ on the functor of points.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AdditiveGroup.frobeniusBialgHom_ι (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] (r : R) :
    (frobeniusBialgHom R p) ((SymmetricAlgebra.ι R R) r) = r • (SymmetricAlgebra.ι R R) 1 ^ p
    source
    theorem TauCeti.AdditiveGroup.frobeniusBialgHom_ι_one (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] :
    (frobeniusBialgHom R p) ((SymmetricAlgebra.ι R R) 1) = (SymmetricAlgebra.ι R R) 1 ^ p
    source
    noncomputable def TauCeti.AdditiveGroup.frobeniusEnd (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] {A : Type v} [CommSemiring A] [Algebra R A] :
    WithConv (SymmetricAlgebra R R →ₐ[R] A) →* WithConv (SymmetricAlgebra R R →ₐ[R] A)

    The Frobenius endomorphism of 𝔾ₐ, on the functor of points. For every commutative R-algebra A it is the homomorphism of the convolution monoid of points induced (contravariantly) by the Frobenius bialgebra endomorphism x ↦ xᵖ; on points it raises a point to its p-th power, a ↦ aᵖ.

    Equations
    Instances For
      source
      theorem TauCeti.AdditiveGroup.toAdd_gaPointsMulEquiv_frobeniusEnd (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] {A : Type v} [CommSemiring A] [Algebra R A] (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) :
      Multiplicative.toAdd (gaPointsMulEquiv ((frobeniusEnd R p) F)) = Multiplicative.toAdd (gaPointsMulEquiv F) ^ p

      The Frobenius endomorphism acts as a ↦ aᵖ on points. Reading a 𝔾ₐ-point off on the generator x = ι 1, the Frobenius endomorphism raises the resulting element of A to its p-th power.

      This is not a simp lemma: the @[simp] lemma toAdd_gaPointsMulEquiv already rewrites the left-hand side Multiplicative.toAdd (gaPointsMulEquiv ..), so the statement is not in simp-normal form.

      source
      theorem TauCeti.AdditiveGroup.mapValue_frobeniusEnd (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] {A : Type v} [CommSemiring A] [Algebra R A] {B : Type w} [CommSemiring B] [Algebra R B] (χ : A →ₐ[R] B) :
      (frobeniusEnd R p).comp (AlgHom.mapValue χ) = (AlgHom.mapValue χ).comp (frobeniusEnd R p)

      Naturality in the value algebra. The Frobenius endomorphism of 𝔾ₐ commutes with the value-algebra functoriality AlgHom.mapValue.