Ring Perfection and Tilt #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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 }.
def
ring.perfection_subsemiring
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
subsemiring (ℕ → R)
The perfection of a ring R with characteristic p, as a subsemiring,
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
- ring.perfection_subsemiring R p = {carrier := (monoid.perfection R p).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _}
def
ring.perfection_subring
(R : Type u₁)
[comm_ring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
The perfection of a ring R with characteristic p, as a subring,
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
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}.
@[protected, instance]
def
perfection.ring.perfection.comm_semiring
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
comm_semiring (ring.perfection R p)
Equations
@[protected, instance]
def
perfection.char_p
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
char_p (ring.perfection R p) p
@[protected, instance]
def
perfection.ring
(p : ℕ)
[hp : fact (nat.prime p)]
(R : Type u₁)
[comm_ring R]
[char_p R p] :
ring (ring.perfection R p)
Equations
- perfection.ring p R = (ring.perfection_subring R p).to_ring
@[protected, instance]
def
perfection.comm_ring
(p : ℕ)
[hp : fact (nat.prime p)]
(R : Type u₁)
[comm_ring R]
[char_p R p] :
comm_ring (ring.perfection R p)
Equations
@[protected, instance]
def
perfection.ring.perfection.inhabited
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
inhabited (ring.perfection R p)
Equations
- perfection.ring.perfection.inhabited R p = {default := 0}
def
perfection.coeff
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p]
(n : ℕ) :
ring.perfection R p →+* R
The n-th coefficient of an element of the perfection.
Equations
- perfection.coeff R p n = {to_fun := λ (f : ring.perfection R p), f.val n, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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] :
ring.perfection R p →+* ring.perfection R p
The p-th root of an element of the perfection.
Equations
- perfection.pth_root R p = {to_fun := λ (f : ring.perfection R p), ⟨λ (n : ℕ), ⇑(perfection.coeff R p (n + 1)) f, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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 : ℕ) :
⇑(perfection.coeff R p n) (⇑(perfection.pth_root R p) f) = ⇑(perfection.coeff R p (n + 1)) 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_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 : ℕ) :
⇑(perfection.coeff R p (n + 1)) (⇑(frobenius (ring.perfection R p) p) f) = ⇑(perfection.coeff R p n) f
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 : ℕ) :
⇑(perfection.coeff R p (n + m)) (⇑(frobenius (ring.perfection R p) p)^[m] f) = ⇑(perfection.coeff R p n) f
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) :
⇑(perfection.coeff R p n) (⇑(frobenius (ring.perfection R p) p)^[m] f) = ⇑(perfection.coeff R p (n - m)) f
theorem
perfection.pth_root_frobenius
{R : Type u₁}
[comm_semiring R]
{p : ℕ}
[hp : fact (nat.prime p)]
[char_p R p] :
(perfection.pth_root R p).comp (frobenius (ring.perfection R p) p) = ring_hom.id (ring.perfection R p)
theorem
perfection.frobenius_pth_root
{R : Type u₁}
[comm_semiring R]
{p : ℕ}
[hp : fact (nat.prime p)]
[char_p R p] :
(frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p)
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) :
⇑(perfection.coeff R p n) f ≠ 0
@[protected, instance]
def
perfection.perfect_ring
(R : Type u₁)
[comm_semiring R]
(p : ℕ)
[hp : fact (nat.prime p)]
[char_p R p] :
perfect_ring (ring.perfection R p) p
Equations
- perfection.perfect_ring R p = {pth_root' := ⇑(perfection.pth_root R p), frobenius_pth_root' := _, pth_root_frobenius' := _}
@[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 : ℕ) :
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] :
(R →+* S) ≃ (R →+* ring.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_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]
(f : R →+* ring.perfection S p) :
⇑((perfection.lift p R S).symm) f = (perfection.coeff S p 0).comp f
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) :
ring.perfection R p →+* ring.perfection S p
A ring homomorphism R →+* S induces perfection R p →+* perfection S p
Equations
- perfection.map p φ = {to_fun := λ (f : ring.perfection R p), ⟨λ (n : ℕ), ⇑φ (⇑(perfection.coeff R p n) f), _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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 : ℕ) :
⇑(perfection.coeff S p n) (⇑(perfection.map p φ) f) = ⇑φ (⇑(perfection.coeff R p n) f)
@[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
- injective : ∀ ⦃x y : P⦄, (∀ (n : ℕ), ⇑π (⇑(pth_root P p)^[n] x) = ⇑π (⇑(pth_root P p)^[n] y)) → x = y
- surjective : ∀ (f : ℕ → R), (∀ (n : ℕ), f (n + 1) ^ p = f n) → (∃ (x : P), ∀ (n : ℕ), ⇑π (⇑(pth_root P p)^[n] x) = f n)
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) :
perfection_map p f
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] :
perfection_map p (perfection.coeff R p 0)
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] :
perfection_map p (ring_hom.id R)
For a perfect ring, it itself is the perfection.
noncomputable
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 π) :
P ≃+* ring.perfection R p
A perfection map induces an isomorphism to the prefection.
Equations
- m.equiv = ring_equiv.of_bijective (⇑(perfection.lift p P R) π) _
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) :
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) :
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) :
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)
noncomputable
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 π) :
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
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]
noncomputable
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
- perfection_map.map p m n φ = ⇑(perfection_map.lift p P S Q σ n) (φ.comp π)
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) :
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) :
perfection_map.map p _ _ φ = perfection.map p φ
@[protected, instance]
def
mod_p.comm_ring
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(O : Type u₂)
[comm_ring O]
[algebra O K]
(hv : v.integers O)
(p : ℕ) :
Equations
- mod_p.comm_ring K v O hv p = ideal.quotient.comm_ring (ideal.span {↑p})
noncomputable
def
mod_p.pre_val
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(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
- mod_p.pre_val K v O hv p x = ite (x = 0) 0 (⇑v (⇑(algebra_map O K) (quotient.out' x)))
theorem
mod_p.pre_val_mk
{K : Type u₁}
[field K]
{v : valuation K nnreal}
{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) :
mod_p.pre_val K v O hv p (⇑(ideal.quotient.mk (ideal.span {↑p})) x) = ⇑v (⇑(algebra_map O K) x)
theorem
mod_p.pre_val_mul
{K : Type u₁}
[field K]
{v : valuation K nnreal}
{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 nnreal}
{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) ≤ linear_order.max (mod_p.pre_val K v O hv p x) (mod_p.pre_val K v O hv p y)
@[nolint]
def
pre_tilt
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(O : Type u₂)
[comm_ring O]
[algebra O K]
(hv : v.integers O)
(p : ℕ) :
Type u₂
Perfection of O/(p) where O is the ring of integers of K.
Equations
- pre_tilt K v O hv p = ring.perfection (mod_p K v O hv p) p
Instances for pre_tilt
@[protected, instance]
def
pre_tilt.comm_ring
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(O : Type u₂)
[comm_ring O]
[algebra O K]
(hv : v.integers O)
(p : ℕ)
[hp : fact (nat.prime p)]
[hvp : fact (⇑v ↑p ≠ 1)] :
Equations
- pre_tilt.comm_ring K v O hv p = perfection.comm_ring p (mod_p K v O hv p)
noncomputable
def
pre_tilt.val_aux
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(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
- pre_tilt.val_aux K v O hv p f = dite (∃ (n : ℕ), ⇑(perfection.coeff (mod_p K v O hv p) p n) f ≠ 0) (λ (h : ∃ (n : ℕ), ⇑(perfection.coeff (mod_p K v O hv p) p n) f ≠ 0), mod_p.pre_val K v O hv p (⇑(perfection.coeff (mod_p K v O hv p) p (nat.find h)) f) ^ p ^ nat.find h) (λ (h : ¬∃ (n : ℕ), ⇑(perfection.coeff (mod_p K v O hv p) p n) f ≠ 0), 0)
theorem
pre_tilt.coeff_nat_find_add_ne_zero
{K : Type u₁}
[field K]
{v : valuation K nnreal}
{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 : ℕ) :
theorem
pre_tilt.val_aux_eq
{K : Type u₁}
[field K]
{v : valuation K nnreal}
{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_mul
{K : Type u₁}
[field K]
{v : valuation K nnreal}
{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 nnreal}
{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) ≤ linear_order.max (pre_tilt.val_aux K v O hv p f) (pre_tilt.val_aux K v O hv p g)
noncomputable
def
pre_tilt.val
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(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
- pre_tilt.val K v O hv p = {to_monoid_with_zero_hom := {to_fun := pre_tilt.val_aux K v O hv p hvp, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}
@[nolint]
def
tilt
(K : Type u₁)
[field K]
(v : valuation K nnreal)
(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
- tilt K v O hv p = fraction_ring (pre_tilt K v O hv p)