English
If A,B are flat R-algebras and A ⊗_R B is a domain, then there exists a field K into which A and B embed with linearly disjoint images.
Русский
Если A,B плоские над R и A ⊗_R B — область, существует поле K и вложения A,B в K с линейно раздельными образами.
LaTeX
$$$\\exists K \\; \\exists fa: A \\to_R K \\; \\exists fb: B \\to_R K \\; fa(A) \\perp_L fb(B)$$$
Lean4
/-- If `A` and `B` are flat algebras over `R`, such that `A ⊗[R] B` is a domain, and such that
the algebra maps are injective, then there exists an `R`-algebra `K` that is a field that `A`
and `B` inject into with linearly disjoint images. Note: `K` can chosen to be the
fraction field of `A ⊗[R] B`, but here we hide this fact. -/
theorem exists_field_of_isDomain_of_injective (A : Type v) [CommRing A] (B : Type w) [CommRing B] [Algebra R A]
[Algebra R B] [Module.Flat R A] [Module.Flat R B] [IsDomain (A ⊗[R] B)] (ha : Function.Injective (algebraMap R A))
(hb : Function.Injective (algebraMap R B)) :
∃ (K : Type (max v w)) (_ : Field K) (_ : Algebra R K) (fa : A →ₐ[R] K) (fb : B →ₐ[R] K),
Function.Injective fa ∧ Function.Injective fb ∧ fa.range.LinearDisjoint fb.range :=
let K := FractionRing (A ⊗[R] B)
let i := IsScalarTower.toAlgHom R (A ⊗[R] B) K
have hi : Function.Injective i := IsFractionRing.injective (A ⊗[R] B) K
⟨K, inferInstance, inferInstance, i.comp Algebra.TensorProduct.includeLeft, i.comp Algebra.TensorProduct.includeRight,
hi.comp (Algebra.TensorProduct.includeLeft_injective hb), hi.comp (Algebra.TensorProduct.includeRight_injective ha),
by simpa only [AlgHom.range_comp] using (include_range R A B).map i hi⟩
