equivTensorQuot — Mathlib

English

Reducing modulo r on the right is the same as right-tensoring with R/(r).

Русский

Правое редуцирование по r то же самое, что правое тензорирование с R/(r).

LaTeX

$$$$ M \otimes_R (R / (r)) \cong_R \QuotSMulTop(r,M) $$$$

Lean4

/-- Reducing a module modulo `r` is the same as right tensoring with `R/(r)`. -/
noncomputable def equivTensorQuot : QuotSMulTop r M ≃ₗ[R] M ⊗[R] (R ⧸ Ideal.span { r }) :=
  quotEquivOfEq _ _ (ideal_span_singleton_smul _ _).symm ≪≫ₗ (tensorQuotEquivQuotSMul M _).symm

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