mulMap' — Mathlib

English

The surjective R-algebra homomorphism mulMap' from A ⊗ B to A ⊔ B is surjective; equivalently, its range equals A ⊔ B.

Русский

Гомоморфизм mulMap' из A ⊗ B на A ⊔ B над R сюръективен; другие слова: образ равен A ⊔ B.

LaTeX

$$$\operatorname{range}(mulMap' A B) = A \sqcup B$$$

Lean4

/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`,
there is the natural `R`-algebra homomorphism
`A ⊗[R] B →ₐ[R] A ⊔ B` induced by multiplication in `S`,
which is surjective (`Subalgebra.mulMap'_surjective`). -/
def mulMap' : A ⊗[R] B →ₐ[R] ↥(A ⊔ B) :=
  (equivOfEq _ _ (mulMap_range A B)).toAlgHom.comp (mulMap A B).rangeRestrict

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