English
There is a natural isomorphism between (⊥ : Subalgebra R S) ⊗_R N and N, induced by multiplication in S; this is the canonical left tensor unit.
Русский
Существует естественное изоморфизм между (⊥ : Subalgebra R S) ⊗_R N и N, порождённый умножением в S; это каноническая левая тензорная единица.
LaTeX
$$$(\\bot : \\text{Subalgebra } R S) \\otimes_R N \\cong_\\mathcal{L}[R] N$$$
Lean4
/-- If `N` is a submodule in an algebra `S` over `R`,
there is the natural isomorphism of `R`-modules between
`i(R) ⊗[R] N` and `N` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `TensorProduct.lid` as `i(R)` is not necessarily isomorphic to `R`. -/
def lTensorOne : (⊥ : Subalgebra R S) ⊗[R] N ≃ₗ[R] N :=
LinearEquiv.ofLinear N.lTensorOne' (TensorProduct.mk R (⊥ : Subalgebra R S) N 1) (by ext; simp) <|
TensorProduct.ext' fun r n ↦ by
change 1 ⊗ₜ[R] lTensorOne' N _ = r ⊗ₜ[R] n
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2
replace h : algebraMap R _ x = r := Subtype.val_injective h
rw [← h, lTensorOne'_tmul, ← TensorProduct.smul_tmul, Algebra.smul_def, mul_one]
