Coordinates of the perfection of a monoid

For a commutative monoid M, Mathlib's Perfection M p is the monoid of compatible systems (xₙ)ₙ with xₙ₊₁ ^ p = xₙ. If every element of M has a p-th root, every element of M starts such a system, and more generally every coordinate map Perfection M p → M is surjective. Mathlib proves this for rings of characteristic p with surjective Frobenius (Perfection.coeff_surjective); the statement here needs no ring structure, and applies for instance to the multiplicative monoid of an algebraically closed field of any characteristic.

Main results

• Perfection.coeffMonoidHom_surjective: if x ↦ x ^ p is surjective on M, so is every coordinate map Perfection.coeffMonoidHom M p n.
• Perfection.coeff_eq_zero_iff: in the perfection of a reduced ring of characteristic p, an element vanishes as soon as one of its coordinates does.
• PreTilt.coeff_eq_zero_iff: the same for the tilt PreTilt O p when O ⧸ p is reduced.
• TauCeti.dvd_of_compatible_roots: in a compatible root sequence, later roots divide earlier ones.

theorem Perfection.coeffMonoidHom_surjective {M : Type u_1} [CommMonoid M] {p : ℕ} (h : Function.Surjective fun (x : M) => x ^ p) (n : ℕ) : Function.Surjective ⇑(coeffMonoidHom M p n)

If every element of M has a p-th root, every coordinate of Perfection M p is surjective.

@[simp]

theorem Perfection.coeff_eq_zero_iff {p : ℕ} {R : Type u_2} [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [IsReduced R] (n : ℕ) {f : Perfection R p} : (coeff R p n) f = 0 ↔ f = 0

In the perfection of a reduced ring, each coordinate detects zero. For f in the perfection of a reduced ring of characteristic p, coeff n f = 0 if and only if f = 0.

@[simp]

theorem PreTilt.coeff_eq_zero_iff {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsReduced (ModP O p)] (n : ℕ) {f : PreTilt O p} : (coeff n) f = 0 ↔ f = 0

If O ⧸ p is reduced, each coordinate of the tilt detects zero. For f in PreTilt O p, coeff n f = 0 if and only if f = 0.

theorem TauCeti.dvd_of_compatible_roots {R : Type u_1} [CommMonoid R] {p : ℕ} {r : ℕ → R} (hr : ∀ (n : ℕ), r (n + 1) ^ p = r n) {m n : ℕ} (hmn : m ≤ n) : r n ∣ r m

In a compatible root sequence, every later root divides every earlier root.