equivQuotTensor — Mathlib

English

Reducing modulo r (i.e., quotient by rM) is equivalent to left tensoring with R/(r).

Русский

Редукция по модулю r эквивалентна левому тензорованию с R/(r).

LaTeX

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

Lean4

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

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