English
For an ideal I, the quotient-tensor-quotient-smul map sends (ȑ) ⊗ x to the class of r·x modulo I·⊤ in M.
Русский
Для идеала I отображение квоты-умножения отправляет (ȑ) ⊗ x в класс r·x по отношению к I·⊤.
LaTeX
$$$$ \text{quotTensorEquivQuotSMul}_M I\big( \overline{r} \otimes x \big) = \overline{r \cdot x}. $$$$
Lean4
/-- Left tensoring a module with a quotient of the ring is the same as
quotienting that module by the corresponding submodule. -/
noncomputable def quotTensorEquivQuotSMul (I : Ideal R) : ((R ⧸ I) ⊗[R] M) ≃ₗ[R] M ⧸ (I • (⊤ : Submodule R M)) :=
quotientTensorEquiv M I ≪≫ₗ
(Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <|
by
rw [← Submodule.map_coe_toLinearMap, ← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp,
Submodule.smul_eq_map₂, map₂_eq_range_lift_comp_mapIncl]
exact congr_arg _ (TensorProduct.ext' fun _ _ ↦ rfl))
