English
If A and B are linearly disjoint subalgebras in a commutative R-algebra S, there is a natural isomorphism between A ⊗_R B and A ⊔ B induced by multiplication in S.
Русский
Если A и B — линейно раздельные подалгебры в коммутативной R-алгебре S, существует естественный изоморфизм между A ⊗_R B и A ⊔ B, индуцируемый умножением в S.
LaTeX
$$$A \\text{ LinearDisjoint } B \\Rightarrow (A \\otimes_R B) \\cong_R (A \\lor B)$, где конус идёт по умножению в S$$
Lean4
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint, then there is the natural isomorphism
`A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. -/
protected def mulMap :=
(AlgEquiv.ofInjective (A.mulMap B) H.injective).trans (equivOfEq _ _ (mulMap_range A B))
