Ring Perfection and Tilt

In this file we define the perfection of a ring of characteristic p, and the tilt of a field given a valuation to ℝ≥0.

TODO

Define the valuation on the tilt, and define a characteristic predicate for the tilt.

def Perfection (α : Type u₁) [Pow α ℕ] (p : ℕ) : Type u₁

The perfection of a monoid α, defined to be the projective limit of α using the p-th power maps α → α indexed by the natural numbers, implemented as { f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }.

If α is a ring with characteristic p and p is prime, Perfection α p is also a ring.

@[deprecated Perfection (since := "2026-03-03")]

def Ring.Perfection (α : Type u₁) [Pow α ℕ] (p : ℕ) : Type u₁

Alias of Perfection.

---

The perfection of a monoid α, defined to be the projective limit of α using the p-th power maps α → α indexed by the natural numbers, implemented as { f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }.

If α is a ring with characteristic p and p is prime, Perfection α p is also a ring.

def Perfection.submonoid (M : Type u_1) [CommMonoid M] (p : ℕ) : Submonoid (ℕ → M)

Perfection M p as a submonoid of ℕ → M.

@[deprecated Perfection.submonoid (since := "2026-03-03")]

def Monoid.perfection (M : Type u_1) [CommMonoid M] (p : ℕ) : Submonoid (ℕ → M)

Alias of Perfection.submonoid.

---

Perfection M p as a submonoid of ℕ → M.

@[implicit_reducible]

instance Perfection.instCommMonoid (M : Type u_1) [CommMonoid M] (p : ℕ) : CommMonoid (Perfection M p)

def Perfection.coeffMonoidHom (M : Type u_1) [CommMonoid M] (p n : ℕ) : Perfection M p →* M

The n-th coefficient of an element of the perfection.

def Perfection.pthRootMonoidHom (M : Type u_1) [CommMonoid M] (p : ℕ) : Perfection M p →* Perfection M p

The p-th root of an element of the perfection.

theorem Perfection.extMonoid {M : Type u_1} [CommMonoid M] {p : ℕ} {f g : Perfection M p} (h : ∀ (n : ℕ), (coeffMonoidHom M p n) f = (coeffMonoidHom M p n) g) : f = g

theorem Perfection.extMonoid_iff {M : Type u_1} [CommMonoid M] {p : ℕ} {f g : Perfection M p} : f = g ↔ ∀ (n : ℕ), (coeffMonoidHom M p n) f = (coeffMonoidHom M p n) g

@[simp]

theorem Perfection.coeffMonoidHom_mk {M : Type u_1} [CommMonoid M] {p : ℕ} (f : ℕ → M) (hf : ∀ (n : ℕ), f (n + 1) ^ p = f n) (n : ℕ) : (coeffMonoidHom M p n) ⟨f, hf⟩ = f n

theorem Perfection.coeffMonoidHom_pthRootMonoidHom {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p n) ((pthRootMonoidHom M p) f) = (coeffMonoidHom M p (n + 1)) f

theorem Perfection.coeffMonoidHom_pow_p {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p (n + 1)) (f ^ p) = (coeffMonoidHom M p n) f

@[simp]

theorem Perfection.coeffMonoidHom_pow_p' {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p (n + 1)) f ^ p = (coeffMonoidHom M p n) f

instance Perfection.instPerfectRing {M : Type u_1} [CommMonoid M] {p : ℕ} : PerfectRing (Perfection M p) p

@[simp]

theorem Perfection.pthRootMonoidHom_eq_powMulEquiv_symm {M : Type u_1} [CommMonoid M] {p : ℕ} : pthRootMonoidHom M p = ↑(powMulEquiv (Perfection M p) p).symm

theorem Perfection.coe_pthRootMonoidHom_eq_powMulEquiv_symm {M : Type u_1} [CommMonoid M] {p : ℕ} : ⇑(pthRootMonoidHom M p) = ⇑(powMulEquiv (Perfection M p) p).symm

