quotSMulTopTensorEquivQuotSMulTop

English

Tensoring on the right and applying QuotSMulTop r commute as a linear equivalence.

Русский

Правое тензорование и применение QuotSMulTop r коммутируют как линейное эквивалентное преобразование.

LaTeX

$$$$ QuotSMulTop r M' \otimes_R M \cong_R QuotSMulTop r (M' \otimes_R M) $$$$

Lean4

/-- Tensoring on the right and applying `QuotSMulTop · r` commute. -/
noncomputable def quotSMulTopTensorEquivQuotSMulTop : QuotSMulTop r M' ⊗[R] M ≃ₗ[R] QuotSMulTop r (M' ⊗[R] M) :=
  (equivQuotTensor r M').rTensor M ≪≫ₗ TensorProduct.assoc R (R ⧸ Ideal.span { r }) M' M ≪≫ₗ
    (equivQuotTensor r (M' ⊗[R] M)).symm

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