untilt — Mathlib

English

The mod p image of untilt coincides with the zeroth coefficient of the perfection expansion: Quotient.mk(span{p})(x.untilt) = coeff(ModP(O,p), p, 0, x).

Русский

Образ modulo p от untilt равен нулевому коэффициенту в разложении совершенствования: Quotient.mk(span{p})(x.untilt) = coeff(ModP(O,p), p, 0, x).

LaTeX

$$$\mathrm{Ideal.Quotient}.mk(\mathrm{Ideal.span}\{\{p:O\}\}, x.\untilt) = coeff( ModP(O,p) , p , 0 , x)$$$

Lean4

/-- 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`.
-/
def untilt : PreTilt O p →* O where
  toFun := untiltFun
  map_one' := by
    rw [← sub_eq_zero, IsHausdorff.eq_iff_smodEq (I := (span {(p : O)}))]
    intro n
    rw [sub_smodEq_zero]
    simp only [smul_eq_mul, mul_top]
    apply (untiltAux_smodEq_untiltFun (1 : PreTilt O p) n).symm.trans
    simp only [span_singleton_pow, SModEq.sub_mem, mem_span_singleton]
    exact pow_dvd_one_untiltAux_sub_one (O := O) (p := p) n
  map_mul' _
    _ := by
    rw [← sub_eq_zero, IsHausdorff.eq_iff_smodEq (I := (span {(p : O)}))]
    intro n
    rw [sub_smodEq_zero]
    simp only [smul_eq_mul, mul_top]
    apply (untiltAux_smodEq_untiltFun _ n).symm.trans
    refine SModEq.trans ?_ (SModEq.mul (untiltAux_smodEq_untiltFun _ n) (untiltAux_smodEq_untiltFun _ n))
    simp only [span_singleton_pow, SModEq.sub_mem, mem_span_singleton]
    exact pow_dvd_mul_untiltAux_sub_untiltAux_mul (O := O) (p := p) _ _ n

Похожие утверждения