mk_untilt_eq_coeff_zero — Mathlib

English

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

Русский

Состав модуля p с untilt равен нулевому коэффициенту совершенствования.

LaTeX

$$Ideal.Quotient.mk(span{p}) ∘ untilt = coeff(ModP(O,p), p, 0)$$

Lean4

/-- The composition of the mod `p` map
with the untilt function equals taking the zeroth component of the perfection.
-/
theorem mk_untilt_eq_coeff_zero (x : PreTilt O p) :
    Ideal.Quotient.mk (Ideal.span {(p : O)}) (x.untilt) = coeff (ModP O p) p 0 x :=
  by
  simp only [untilt]
  rw [← Ideal.Quotient.mk_out ((coeff (ModP O p) p 0) x), Ideal.Quotient.eq, ← SModEq.sub_mem]
  simpa [untiltAux] using (x.untiltAux_smodEq_untiltFun 1).symm

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