English
There is a natural linear isomorphism between S ⊗ T and ranges of includeLeft and includeRight.
Русский
Существует естественный линейный изоморфизм между S ⊗ T и произведениями includeLeft.range и includeRight.range.
LaTeX
$$$S \\otimes_R T \\cong_R (\\mathrm{includeLeft}.range) \\otimes_R (\\mathrm{includeRight}.range)$$$
Lean4
/-- Given `R`-algebras `S,T`, there is a natural `R`-linear isomorphism from `S ⊗[R] T` to
`S' ⊗[R] T'` where `S',T'` are the images of `S,T` in `S ⊗[R] T` respectively.
This is promoted to an `R`-algebra isomorphism `Algebra.TensorProduct.algEquivIncludeRange`. -/
def linearEquivIncludeRange :
S ⊗[R] T ≃ₗ[R] (includeLeft : S →ₐ[R] S ⊗[R] T).range ⊗[R] (includeRight : T →ₐ[R] S ⊗[R] T).range :=
.ofLinear (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
((LinearMap.range includeLeft).mulMap (LinearMap.range includeRight))
(_root_.TensorProduct.ext' <|
by
rintro ⟨x', x, rfl : x ⊗ₜ 1 = x'⟩ ⟨y', y, rfl : 1 ⊗ₜ y = y'⟩
rw [LinearMap.comp_apply, LinearMap.id_apply]
erw [Submodule.mulMap_tmul]
rw [tmul_mul_tmul, mul_one, one_mul, _root_.TensorProduct.map_tmul]
rfl)
(_root_.TensorProduct.ext' fun x y ↦
by
rw [LinearMap.comp_apply, LinearMap.id_apply, _root_.TensorProduct.map_tmul]
erw [Submodule.mulMap_tmul]
change (x ⊗ₜ 1) * (1 ⊗ₜ y) = _
rw [tmul_mul_tmul, mul_one, one_mul])
