English
If A ⊗_R B is a field, then for any injective A- and B-algebras into S, their images are linearly disjoint.
Русский
Если A ⊗_R B является полем, то для любых инъективных A- и B-алгебр в S их образы линейно раздельны.
LaTeX
$$$\\text{IsField}(A\\otimes_R B) \\Rightarrow fa.range \\perp_L fb.range$ for injective fa, fb$$
Lean4
/-- If `A ⊗[R] B` is a field, then for any `R`-algebra `S`
and injections of `A` and `B` into `S`, their images are linearly disjoint. -/
theorem of_isField' {A : Type v} [Ring A] {B : Type w} [Ring B] [Algebra R A] [Algebra R B] (H : IsField (A ⊗[R] B))
(fa : A →ₐ[R] S) (fb : B →ₐ[R] S) (hfa : Function.Injective fa) (hfb : Function.Injective fb) :
fa.range.LinearDisjoint fb.range := by
apply of_isField
exact
Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa) (AlgEquiv.ofInjective fb hfb) |>.symm.toMulEquiv.isField H
