The Frobenius kernel group scheme αₚ

Over a base ring R of prime characteristic p, the additive group 𝔾ₐ = Spec R[x] (here x = ι R R 1 in SymmetricAlgebra R R) has a closed subgroup scheme αₚ, the kernel of the Frobenius endomorphism x ↦ xᵖ. Its coordinate ring is the quotient Hopf algebra R[x] / (xᵖ), and for every commutative R-algebra A its A-points are the p-nilpotent elements of A: the elements a ∈ A with aᵖ = 0. (This is the Frobenius kernel, not the kernel of multiplication by p; in characteristic p the latter is all of 𝔾ₐ.)

This file builds αₚ as the quotient of the additive-group Hopf algebra by the Hopf ideal generated by xᵖ, and identifies its functor of points with these p-nilpotent elements.

The Hopf-ideal check is the freshman's dream in characteristic p: because x is primitive, Δ x = x ⊗ 1 + 1 ⊗ x, and in characteristic p Δ(xᵖ) = (x ⊗ 1 + 1 ⊗ x)ᵖ = xᵖ ⊗ 1 + 1 ⊗ xᵖ ∈ (xᵖ) ⊗ R[x] + R[x] ⊗ (xᵖ) (TauCeti.AdditiveGroup.comul_ι_pow, the shared primitivity of xᵖ). The counit vanishes on xᵖ since ε x = 0, and the antipode preserves (xᵖ) since S(xᵖ) = (-x)ᵖ. Mathlib's quotient Hopf-algebra instance then equips R[x] / (xᵖ) with its Hopf structure through the bridge instances of TauCeti.Algebra.HopfAlgebra.HopfIdeal.Basic.

The functor of points is recovered by pre-composing points of αₚ with the quotient map R[x] → R[x] / (xᵖ) (a bialgebra morphism, hence a convolution homomorphism through TauCeti.AlgHom.mapDomain) and reading the resulting 𝔾ₐ-point off with TauCeti.AdditiveGroup.gaPointsMulEquiv. The image consists of exactly the p-nilpotent elements, and the pre-composition map is injective because the quotient map is surjective, so αₚ(A) is the additive group of p-nilpotent elements of A (those a with aᵖ = 0). This exhibits αₚ as a non-reduced affine group scheme, the additive companion of the μ_p example of TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.NotReduced.

Main declarations

• TauCeti.AlphaP.hopfIdeal: the Hopf ideal (xᵖ) of the additive-group Hopf algebra.
• TauCeti.AlphaP.map_augmentation_frobeniusBialgHom_eq_hopfIdeal: mapping the augmentation Hopf ideal along Frobenius gives TauCeti.AlphaP.hopfIdeal.
• TauCeti.AlphaP.CoordinateRing: the coordinate Hopf algebra R[x] / (xᵖ) of αₚ.
• TauCeti.AlphaP.pointsHom: the injective homomorphism from the convolution group of points of αₚ to the additive group Multiplicative A, landing in the p-nilpotent elements.
• TauCeti.AlphaP.mem_range_pointsHom_iff: a point value a comes from αₚ iff aᵖ = 0, so the functor of points of αₚ is the p-nilpotent elements of the additive group.
• TauCeti.AlphaP.pNilpotent: the p-nilpotent elements as a subgroup of the additive group.
• TauCeti.AlphaP.pointsMulEquiv: the group isomorphism identifying the points of αₚ with the p-nilpotent subgroup.

See also

The Hopf structure on the additive group is Tau Ceti's TauCeti.Algebra.HopfAlgebra.SymmetricAlgebra.Basic and TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Basic; the Hopf-ideal quotient machinery and its bridge to Mathlib's quotient Hopf algebra are TauCeti.Algebra.HopfAlgebra.HopfIdeal.Basic. The primitivity of xᵖ reuses TauCeti.AdditiveGroup.comul_ι_pow of TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Frobenius; the tensor-product bialgebra structure is from Mathlib.

