Commit 2025-02-20 10:22 4682defd

View on Github →

feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) In this PR,

  1. we generalize the definition of the pretilt and
  2. define the untilt function from the pretilt of a p-adically complete ring to the ring itself. The results about pretilt and tilt are kept unchanged as much as possible. They will be generalized in future PRs.

Estimated changes

added theorem sub_smodEq_zero
added theorem Ideal.Quotient.mk_out
modified theorem ModP.preVal_add
modified theorem ModP.preVal_eq_zero
modified theorem ModP.preVal_mk
modified theorem ModP.preVal_mul
modified theorem ModP.preVal_zero
modified theorem ModP.v_p_lt_preVal
modified def ModP
added theorem PreTilt.isDomain
modified theorem PreTilt.map_eq_zero
modified theorem PreTilt.valAux_add
modified theorem PreTilt.valAux_eq
modified theorem PreTilt.valAux_mul
modified theorem PreTilt.valAux_one
modified theorem PreTilt.valAux_zero
modified def Tilt
added def PreTilt.untilt