tensorQuotEquivQuotSMul — Mathlib

English

The composition of quotient-tensor-smul with the canonical quotient map equals the canonical quotient map composed with the inclusion map.

Русский

Композиция отображения квоты-умножения через тензор с каноническим отображением квоты совпадает с каноническим отображением квоты через вложение.

LaTeX

$$$$(\text{quotTensorEquivQuotSMul} \; M \; I) \circ (I \cdot \top).mkQ = \text{mkQ} \circ (\text{lid } R M). $$$$

Lean4

/-- Right tensoring a module with a quotient of the ring is the same as
quotienting that module by the corresponding submodule. -/
noncomputable def tensorQuotEquivQuotSMul (I : Ideal R) : (M ⊗[R] (R ⧸ I)) ≃ₗ[R] M ⧸ (I • (⊤ : Submodule R M)) :=
  TensorProduct.comm _ _ _ ≪≫ₗ quotTensorEquivQuotSMul M I

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