Documentation

TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.ReducedPoints

Points of αₚ over reduced algebras #

The Frobenius kernel αₚ has nontrivial points only on algebras with nilpotents. More precisely, its points on a commutative algebra A are the elements whose p-th power vanishes. If A is reduced, such an element is zero, so the p-nilpotent subgroup is trivial and the convolution group αₚ(A) has one element.

This is an important qualification to the non-reduced worked example: although the group scheme αₚ itself is nontrivial, it is invisible on every reduced test algebra. In particular its field-valued points are trivial. Non-reduced test algebras, such as dual numbers, are required to detect it.

The proofs use the description of the functor of points in TauCeti.Algebra.AlgebraicGroup.AdditiveFrobeniusKernel.Basic and Mathlib's eq_zero_of_pow_eq_zero for reduced rings.

Main declarations #

source
theorem TauCeti.AlphaP.pNilpotent_eq_bot_of_isReduced {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] [IsReduced A] :
pNilpotent p = ⊥

Over a reduced algebra, the subgroup of p-nilpotent elements is the trivial subgroup.

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

Every point of αₚ over a reduced algebra maps to the identity element of the additive group under the canonical inclusion.

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

Every point of αₚ over a reduced algebra is the identity for convolution.

source
@[instance_reducible]
noncomputable instance TauCeti.AlphaP.instUniquePointsOfIsReduced {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] [IsReduced A] :
Unique (WithConv (CoordinateRing p →ₐ[R] A))

The convolution group of αₚ-points over a reduced algebra has a unique element.

Equations
source
noncomputable def TauCeti.AlphaP.reducedPointsMulEquivPUnit {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] [IsReduced A] :
WithConv (CoordinateRing p →ₐ[R] A) ≃* PUnit.{u_1 + 1}

Over a reduced algebra, the functor of points of αₚ is canonically isomorphic to the trivial group.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlphaP.reducedPointsMulEquivPUnit_apply {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] [IsReduced A] (F : WithConv (CoordinateRing p →ₐ[R] A)) :
    (reducedPointsMulEquivPUnit p) F = PUnit.unit
    source
    @[simp]
    theorem TauCeti.AlphaP.reducedPointsMulEquivPUnit_symm_apply {R : Type u} [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {A : Type v} [CommRing A] [Algebra R A] [IsReduced A] (x : PUnit.{u_1 + 1}) :
    (reducedPointsMulEquivPUnit p).symm x = 1