English
Let fa : A → S and fb : B → S be injective algebra maps whose ranges are linearly disjoint; then A ⊗_R B is a domain.
Русский
Пусть fa: A → S и fb: B → S инъективны и их образы линейно раздельны; тогда A ⊗_R B — область.
LaTeX
$$$\\text{Injective } fa, fb, \\ fa\\range \\perp fb\\range \\Rightarrow IsDomain(A \\otimes_R B)$$$
Lean4
/-- If `A` and `B` are `R`-algebras, such that there exists a domain `S` over `R`
such that `A` and `B` inject into it and their images are linearly disjoint,
then `A ⊗[R] B` is also a domain. -/
theorem isDomain_of_injective [IsDomain S] {A B : Type*} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
{fa : A →ₐ[R] S} {fb : B →ₐ[R] S} (hfa : Function.Injective fa) (hfb : Function.Injective fb)
(H : fa.range.LinearDisjoint fb.range) : IsDomain (A ⊗[R] B) :=
have := H.isDomain
(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa) (AlgEquiv.ofInjective fb hfb)).toMulEquiv.isDomain
