English
There exists a way to realize A and B inside some field extension so that their tensor product is a domain, hence linear disjointness on the image ranges.
Русский
Существует способ поместить A и B в некоторое расширение поля так, чтобы их тензорное произведение было областью, следовательно, линейная независимость на образах.
LaTeX
$$$\exists fa fb, \; fa.fieldRange.LinearDisjoint fb.fieldRange$$$
Lean4
/-- If `A` and `B` are field extensions of `F`, there exists a field extension `E` of `F` that
`A` and `B` embed into with linearly disjoint images, then `A ⊗[F] B` is a domain. -/
theorem isDomain' {A B : Type*} [Field A] [Algebra F A] [Field B] [Algebra F B] {fa : A →ₐ[F] E} {fb : B →ₐ[F] E}
(H : fa.fieldRange.LinearDisjoint fb.fieldRange) : IsDomain (A ⊗[F] B) :=
by
simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra] at H
exact H.isDomain_of_injective fa.injective fb.injective
