mathlib documentation

ring_theory.perfection

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 monoid.perfection (M : Type u₁) [comm_monoid M] (p : ) :
submonoid ( → M)

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

Equations
def ring.perfection (R : Type u₁) [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] :

The perfection of a ring R with characteristic p, defined to be the projective limit of R using the Frobenius maps R → R indexed by the natural numbers, implemented as { f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }.

Equations
def perfection.coeff (R : Type u₁) [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] (n : ) :

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

Equations
@[ext]
theorem perfection.ext {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] {f g : (ring.perfection R p)} (h : ∀ (n : ), (perfection.coeff R p n) f = (perfection.coeff R p n) g) :
f = g
def perfection.pth_root (R : Type u₁) [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] :

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

Equations
@[simp]
theorem perfection.coeff_mk {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : → R) (hf : f ring.perfection R p) (n : ) :
(perfection.coeff R p n) f, hf⟩ = f n
theorem perfection.coeff_pth_root {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n : ) :
theorem perfection.coeff_pow_p {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n : ) :
(perfection.coeff R p (n + 1)) (f ^ p) = (perfection.coeff R p n) f
theorem perfection.coeff_pow_p' {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n : ) :
(perfection.coeff R p (n + 1)) f ^ p = (perfection.coeff R p n) f
theorem perfection.coeff_frobenius {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n : ) :
theorem perfection.coeff_iterate_frobenius {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n m : ) :
theorem perfection.coeff_iterate_frobenius' {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (f : (ring.perfection R p)) (n m : ) (hmn : m n) :
theorem perfection.coeff_add_ne_zero {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] {f : (ring.perfection R p)} {n : } (hfn : (perfection.coeff R p n) f 0) (k : ) :
(perfection.coeff R p (n + k)) f 0
theorem perfection.coeff_ne_zero_of_le {R : Type u₁} [comm_semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] {f : (ring.perfection R p)} {m n : } (hfm : (perfection.coeff R p m) f 0) (hmn : m n) :
@[instance]
def perfection.ring (p : ) [hp : fact (nat.prime p)] (R : Type u₁) [comm_ring R] [char_p R p] :
Equations
@[instance]
def perfection.comm_ring (p : ) [hp : fact (nat.prime p)] (R : Type u₁) [comm_ring R] [char_p R p] :
Equations
@[simp]
theorem perfection.lift_apply_apply_coe (p : ) [hp : fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p] (f : R →+* S) (r : R) (n : ) :
(((perfection.lift p R S) f) r) n = f ((pth_root R p)^[n] r)
def perfection.lift (p : ) [hp : fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p 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.

Equations
@[simp]
theorem perfection.lift_symm_apply (p : ) [hp : fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p] (hmn : R →+* (ring.perfection S p)) :
((perfection.lift p R S).symm) hmn = (perfection.coeff S p 0).comp hmn
theorem perfection.hom_ext (p : ) [hp : fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] [perfect_ring R p] {S : Type u₂} [comm_semiring S] [char_p S p] {f g : R →+* (ring.perfection S p)} (hfg : ∀ (x : R), (perfection.coeff S p 0) (f x) = (perfection.coeff S p 0) (g x)) :
f = g
@[simp]
theorem perfection.map_apply_coe {R : Type u₁} [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] {S : Type u₂} [comm_semiring S] [char_p S p] (φ : R →+* S) (f : (ring.perfection R p)) (n : ) :
((perfection.map p φ) f) n = φ ((perfection.coeff R p n) f)
def perfection.map {R : Type u₁} [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] {S : Type u₂} [comm_semiring S] [char_p S p] (φ : R →+* S) :

A ring homomorphism R →+* S induces perfection R p →+* perfection S p

Equations
theorem perfection.coeff_map {R : Type u₁} [comm_semiring R] (p : ) [hp : fact (nat.prime p)] [char_p R p] {S : Type u₂} [comm_semiring S] [char_p S p] (φ : R →+* S) (f : (ring.perfection R p)) (n : ) :
@[nolint]
structure perfection_map (p : ) [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₂} [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* R) :
Prop

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

theorem perfection_map.mk' {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {f : P →+* R} (g : P ≃+* (ring.perfection R p)) (hfg : (perfection.lift p P R) f = g) :

Create a perfection_map from an isomorphism to the perfection.

theorem perfection_map.of (p : ) [fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] :

The canonical perfection map from the perfection of a ring.

theorem perfection_map.id (p : ) [fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] :

For a perfect ring, it itself is the perfection.

def perfection_map.equiv {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») :

A perfection map induces an isomorphism to the prefection.

Equations
theorem perfection_map.equiv_apply {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») (x : P) :
(m.equiv) x = ((perfection.lift p P R) «π») x
theorem perfection_map.comp_equiv {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») (x : P) :
(perfection.coeff R p 0) ((m.equiv) x) = «π» x
theorem perfection_map.comp_equiv' {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») :
(perfection.coeff R p 0).comp (m.equiv) = «π»
theorem perfection_map.comp_symm_equiv {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») (f : (ring.perfection R p)) :
«π» ((m.equiv.symm) f) = (perfection.coeff R p 0) f
theorem perfection_map.comp_symm_equiv' {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {π : P →+* R} (m : perfection_map p «π») :
@[simp]
theorem perfection_map.lift_apply (p : ) [fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p] (P : Type u₃) [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* S) (m : perfection_map p «π») (f : R →+* S) :
(perfection_map.lift p R S P «π» m) f = (m.equiv.symm).comp ((perfection.lift p R S) f)
def perfection_map.lift (p : ) [fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p] (P : Type u₃) [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* S) (m : perfection_map 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.

Equations
@[simp]
theorem perfection_map.lift_symm_apply (p : ) [fact (nat.prime p)] (R : Type u₁) [comm_semiring R] [char_p R p] [perfect_ring R p] (S : Type u₂) [comm_semiring S] [char_p S p] (P : Type u₃) [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* S) (m : perfection_map p «π») (f : R →+* P) :
((perfection_map.lift p R S P «π» m).symm) f = «π».comp f
theorem perfection_map.hom_ext {p : } [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] [perfect_ring R p] {S : Type u₂} [comm_semiring S] [char_p S p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] (π : P →+* S) (m : perfection_map p «π») {f g : R →+* P} (hfg : ∀ (x : R), «π» (f x) = «π» (g x)) :
f = g
@[nolint]
def perfection_map.map (p : ) [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {S : Type u₂} [comm_semiring S] [char_p S p] {Q : Type u₄} [comm_semiring Q] [char_p Q p] [perfect_ring Q p] {π : P →+* R} (m : perfection_map p «π») {σ : Q →+* S} (n : perfection_map p σ) (φ : R →+* S) :
P →+* Q

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

Equations
theorem perfection_map.comp_map (p : ) [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {S : Type u₂} [comm_semiring S] [char_p S p] {Q : Type u₄} [comm_semiring Q] [char_p Q p] [perfect_ring Q p] {π : P →+* R} (m : perfection_map p «π») {σ : Q →+* S} (n : perfection_map p σ) (φ : R →+* S) :
σ.comp (perfection_map.map p m n φ) = φ.comp «π»
theorem perfection_map.map_map (p : ) [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {P : Type u₃} [comm_semiring P] [char_p P p] [perfect_ring P p] {S : Type u₂} [comm_semiring S] [char_p S p] {Q : Type u₄} [comm_semiring Q] [char_p Q p] [perfect_ring Q p] {π : P →+* R} (m : perfection_map p «π») {σ : Q →+* S} (n : perfection_map p σ) (φ : R →+* S) (x : P) :
σ ((perfection_map.map p m n φ) x) = φ («π» x)
theorem perfection_map.map_eq_map (p : ) [fact (nat.prime p)] {R : Type u₁} [comm_semiring R] [char_p R p] {S : Type u₂} [comm_semiring S] [char_p S p] (φ : R →+* S) :
@[nolint]
def mod_p (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) :
Type u₂

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

Equations
@[instance]
def mod_p.comm_ring (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) :
comm_ring (mod_p K v O hv p)
Equations
@[instance]
def mod_p.char_p (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
char_p (mod_p K v O hv p) p
@[instance]
def mod_p.nontrivial (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
nontrivial (mod_p K v O hv p)
def mod_p.pre_val (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) (x : mod_p K v O hv p) :

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).

Equations
theorem mod_p.pre_val_mk {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } {x : O} (hx : (ideal.quotient.mk (ideal.span {p})) x 0) :
theorem mod_p.pre_val_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } :
mod_p.pre_val K v O hv p 0 = 0
theorem mod_p.pre_val_mul {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } {x y : mod_p K v O hv p} (hxy0 : x * y 0) :
mod_p.pre_val K v O hv p (x * y) = (mod_p.pre_val K v O hv p x) * mod_p.pre_val K v O hv p y
theorem mod_p.pre_val_add {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } (x y : mod_p K v O hv p) :
mod_p.pre_val K v O hv p (x + y) max (mod_p.pre_val K v O hv p x) (mod_p.pre_val K v O hv p y)
theorem mod_p.v_p_lt_pre_val {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } {x : mod_p K v O hv p} :
v p < mod_p.pre_val K v O hv p x x 0
theorem mod_p.pre_val_eq_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } {x : mod_p K v O hv p} :
mod_p.pre_val K v O hv p x = 0 x = 0
theorem mod_p.v_p_lt_val {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] (hv : v.integers O) {p : } {x : O} :
theorem mod_p.mul_ne_zero_of_pow_p_ne_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] {x y : mod_p K v O hv p} (hx : x ^ p 0) (hy : y ^ p 0) :
x * y 0
@[nolint]
def pre_tilt (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
subsemiring (mod_p K v O hv p)

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

Equations
@[instance]
def pre_tilt.comm_ring (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
comm_ring (pre_tilt K v O hv p)
Equations
def pre_tilt.val_aux (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] (f : (pre_tilt K v O hv p)) :

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

Equations
theorem pre_tilt.coeff_nat_find_add_ne_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] {f : (pre_tilt K v O hv p)} {h : ∃ (n : ), (perfection.coeff (mod_p K v O hv p) p n) f 0} (k : ) :
(perfection.coeff (mod_p K v O hv p) p (nat.find h + k)) f 0
theorem pre_tilt.val_aux_eq {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] {f : (pre_tilt K v O hv p)} {n : } (hfn : (perfection.coeff (mod_p K v O hv p) p n) f 0) :
pre_tilt.val_aux K v O hv p f = mod_p.pre_val K v O hv p ((perfection.coeff (mod_p K v O hv p) p n) f) ^ p ^ n
theorem pre_tilt.val_aux_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
pre_tilt.val_aux K v O hv p 0 = 0
theorem pre_tilt.val_aux_one {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
pre_tilt.val_aux K v O hv p 1 = 1
theorem pre_tilt.val_aux_mul {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] (f g : (pre_tilt K v O hv p)) :
pre_tilt.val_aux K v O hv p (f * g) = (pre_tilt.val_aux K v O hv p f) * pre_tilt.val_aux K v O hv p g
theorem pre_tilt.val_aux_add {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] (f g : (pre_tilt K v O hv p)) :
pre_tilt.val_aux K v O hv p (f + g) max (pre_tilt.val_aux K v O hv p f) (pre_tilt.val_aux K v O hv p g)
def pre_tilt.val (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :

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

Equations
theorem pre_tilt.map_eq_zero {K : Type u₁} [field K] {v : valuation K ℝ≥0} {O : Type u₂} [comm_ring O] [algebra O K] {hv : v.integers O} {p : } [hp : fact (nat.prime p)] [hvp : fact (v p 1)] {f : (pre_tilt K v O hv p)} :
(pre_tilt.val K v O hv p) f = 0 f = 0
@[nolint]
def tilt (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : 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 [Sch11]. 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).

Equations
@[instance]
def tilt.field (K : Type u₁) [field K] (v : valuation K ℝ≥0) (O : Type u₂) [comm_ring O] [algebra O K] (hv : v.integers O) (p : ) [hp : fact (nat.prime p)] [hvp : fact (v p 1)] :
field (tilt K v O hv p)
Equations