Roots of elements of perfect rings

Let R be a perfect ring of exponential characteristic p. Every x ∈ R has a unique p ^ n-th root (iterateFrobeniusEquiv R p n).symm x for each n. This file records how these roots relate to each other, the fact that R is reduced when p is prime, and the fact that p-th powers can be cancelled from annihilation relations.

Main results

• TauCeti.iterateFrobeniusEquiv_symm_add_pow: the p ^ n-th power of the p ^ (m + n)-th root of x is its p ^ m-th root.
• TauCeti.iterateFrobeniusEquiv_symm_succ_pow: the p-th power of the p ^ (n + 1)-th root of x is its p ^ n-th root.
• TauCeti.iterateFrobeniusEquiv_symm_dvd_of_le: deeper roots of x divide shallower ones.
• TauCeti.isReduced_of_perfectRing: a perfect ring of prime characteristic is reduced.
• TauCeti.mul_eq_zero_of_mul_pow_eq_zero_of_perfectRing: a * b ^ p = 0 implies a * b = 0.
• TauCeti.mul_iterateFrobeniusEquiv_symm_succ_eq_zero: an element killing the p ^ n-th root of x also kills its p ^ (n + 1)-th root.
• TauCeti.frobeniusEquiv_symm_smul: over a perfect ring of scalars, p-th roots are semilinear along the p-th root of the scalars.
• TauCeti.isRadical_iff_frobeniusEquiv_symm_mem: an ideal is radical exactly when it contains the p-th roots of its elements.
• Ideal.IsRadical.sup, Ideal.IsRadical.map, Ideal.IsRadical.map_inf: sums of radical ideals are radical, and extension along a homomorphism of perfect rings preserves radical ideals and their intersections. The first fails for general rings: in ℚ[x, y] the sum of the radical ideals (x) and (x - y ^ 2) is (x, y ^ 2), which is not radical.

@[simp]

theorem TauCeti.iterateFrobeniusEquiv_symm_add_pow {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (x : R) (m n : ℕ) : (iterateFrobeniusEquiv R p (m + n)).symm x ^ p ^ n = (iterateFrobeniusEquiv R p m).symm x

The p ^ n-th power of the p ^ (m + n)-th root of x is its p ^ m-th root.

@[simp]

theorem TauCeti.iterateFrobeniusEquiv_symm_succ_pow {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (x : R) (n : ℕ) : (iterateFrobeniusEquiv R p (n + 1)).symm x ^ p = (iterateFrobeniusEquiv R p n).symm x

The p-th power of the p ^ (n + 1)-th root of x is its p ^ n-th root.

theorem TauCeti.iterateFrobeniusEquiv_symm_dvd_of_le {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] (x : R) {m n : ℕ} (h : m ≤ n) : (iterateFrobeniusEquiv R p n).symm x ∣ (iterateFrobeniusEquiv R p m).symm x

Deeper roots of x divide shallower ones: the p ^ n-th root of x divides its p ^ m-th root when m ≤ n.

theorem TauCeti.isReduced_of_perfectRing (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] [hp : Fact (Nat.Prime p)] : IsReduced R

A perfect ring of prime characteristic p is reduced.

theorem TauCeti.mul_eq_zero_of_mul_pow_eq_zero_of_perfectRing {R : Type u_1} [CommSemiring R] {p : ℕ} [PerfectRing R p] {a b : R} (h : a * b ^ p = 0) : a * b = 0

In a perfect ring for the exponent p, if a kills b ^ p then a kills b.

theorem TauCeti.mul_iterateFrobeniusEquiv_symm_succ_eq_zero {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {x c : R} {n : ℕ} (h : c * (iterateFrobeniusEquiv R p n).symm x = 0) : c * (iterateFrobeniusEquiv R p (n + 1)).symm x = 0

If c kills the p ^ n-th root of x, then it kills the p ^ (n + 1)-th root of x.

theorem TauCeti.mul_iterateFrobeniusEquiv_symm_succ_pow_eq_zero {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {x c : R} {n k : ℕ} (hk : k ≠ 0) (h : c * (iterateFrobeniusEquiv R p n).symm x = 0) : c * (iterateFrobeniusEquiv R p (n + 1)).symm x ^ k = 0

If c kills the p ^ n-th root of x, then it kills every positive power of the p ^ (n + 1)-th root of x.

theorem TauCeti.frobeniusEquiv_symm_smul {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {A : Type u_2} [CommSemiring A] [ExpChar A p] [PerfectRing A p] [Algebra A R] (a : A) (x : R) : (frobeniusEquiv R p).symm (a • x) = (frobeniusEquiv A p).symm a • (frobeniusEquiv R p).symm x

Over a perfect ring of scalars A, the p-th root of R is semilinear along the p-th root of A: (a • x) ^ (1 / p) = a ^ (1 / p) • x ^ (1 / p).

theorem TauCeti.isRadical_iff_frobeniusEquiv_symm_mem {R : Type u_1} [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] [Fact (Nat.Prime p)] {I : Ideal R} : I.IsRadical ↔ ∀ x ∈ I, (frobeniusEquiv R p).symm x ∈ I

In a perfect ring of prime characteristic p, an ideal is radical exactly when it contains the p-th roots of its elements.

theorem Ideal.IsRadical.sup {R : Type u_1} [CommSemiring R] {I J : Ideal R} (p : ℕ) [Fact (Nat.Prime p)] [ExpChar R p] [PerfectRing R p] (hI : I.IsRadical) (hJ : J.IsRadical) : (I ⊔ J).IsRadical

In a perfect ring of prime characteristic, the sum of two radical ideals is radical: taking p-th roots is additive.

theorem Ideal.IsRadical.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [CommSemiring S] {I : Ideal R} [FunLike F R S] [RingHomClass F R S] (p : ℕ) [Fact (Nat.Prime p)] [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (hI : I.IsRadical) (φ : F) : (Ideal.map φ I).IsRadical

The extension of a radical ideal along a homomorphism of perfect rings of prime characteristic is radical.

theorem Ideal.IsRadical.map_inf {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [CommSemiring S] {I J : Ideal R} [FunLike F R S] [RingHomClass F R S] (p : ℕ) [Fact (Nat.Prime p)] [ExpChar R p] [PerfectRing R p] [ExpChar S p] [PerfectRing S p] (hI : I.IsRadical) (hJ : J.IsRadical) (φ : F) : Ideal.map φ (I ⊓ J) = Ideal.map φ I ⊓ Ideal.map φ J

Extension along a homomorphism of perfect rings of prime characteristic commutes with intersections of radical ideals.