English
If A ⊔ B = S in a commutative algebra over R, there is a natural isomorphism of A-algebras A ⊗_R B ≅_A S induced by multiplication in S.
Русский
Пусть сумма подалгебр A ⊔ B равна S. Тогда существует естественный A-алгебраизоморфизм A ⊗_R B ≅_A S, индуцированный умножением в S.
LaTeX
$$$A \\oplus B = S \\Rightarrow A \\otimes_R B \\cong_A S$$$
Lean4
/-- If `A` and `B` are linearly disjoint subalgebras in a commutative algebra `S` over `R`
such that `A ⊔ B = S`, then this is the natural isomorphism
`A ⊗[R] B ≃ₐ[A] S` induced by multiplication in `S`.
-/
noncomputable def mulMapLeftOfSupEqTop (H' : A ⊔ B = ⊤) : A ⊗[R] B ≃ₐ[A] S :=
(AlgEquiv.ofInjective (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId A S) B.val) H.injective).trans
((Subalgebra.equivOfEq _ _
(by
apply Subalgebra.restrictScalars_injective R
rw [restrictScalars_top, ← H']
exact mulMap_range A B)).trans
Subalgebra.topEquiv)