@[simp]

theorem Perfection.coeffMonoidHom_symm_powMulEquiv {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p n) ((powMulEquiv (Perfection M p) p).symm f) = (coeffMonoidHom M p (n + 1)) f

@[simp]

theorem Perfection.coeffMonoidHom_iterate_symm_powMulEquiv {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ) : (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f

theorem Perfection.coeffMonoidHom_pow_p_pow {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (m n : ℕ) : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f

@[simp]

theorem Perfection.coeffMonoidHom_pow_p_pow' {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (m n : ℕ) : (coeffMonoidHom M p (m + n)) f ^ p ^ n = (coeffMonoidHom M p m) f

@[simp]

theorem Perfection.coeffMonoidHom_pow_p_pow_self {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p n) f ^ p ^ n = (coeffMonoidHom M p 0) f

theorem Perfection.coeffMonoidHom_powMonoidHom {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ) : (coeffMonoidHom M p (n + 1)) ((powMonoidHom p) f) = (coeffMonoidHom M p n) f

theorem Perfection.coeffMonoidHom_iterate_powMonoidHom {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ) : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f

theorem Perfection.coeffMonoidHom_iterate_powMonoidHom' {M : Type u_1} [CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ) (hmn : m ≤ n) : (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m)) f

noncomputable def Perfection.liftMonoidHom (p : ℕ) (M : Type u_2) [CommMonoid M] [PerfectRing M p] (N : Type u_3) [CommMonoid N] : (M →* N) ≃* (M →* Perfection N p)

Given monoids M and N, with M being perfect, any homomorphism M →+* N can be lifted uniquely to a homomorphism M →* Perfection N p.

@[simp]

theorem Perfection.liftMonoidHom_symm_apply (p : ℕ) (M : Type u_2) [CommMonoid M] [PerfectRing M p] (N : Type u_3) [CommMonoid N] (hmn : M →* Perfection N p) : (liftMonoidHom p M N).symm hmn = (coeffMonoidHom N p 0).comp hmn

@[simp]

theorem Perfection.coeffMonoidHom_zero_liftMonoidHom (p : ℕ) {M : Type u_2} {N : Type u_3} [CommMonoid M] [PerfectRing M p] [CommMonoid N] (e : M →* N) (x : M) : (coeffMonoidHom N p 0) (((liftMonoidHom p M N) e) x) = e x

def Perfection.mapMonoidHom (p : ℕ) {M : Type u_2} {N : Type u_3} [CommMonoid M] [CommMonoid N] (φ : M →* N) : Perfection M p →* Perfection N p

A monoid homomorphism M →* N induces Perfection M p →* Perfection N p.

@[simp]

theorem Perfection.coeffMonoidHom_mapMonoidHom (p : ℕ) {M : Type u_2} {N : Type u_3} [CommMonoid M] [CommMonoid N] (φ : M →* N) (f : Perfection M p) (n : ℕ) : (coeffMonoidHom N p n) ((mapMonoidHom p φ) f) = φ ((coeffMonoidHom M p n) f)

def Perfection.subsemiring (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Subsemiring (ℕ → R)

Perfection R p as a subsemiring of ℕ → R.

@[deprecated Perfection.subsemiring (since := "2026-03-03")]

def Ring.perfectionSubsemiring (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Subsemiring (ℕ → R)

Alias of Perfection.subsemiring.

---

Perfection R p as a subsemiring of ℕ → R.

@[implicit_reducible]

instance Perfection.instCommSemiring (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : CommSemiring (Perfection R p)

instance Perfection.instCharP (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : CharP (Perfection R p) p

def Perfection.coeff (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : Perfection R p →+* R

The n-th coefficient of an element of the perfection.

def Perfection.pthRoot (R : Type u_1) [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Perfection R p →+* Perfection R p

The p-th root of an element of the perfection.

The preferred way to use this is (frobeniusEquiv (Perfection R p) p).symm.

theorem Perfection.ext {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {f g : Perfection R p} (h : ∀ (n : ℕ), (coeff R p n) f = (coeff R p n) g) : f = g

theorem Perfection.ext_iff {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {f g : Perfection R p} : f = g ↔ ∀ (n : ℕ), (coeff R p n) f = (coeff R p n) g

@[simp]

theorem Perfection.pthRoot_eq_symm_frobeniusEquiv {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : pthRoot R p = ↑(frobeniusEquiv (Perfection R p) p).symm

theorem Perfection.coe_pthRoot_eq_symm_frobeniusEquiv {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : ⇑(pthRoot R p) = ⇑(frobeniusEquiv (Perfection R p) p).symm

@[simp]

theorem Perfection.coeffMonoidHom_eq_coeff {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : ⇑(coeffMonoidHom R p n) = ⇑(coeff R p n)

theorem Perfection.pthRootMonoidHom_eq_pthRoot {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : ⇑(pthRootMonoidHom R p) = ⇑(pthRoot R p)

theorem Perfection.pthRootMonoidHom_eq_symm_frobeniusEquiv {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : ⇑(pthRootMonoidHom R p) = ⇑↑(frobeniusEquiv (Perfection R p) p).symm

theorem Perfection.coeff_toMonoidHom {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : ↑(coeff R p n) = coeffMonoidHom R p n

@[simp]

theorem Perfection.coeff_mk {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : ℕ → R) (hf : ∀ (n : ℕ), f (n + 1) ^ p = f n) (n : ℕ) : (coeff R p n) ⟨f, hf⟩ = f n

@[simp]

theorem Perfection.coeff_symm_frobeniusEquiv {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n : ℕ) : (coeff R p n) ((frobeniusEquiv (Perfection R p) p).symm f) = (coeff R p (n + 1)) f

@[simp]

theorem Perfection.coeff_iterate_symm_frobeniusEquiv {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n m : ℕ) : (coeff R p n) ((⇑(frobeniusEquiv (Perfection R p) p).symm)^[m] f) = (coeff R p (n + m)) f

theorem Perfection.coeff_pow_p {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n : ℕ) : (coeff R p (n + 1)) (f ^ p) = (coeff R p n) f

@[simp]

theorem Perfection.coeff_pow_p' {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n : ℕ) : (coeff R p (n + 1)) f ^ p = (coeff R p n) f

@[simp]

theorem Perfection.coeff_frobenius {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n : ℕ) : (coeff R p (n + 1)) ((frobenius (Perfection R p) p) f) = (coeff R p n) f

@[simp]

theorem Perfection.coeff_iterate_frobenius {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n m : ℕ) : (coeff R p (n + m)) ((⇑(frobenius (Perfection R p) p))^[m] f) = (coeff R p n) f

theorem Perfection.coeff_iterate_frobenius' {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (f : Perfection R p) (n m : ℕ) (hmn : m ≤ n) : (coeff R p n) ((⇑(frobenius (Perfection R p) p))^[m] f) = (coeff R p (n - m)) f

theorem Perfection.pthRoot_frobenius {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : (pthRoot R p).comp (frobenius (Perfection R p) p) = RingHom.id (Perfection R p)

theorem Perfection.frobenius_pthRoot {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : (frobenius (Perfection R p) p).comp (pthRoot R p) = RingHom.id (Perfection R p)

theorem Perfection.coeff_add_ne_zero {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {f : Perfection R p} {n : ℕ} (hfn : (coeff R p n) f ≠ 0) (k : ℕ) : (coeff R p (n + k)) f ≠ 0

theorem Perfection.coeff_ne_zero_of_le {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {f : Perfection R p} {m n : ℕ} (hfm : (coeff R p m) f ≠ 0) (hmn : m ≤ n) : (coeff R p n) f ≠ 0

theorem Perfection.coeff_surjective {R : Type u_1} [CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (h : Function.Surjective ⇑(frobenius R p)) (n : ℕ) : Function.Surjective ⇑(coeff R p n)

noncomputable def Perfection.lift (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] : (R →+* S) ≃ (R →+* Perfection S p)

Given rings R and S of characteristic p, with R being perfect, any homomorphism R →+* S can be lifted to a homomorphism R →+* Perfection S p.

@[simp]

theorem Perfection.lift_apply_apply_coe (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (f : R →+* S) (r : R) (n : ℕ) : ↑(((lift p R S) f) r) n = f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)

@[simp]

theorem Perfection.lift_symm_apply (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (f : R →+* Perfection S p) : (lift p R S).symm f = (coeff S p 0).comp f

theorem Perfection.hom_ext (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p] {f g : R →+* Perfection S p} (hfg : ∀ (x : R), (coeff S p 0) (f x) = (coeff S p 0) (g x)) : f = g

def Perfection.map {R : Type u_1} [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) : Perfection R p →+* Perfection S p

A ring homomorphism R →+* S induces Perfection R p →+* Perfection S p.

@[simp]

theorem Perfection.coeff_map {R : Type u_1} [CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) (f : Perfection R p) (n : ℕ) : (coeff S p n) ((map p φ) f) = φ ((coeff R p n) f)

def Perfection.subring (R : Type u_1) [CommRing R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Subring (ℕ → R)

Perfection R p as a semiring of ℕ → R.

@[deprecated Perfection.subring (since := "2026-03-03")]

def Ring.perfectionSubring (R : Type u_1) [CommRing R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Subring (ℕ → R)

Alias of Perfection.subring.

---

Perfection R p as a semiring of ℕ → R.

@[implicit_reducible]

instance Perfection.instRing (R : Type u_1) [CommRing R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : Ring (Perfection R p)

@[implicit_reducible]

instance Perfection.instCommRing (R : Type u_1) [CommRing R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : CommRing (Perfection R p)

@[simp]

theorem Perfection.coeff_mapMonoidHom {p : ℕ} [Fact (Nat.Prime p)] {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommRing N] [CharP N p] (e : M →* N) (n : ℕ) (x : Perfection M p) : (coeff N p n) ((mapMonoidHom p e) x) = e ((coeffMonoidHom M p n) x)

structure PerfectionMap (p : ℕ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₂} [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* R) : Prop

A perfection map to a ring of characteristic p is a map that is isomorphic to its perfection.

• injective ⦃x y : P⦄ : (∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) → x = y
• surjective (f : ℕ → R) : (∀ (n : ℕ), f (n + 1) ^ p = f n) → ∃ (x : P), ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n

theorem PerfectionMap.mk' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {f : P →+* R} (g : P ≃+* Perfection R p) (hfg : (Perfection.lift p P R) f = ↑g) : PerfectionMap p f

Create a PerfectionMap from an isomorphism to the perfection.

theorem PerfectionMap.of (p : ℕ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] : PerfectionMap p (Perfection.coeff R p 0)

The canonical perfection map from the perfection of a ring.

theorem PerfectionMap.id (p : ℕ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] : PerfectionMap p (RingHom.id R)

For a perfect ring, it itself is the perfection.

noncomputable def PerfectionMap.equiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) : P ≃+* Perfection R p

A perfection map induces an isomorphism to the perfection.

theorem PerfectionMap.equiv_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (x : P) : m.equiv x = ((Perfection.lift p P R) π) x

theorem PerfectionMap.comp_equiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (x : P) : (Perfection.coeff R p 0) (m.equiv x) = π x

theorem PerfectionMap.comp_equiv' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) : (Perfection.coeff R p 0).comp ↑m.equiv = π

theorem PerfectionMap.comp_symm_equiv {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (f : Perfection R p) : π (m.equiv.symm f) = (Perfection.coeff R p 0) f

theorem PerfectionMap.comp_symm_equiv' {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) : π.comp ↑m.equiv.symm = Perfection.coeff R p 0

noncomputable def PerfectionMap.lift (p : ℕ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) : (R →+* S) ≃ (R →+* P)

Given rings R and S of characteristic p, with R being perfect, any homomorphism R →+* S can be lifted to a homomorphism R →+* P, where P is any perfection of S.

@[simp]

theorem PerfectionMap.lift_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) (f : R →+* P) : (lift p R S P π m).symm f = π.comp f

@[simp]

theorem PerfectionMap.lift_apply (p : ℕ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) (f : R →+* S) : (lift p R S P π m) f = (↑m.equiv.symm).comp ((Perfection.lift p R S) f)

theorem PerfectionMap.hom_ext {p : ℕ} [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) {f g : R →+* P} (hfg : ∀ (x : R), π (f x) = π (g x)) : f = g

noncomputable def PerfectionMap.map (p : ℕ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [PerfectRing Q p] {π : P →+* R} : PerfectionMap p π → {σ : Q →+* S} → (n : PerfectionMap p σ) → (φ : R →+* S) → P →+* Q

A ring homomorphism R →+* S induces P →+* Q, a map of the respective perfections.

theorem PerfectionMap.comp_map (p : ℕ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [PerfectRing Q p] {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) : σ.comp (map p m n φ) = φ.comp π

theorem PerfectionMap.map_map (p : ℕ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [PerfectRing Q p] {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) (x : P) : σ ((map p m n φ) x) = φ (π x)

theorem PerfectionMap.map_eq_map (p : ℕ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) : map p ⋯ ⋯ φ = Perfection.map p φ

@[reducible, inline]

abbrev ModP (O : Type u₂) [CommRing O] (p : ℕ) : Type u₂

O/(p) for O, ring of integers of K.

instance ModP.instCharPOfPrimeOfFactNotIsUnitCast (O : Type u₂) [CommRing O] (p : ℕ) [Fact (Nat.Prime p)] [hvp : Fact ¬IsUnit ↑p] : CharP (ModP O p) p

instance ModP.instNontrivialOfPrimeOfFactNotIsUnitCast (O : Type u₂) [CommRing O] (p : ℕ) [hp : Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : Nontrivial (ModP O p)

noncomputable def ModP.preVal (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (p : ℕ) (x : ModP O p) : NNReal

For a field K with valuation v : K → ℝ≥0 and ring of integers O, a function O/(p) → ℝ≥0 that sends 0 to 0 and x + (p) to v(x) as long as x ∉ (p).

theorem ModP.preVal_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {p : ℕ} : preVal K v O p 0 = 0

theorem ModP.preVal_mk {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} {x : O} (hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0) : preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)

theorem ModP.preVal_mul {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} {x y : ModP O p} (hxy0 : x * y ≠ 0) : preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

theorem ModP.preVal_add {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} (x y : ModP O p) : preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

theorem ModP.v_p_lt_preVal {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} {x : ModP O p} : v ↑p < preVal K v O p x ↔ x ≠ 0

theorem ModP.preVal_eq_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} {x : ModP O p} : preVal K v O p x = 0 ↔ x = 0

theorem ModP.v_p_lt_val {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} {x : O} : v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0

theorem ModP.mul_ne_zero_of_pow_p_ne_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ModP O p} (hx : x ^ p ≠ 0) (hy : y ^ p ≠ 0) : x * y ≠ 0

def PreTilt (O : Type u₂) [CommRing O] (p : ℕ) : Type u₂

Perfection of O/(p) where O is the ring of integers of K.

@[implicit_reducible]

instance PreTilt.instCommRing (O : Type u₂) [CommRing O] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : CommRing (PreTilt O p)

instance PreTilt.instCharP (O : Type u₂) [CommRing O] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : CharP (PreTilt O p) p

instance PreTilt.instPerfectRing (O : Type u₂) [CommRing O] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : PerfectRing (PreTilt O p) p

def PreTilt.coeff {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (n : ℕ) : PreTilt O p →+* ModP O p

The n-th coefficient of an element of the perfection of O/(p).

theorem PreTilt.coeff_def {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (n : ℕ) (x : PreTilt O p) : (coeff n) x = (Perfection.coeff (ModP O p) p n) x

@[simp]

theorem PreTilt.coeff_frobenius {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (n : ℕ) (x : PreTilt O p) : (coeff (n + 1)) ((frobenius (PreTilt O p) p) x) = (coeff n) x

@[simp]

theorem PreTilt.coeff_iterate_frobenius {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (m n : ℕ) (x : PreTilt O p) : (coeff (m + n)) ((⇑(frobenius (PreTilt O p) p))^[n] x) = (coeff m) x

theorem PreTilt.coeff_iterate_frobenius' {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) {m n : ℕ} (hmn : m ≤ n) : (coeff n) ((⇑(frobenius (PreTilt O p) p))^[m] x) = (coeff (n - m)) x

A variant of PreTilt.coeff_iterate_frobenius using m-n and n.

@[simp]

theorem PreTilt.coeff_pow_p {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) (n : ℕ) : (coeff (n + 1)) x ^ p = (coeff n) x

@[simp]

theorem PreTilt.coeff_frobeniusEquiv_symm {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (n : ℕ) (x : PreTilt O p) : (coeff n) ((frobeniusEquiv (PreTilt O p) p).symm x) = (coeff (n + 1)) x

@[simp]

theorem PreTilt.coeff_iterate_frobeniusEquiv_symm {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (m n : ℕ) (x : PreTilt O p) : (coeff m) ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x) = (coeff (m + n)) x

noncomputable def PreTilt.valAux (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (f : PreTilt O p) : NNReal

The valuation Perfection(O/(p)) → ℝ≥0 as a function. Given f ∈ Perfection(O/(p)), if f = 0 then output 0; otherwise output preVal(f(n))^(p^n) for any n such that f(n) ≠ 0.

theorem PreTilt.coeff_nat_find_add_ne_zero {O : Type u₂} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] {f : PreTilt O p} {h : ∃ (n : ℕ), (coeff n) f ≠ 0} (k : ℕ) : (coeff (Nat.find h + k)) f ≠ 0

theorem PreTilt.valAux_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : valAux K v O p 0 = 0

theorem PreTilt.valAux_eq {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] {f : PreTilt O p} {n : ℕ} (hfn : (coeff n) f ≠ 0) : valAux K v O p f = ModP.preVal K v O p ((coeff n) f) ^ p ^ n

theorem PreTilt.valAux_one {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : valAux K v O p 1 = 1

theorem PreTilt.valAux_mul {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (f g : PreTilt O p) : valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

theorem PreTilt.valAux_add {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (f g : PreTilt O p) : valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

noncomputable def PreTilt.val (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : Valuation (PreTilt O p) NNReal

The valuation Perfection(O/(p)) → ℝ≥0. Given f ∈ Perfection(O/(p)), if f = 0 then output 0; otherwise output preVal(f(n))^(p^n) for any n such that f(n) ≠ 0.

theorem PreTilt.map_eq_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] {f : PreTilt O p} : (val K v O hv p) f = 0 ↔ f = 0

theorem PreTilt.isDomain (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] : IsDomain (PreTilt O p)

def Tilt (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ℕ) [Fact (Nat.Prime p)] [hvp : Fact (v ↑p ≠ 1)] : Type u₂

The tilt of a field, as defined in Perfectoid Spaces by Peter Scholze, as in [scholze2011perfectoid]. Given a field K with valuation K → ℝ≥0 and ring of integers O, this is implemented as the fraction field of the perfection of O/(p).

@[implicit_reducible]

noncomputable instance Tilt.instField (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ℕ) [Fact (Nat.Prime p)] [hvp : Fact (v ↑p ≠ 1)] : Field (Tilt K v O hv p)