map_exact — Mathlib

English

Let S be an R-algebra; an isomorphism exists between S ⊗ (M/rM) and (S ⊗ M)/r(S ⊗ M).

Русский

Для алгебры S над R существует изоморфизм между S ⊗ (M/rM) и (S ⊗ M)/r(S ⊗ M).

LaTeX

$$$$ QuotSMulTop((\text{algebraMap } R S)\, r) (S \otimes_R M) \cong_S S \otimes_R QuotSMulTop(r,M) $$$$

Lean4

theorem map_exact {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''} (hfg : Exact f g) (hg : Surjective g) :
    Exact (map r f) (map r g) :=
  (Exact.iff_of_ladder_linearEquiv (equivQuotTensor_naturality r f).symm (equivQuotTensor_naturality r g).symm).mp
    (lTensor_exact (R ⧸ Ideal.span { r }) hfg hg)

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