Untilt Function

In this file, we define the untilt function from the pretilt of a p-adically complete ring to the ring itself. Note that this is not the untilt functor.

Main definition

• PreTilt.untilt : Given a p-adically complete ring O, this is the multiplicative map from PreTilt O p to O itself. Specifically, it is defined as the limit of p^n-th powers of arbitrary lifts in O of the n-th component from the perfection of O/p.

Main theorem

• PreTilt.mk_untilt_eq_coeff_zero : The composition of the mod p map with the untilt function equals taking the zeroth component of the perfection.

Reference

• [Berkeley Lectures on ( p )-adic Geometry][MR4446467]

Tags

Perfectoid, Tilting equivalence, Untilt

def PreTilt.untiltAux {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) (n : ℕ) : O

The auxiliary sequence to define the untilt map. The (n + 1)-th term is the p^n-th powers of arbitrary lifts in O of the n-th component from the perfection of O/p.

Equations

• x.untiltAux 0 = 1
• x.untiltAux n_2.succ = Quotient.out ((PreTilt.coeff n_2) x) ^ p ^ n_2

theorem PreTilt.pow_dvd_untiltAux_sub_untiltAux {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) {m n : ℕ} (h : m ≤ n) : ↑p ^ m ∣ x.untiltAux m - x.untiltAux n

theorem PreTilt.pow_dvd_one_untiltAux_sub_one {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (m : ℕ) : ↑p ^ m ∣ untiltAux 1 m - 1

theorem PreTilt.pow_dvd_mul_untiltAux_sub_untiltAux_mul {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x y : PreTilt O p) (m : ℕ) : ↑p ^ m ∣ (x * y).untiltAux m - x.untiltAux m * y.untiltAux m

theorem PreTilt.exists_smodEq_untiltAux {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) : ∃ (y : O), ∀ (n : ℕ), x.untiltAux n ≡ y [SMOD Ideal.span {↑p} ^ n • ⊤]

def PreTilt.untiltFun {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) : O

Given a p-adically complete ring O, this is the underlying function of the untilt map. It is defined as the limit of p^n-th powers of arbitrary lifts in O of the n-th component from the perfection of O/p.

Equations

• x.untiltFun = Classical.choose ⋯

theorem PreTilt.untiltAux_smodEq_untiltFun {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) (n : ℕ) : x.untiltAux n ≡ x.untiltFun [SMOD Ideal.span {↑p} ^ n]

def PreTilt.untilt {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] : PreTilt O p →* O

Given a p-adically complete ring O, this is the multiplicative map from PreTilt O p to O itself. Specifically, it is defined as the limit of p^n-th powers of arbitrary lifts in O of the n-th component from the perfection of O/p.

Equations

• PreTilt.untilt = { toFun := PreTilt.untiltFun, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PreTilt.mk_untilt_eq_coeff_zero {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] (x : PreTilt O p) : (Ideal.Quotient.mk (Ideal.span {↑p})) (untilt x) = (coeff 0) x

The composition of the mod p map with the untilt function equals taking the zeroth component of the perfection.

@[simp]

theorem PreTilt.mk_comp_untilt_eq_coeff_zero {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] : ⇑(Ideal.Quotient.mk (Ideal.span {↑p})) ∘ ⇑untilt = ⇑(coeff 0)

The composition of the mod p map with the untilt function equals taking the zeroth component of the perfection. A variation of PreTilt.mk_untilt_eq_coeff_zero.

@[simp]

theorem PreTilt.untilt_iterate_frobeniusEquiv_symm_pow {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] (x : PreTilt O p) (n : ℕ) : untilt ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x) ^ p ^ n = untilt x