quotientQuotientEquivQuotient — Mathlib

English

Let S ⊆ T be submodules of M over a ring R. Then the natural isomorphism ((M/S) / (T.map S.mkQ)) ≅ M/T holds, i.e., the quotient of M by T is canonically the same as the quotient of M/S by T/S.

Русский

Пусть S \subseteq T — подмодули M над кольцом R. Тогда естественный изоморфизм ((M/S) / (T.map S.mkQ)) ≅ M/T существует, то есть частное по T соответствует частному по S.

LaTeX

$$$$((M/S) / (T.map S.mkQ)) \\cong_R M / T$$$$

Lean4

/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`. -/
def quotientQuotientEquivQuotient : ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ T :=
  {
    quotientQuotientEquivQuotientAux S T
      h with
    toFun := quotientQuotientEquivQuotientAux S T h
    invFun := mapQ _ _ (mkQ S) (le_comap_map _ _)
    left_inv := fun x =>
      Submodule.Quotient.induction_on _ x fun x => Submodule.Quotient.induction_on _ x fun x => by simp
    right_inv := fun x => Submodule.Quotient.induction_on _ x fun x => by simp }

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