algEquivIncludeRange — Mathlib

English

There is an algebra isomorphism between S ⊗ T and the tensor product of the ranges of includeLeft and includeRight.

Русский

Существует алгебрный изоморфизм между S ⊗ T и тензорным произведением диапазонов includeLeft и includeRight.

LaTeX

$$$\\text{algEquivIncludeRange} : S ⊗_R T ≃ₐ[R] (includeLeft.range) ⊗_R (includeRight.range)$$$

Lean4

/-- Given `R`-algebras `S,T`, there is a natural `R`-algebra isomorphism from `S ⊗[R] T` to
`S' ⊗[R] T'` where `S',T'` are the images of `S,T` in `S ⊗[R] T` respectively. -/
def algEquivIncludeRange :
    S ⊗[R] T ≃ₐ[R] (includeLeft : S →ₐ[R] S ⊗[R] T).range ⊗[R] (includeRight : T →ₐ[R] S ⊗[R] T).range :=
  algEquivOfLinearEquivTensorProduct (linearEquivIncludeRange R S T) (by simp) rfl

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