English
The quotient tensor-quotient equivalence maps the tensor of quotient representatives to the quotient of the tensor: quotientTensorQuotientEquiv m n (Submodule.Quotient.mk x ⊗ Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ y).
Русский
Эквивалентность quotientTensorQuotientEquiv отправляет тензор частичных представителей в частицу тензора: Quot.mk x ⊗ Quot.mk y ↦ Quot.mk (x ⊗ y).
LaTeX
$$$\\text{quotientTensorQuotientEquiv}(m,n)(\\mathrm{Submodule.Quotient.mk}\\,x \\otimes_R \\mathrm{Submodule.Quotient.mk}\\,y) = \\mathrm{Submodule.Quotient.mk}(x \\otimes_R y)$$$
Lean4
/-- If `M` is a submodule in an algebra `S` over `R`,
there is the natural isomorphism of `R`-modules between
`M ⊗[R] i(R)` and `M` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `TensorProduct.rid` as `i(R)` is not necessarily isomorphic to `R`. -/
def rTensorOne : M ⊗[R] (⊥ : Subalgebra R S) ≃ₗ[R] M :=
LinearEquiv.ofLinear M.rTensorOne'
((TensorProduct.comm R _ _).toLinearMap ∘ₗ TensorProduct.mk R (⊥ : Subalgebra R S) M 1) (by ext; simp) <|
TensorProduct.ext' fun n r ↦ by
change rTensorOne' M _ ⊗ₜ[R] 1 = n ⊗ₜ[R] r
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
replace h : algebraMap R _ x = r := Subtype.val_injective h
rw [← h, rTensorOne'_tmul, TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
