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

noncomputable 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 = Perfection.teichmuller p (Ideal.span {↑p})

@[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