Documentation

TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.Kernel

αₚ is the kernel of the Frobenius endomorphism of the additive group #

Over a base ring R of prime characteristic p, the additive group 𝔾ₐ = Spec R[x] (here x = ι R R 1 in SymmetricAlgebra R R) carries the Frobenius endomorphism F : 𝔾ₐ → 𝔾ₐ (TauCeti.AdditiveGroup.frobeniusEnd, of TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Frobenius), which on every commutative R-algebra A raises a point to its p-th power, a ↦ aᵖ.

TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.Basic builds the Frobenius kernel group scheme αₚ = Spec R[x]/(xᵖ) and identifies its functor of points with the p-nilpotent elements of the additive group. This file exhibits the inclusion αₚ ↪ 𝔾ₐ on the functor of points and proves that αₚ is exactly the kernel of the Frobenius endomorphism: as subgroups of the group of 𝔾ₐ-points, the image of the inclusion αₚ ↪ 𝔾ₐ equals the kernel of the Frobenius endomorphism. This realizes αₚ = ker(𝔾ₐ --a ↦ aᵖ--> 𝔾ₐ) on the functor of points, the additive companion of the identification of μ_n with the kernel of the nth power endomorphism of 𝔾ₘ (TauCeti.Algebra.AlgebraicGroup.RootsOfUnity.Kernel).

The mechanism is the worked-example points dictionary. A point of 𝔾ₐ = Spec R[x] reads off the element F(x) : A (TauCeti.AdditiveGroup.gaPointsMulEquiv); the Frobenius endomorphism raises that element to the p-th power (TauCeti.AdditiveGroup.toAdd_gaPointsMulEquiv_frobeniusEnd), while an included αₚ-point reads off a p-nilpotent element (aᵖ = 0), whose p-th power vanishes. Conversely a 𝔾ₐ-point read off as an element a with aᵖ = 0 is a p-nilpotent element, hence the image of the αₚ-point attached to it (TauCeti.AlphaP.mem_range_pointsHom_iff).

Main declarations #

See also #

The Frobenius endomorphism TauCeti.AdditiveGroup.frobeniusEnd of 𝔾ₐ is Tau Ceti's TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Frobenius; the Frobenius kernel αₚ and its p-nilpotent functor of points are TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.Basic. The additive-group points dictionary TauCeti.AdditiveGroup.gaPointsMulEquiv and the coordinate-Hopf-algebra functoriality TauCeti.AlgHom.mapDomain (with its naturality TauCeti.AlgHom.mapValue_mapDomain) are Tau Ceti's. This realizes αₚ = ker(Frobenius) on the functor of points, the additive companion of TauCeti.Algebra.AlgebraicGroup.RootsOfUnity.Kernel.

αₚ as the kernel of the Frobenius endomorphism #

source
noncomputable def TauCeti.AlphaP.inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] :
WithConv (CoordinateRing p →ₐ[R] A) →* WithConv (SymmetricAlgebra R R →ₐ[R] A)

The inclusion αₚ ↪ 𝔾ₐ on the functor of points. It is the homomorphism of convolution groups of points induced (contravariantly) by the quotient bialgebra map R[x] ↠ R[x]/(xᵖ), i.e. pre-composition of a point of αₚ with the quotient map. It agrees with the underlying-element map TauCeti.AlphaP.pointsHom through TauCeti.AdditiveGroup.gaPointsMulEquiv.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlphaP.gaPointsMulEquiv_inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] (F : WithConv (CoordinateRing p →ₐ[R] A)) :
    AdditiveGroup.gaPointsMulEquiv ((inclusion p) F) = (pointsHom p) F

    Reading an included αₚ-point off as an element of the additive group is the underlying-element map TauCeti.AlphaP.pointsHom: both pre-compose the point with the quotient map R[x] ↠ R[x]/(xᵖ) and evaluate at the generator.

    source
    theorem TauCeti.AlphaP.inclusion_injective {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] :
    Function.Injective ⇑(inclusion p)

    The inclusion αₚ ↪ 𝔾ₐ is injective on the functor of points. It agrees through TauCeti.AdditiveGroup.gaPointsMulEquiv with the injective underlying-element map TauCeti.AlphaP.pointsHom, so distinct αₚ-points include to distinct 𝔾ₐ-points.

    source
    theorem TauCeti.AlphaP.mapValue_inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (χ : A →ₐ[R] B) :
    (inclusion p).comp (AlgHom.mapValue χ) = (AlgHom.mapValue χ).comp (inclusion p)

    Naturality in the value algebra. The inclusion αₚ ↪ 𝔾ₐ commutes with the value-algebra functoriality AlgHom.mapValue.

    source
    theorem TauCeti.AlphaP.frobeniusEnd_comp_inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] :
    (AdditiveGroup.frobeniusEnd R p).comp (inclusion p) = 1

    The Frobenius endomorphism annihilates αₚ. Composing the Frobenius endomorphism of 𝔾ₐ after the inclusion αₚ ↪ 𝔾ₐ is the trivial homomorphism of group functors: every αₚ-point maps to a p-nilpotent element, whose p-th power is 0.

    source
    @[simp]
    theorem TauCeti.AlphaP.frobeniusEnd_inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] (F : WithConv (CoordinateRing p →ₐ[R] A)) :
    (AdditiveGroup.frobeniusEnd R p) ((inclusion p) F) = 1

    The Frobenius endomorphism annihilates every αₚ-point, in element form.

    source
    theorem TauCeti.AlphaP.mem_range_inclusion_iff {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] {g : WithConv (SymmetricAlgebra R R →ₐ[R] A)} :
    g ∈ (inclusion p).range ↔ (AdditiveGroup.frobeniusEnd R p) g = 1

    Membership in the image of αₚ ↪ 𝔾ₐ. A 𝔾ₐ-point lies in the image of the αₚ inclusion exactly when the Frobenius endomorphism kills it: g comes from αₚ iff gᵖ = 0 in the additive group of points.

    source
    theorem TauCeti.AlphaP.range_inclusion {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] :
    (inclusion p).range = (AdditiveGroup.frobeniusEnd R p).ker

    αₚ is the kernel of the Frobenius endomorphism of 𝔾ₐ. As subgroups of the group of 𝔾ₐ-points, the image of the inclusion αₚ ↪ 𝔾ₐ equals the kernel of the Frobenius endomorphism: a 𝔾ₐ-point comes from αₚ exactly when its p-th power is trivial. This realizes αₚ = ker(𝔾ₐ --a ↦ aᵖ--> 𝔾ₐ) on the functor of points.