quotCotangent — Mathlib

English

The two-step quotient construction yields a ring isomorphism (R/I^2)/I.cotangentIdeal ≃+* R/I.

Русский

Две последовательных факторизации дают изоморфизм кол-во R/I^2 по I.cotangentIdeal с R/I.

LaTeX

$$(R / I^2) / I.cotangentIdeal \cong+* R / I$$

Lean4

/-- The quotient ring of `I ⧸ I ^ 2` is `R ⧸ I`. -/
def quotCotangent : (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I :=
  by
  refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_
  refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_
  exact Ideal.quotEquivOfEq (sup_eq_right.mpr <| Ideal.pow_le_self two_ne_zero)

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