English
The tilt of a field K, with valuation v and integers O, yields a genuine field structure on Tilt(K, v, O, hv, p).
Русский
Поворот поля K с вальюацией v и целыми O образует поле на Tilt(K, v, O, hv, p).
LaTeX
$$Tilt(K,v,O,hv,p) is a Field$$
Lean4
/-- 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)`. -/
def Tilt [Fact p.Prime] [hvp : Fact (v p ≠ 1)] :=
have _ := Fact.mk <| mt hv.one_of_isUnit <| (map_natCast (algebraMap O K) p).symm ▸ hvp.1
FractionRing (PreTilt O p)