noncomputable def TauCeti.AlphaP.hopfIdeal {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : HopfIdeal R (SymmetricAlgebra R R)

The Hopf ideal (xᵖ) of the additive group. For R of prime characteristic p, the principal ideal generated by xᵖ in the coordinate Hopf algebra R[x] of 𝔾ₐ is a Hopf ideal: its comultiplication lands in (xᵖ) ⊗ R[x] + R[x] ⊗ (xᵖ), its counit vanishes, and it is antipode-stable. Its quotient is the coordinate ring of the Frobenius kernel group scheme αₚ.

Equations

• TauCeti.AlphaP.hopfIdeal p = TauCeti.HopfIdeal.ofIdeal (Ideal.span {(SymmetricAlgebra.ι R R) 1 ^ p}) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.AlphaP.hopfIdeal_toIdeal {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : (hopfIdeal p).toIdeal = Ideal.span {(SymmetricAlgebra.ι R R) 1 ^ p}

@[simp]

theorem TauCeti.AlphaP.map_augmentation_frobeniusBialgHom_eq_hopfIdeal {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : (HopfIdeal.augmentation R (SymmetricAlgebra R R)).map (AdditiveGroup.frobeniusBialgHom R p) = hopfIdeal p

Mapping the augmentation Hopf ideal of the additive group along the Frobenius coordinate endomorphism x ↦ xᵖ gives the Hopf ideal (xᵖ) defining αₚ. This is the concrete ideal identification relating αₚ to the generic kernel construction for affine group schemes.

@[reducible, inline]

noncomputable abbrev TauCeti.AlphaP.CoordinateRing {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : Type u

The coordinate Hopf algebra of αₚ, the quotient R[x] / (xᵖ). It carries a Hopf algebra structure through the bridge instances of TauCeti.Algebra.HopfAlgebra.HopfIdeal.Basic.

Equations

• TauCeti.AlphaP.CoordinateRing p = (SymmetricAlgebra R R ⧸ (TauCeti.AlphaP.hopfIdeal p).toIdeal)

@[simp]

theorem TauCeti.AlphaP.mk_ι_pow_eq_zero {R : Type u} [CommRing R] (p : ℕ) : (Ideal.Quotient.mk (Ideal.span {(SymmetricAlgebra.ι R R) 1 ^ p})) ((SymmetricAlgebra.ι R R) 1) ^ p = 0

The class of x in the coordinate ring of αₚ is p-nilpotent: its p-th power is 0.

The left-hand side is stated over Ideal.span {x ^ p} rather than (hopfIdeal p).toIdeal so that it is in simp normal form: hopfIdeal_toIdeal is itself @[simp], so a statement phrased over .toIdeal would be rewritten out from under this lemma and it could never fire. The two ideals are definitionally equal (hopfIdeal_toIdeal is rfl), so this still applies to goals phrased either way. In this form the statement needs neither primality of p nor CharP R p.

theorem TauCeti.AlphaP.mk_ι_ne_zero {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [Nontrivial R] : (Ideal.Quotient.mk (hopfIdeal p).toIdeal) ((SymmetricAlgebra.ι R R) 1) ≠ 0

The class of x in the coordinate ring of αₚ is nonzero over a nontrivial base: the dual-number test algebra R[ε] receives x ↦ ε, sending the relation xᵖ to εᵖ = 0 (as p ≥ 2) but not x itself. So xᵖ does not divide x in R[x].

theorem TauCeti.AlphaP.coordinateRing_not_isReduced {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [Nontrivial R] : ¬IsReduced (CoordinateRing p)

The coordinate ring of αₚ is not reduced. Over a nontrivial base of characteristic p, the class of x is a nonzero nilpotent (x̄ᵖ = 0), so R[x] / (xᵖ) is non-reduced. This is the additive companion of the non-reduced μ_p example.

noncomputable def TauCeti.AlphaP.pointsHom {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) →* Multiplicative A

The functor of points of αₚ, as a subgroup of the additive group. Pre-composition of a point of αₚ with the quotient map R[x] → R[x] / (xᵖ) gives a point of 𝔾ₐ, read off as an element of Multiplicative A by TauCeti.AdditiveGroup.gaPointsMulEquiv.

Equations

• TauCeti.AlphaP.pointsHom p = TauCeti.AdditiveGroup.gaPointsMulEquiv.toMonoidHom.comp (TauCeti.AlgHom.mapDomain (Bialgebra.Quotient.mkBialgHom (TauCeti.AlphaP.hopfIdeal p).toIdeal))

@[simp]

theorem TauCeti.AlphaP.toAdd_pointsHom {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)) : Multiplicative.toAdd ((pointsHom p) F) = F.ofConv ((Ideal.Quotient.mk (hopfIdeal p).toIdeal) ((SymmetricAlgebra.ι R R) 1))

A point of αₚ is sent to the value at x of its underlying R[x]-point: the element F(x̄) of A, where x̄ is the class of x in the coordinate ring.

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

The points homomorphism of αₚ is injective, because the quotient map R[x] → R[x] / (xᵖ) is surjective, so pre-composition with it is injective on algebra homomorphisms.

theorem TauCeti.AlphaP.mem_range_pointsHom_iff {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] (a : Multiplicative A) : a ∈ (pointsHom p).range ↔ Multiplicative.toAdd a ^ p = 0

The functor of points of αₚ is the p-nilpotent elements of the additive group. An element a of A is the value of a point of αₚ iff aᵖ = 0.

noncomputable def TauCeti.AlphaP.pNilpotent {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] : Subgroup (Multiplicative A)

The p-nilpotent subgroup of the additive group. For a commutative R-algebra A, the elements a : A with aᵖ = 0 form a subgroup of the additive group Multiplicative A: they are exactly the image of the points homomorphism of αₚ, hence closed under the group operations.

Equations

• TauCeti.AlphaP.pNilpotent p = (TauCeti.AlphaP.pointsHom p).range

@[simp]

theorem TauCeti.AlphaP.mem_pNilpotent_iff {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] (a : Multiplicative A) : a ∈ pNilpotent p ↔ Multiplicative.toAdd a ^ p = 0

Membership in the p-nilpotent subgroup is the relation aᵖ = 0.

noncomputable def TauCeti.AlphaP.pointsMulEquiv {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) ≃* ↥(pNilpotent p)

The functor of points of αₚ as the p-nilpotent subgroup. The points homomorphism corestricts to a group isomorphism from the convolution group of points of αₚ onto the p-nilpotent subgroup of the additive group, so αₚ(A) is the group of p-nilpotent elements of A.

Equations

• TauCeti.AlphaP.pointsMulEquiv p = MonoidHom.ofInjective ⋯

@[simp]

theorem TauCeti.AlphaP.coe_pointsMulEquiv {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)) : ↑((pointsMulEquiv p) F) = (pointsHom p) F

The points isomorphism of αₚ agrees with the points homomorphism on underlying elements.

@[simp]

theorem TauCeti.AlphaP.pointsHom_pointsMulEquiv_symm {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] (a : ↥(pNilpotent p)) : (pointsHom p) ((pointsMulEquiv p).symm a) = ↑a

The inverse of the points isomorphism of αₚ is a section of the points homomorphism.