English
If E and K are field extensions of F, one of them is algebraic, and E ⊗F K is a domain, then E ⊗F K is a field.
Русский
Если E и K — поля, расширяющие F, одно из них алгебраическое над F, и их тензорное произведение E ⊗F K является доменом, то оно является полем.
LaTeX
$$$(\\text{Algebra.IsAlgebraic } F E \\lor \\text{Algebra.IsAlgebraic } F K) \\land IsDomain(E \\otimes_{F} K) \\Rightarrow IsField(E \\otimes_{F} K)$$$
Lean4
/-- If `E` and `K` are field extensions of `F`, one of them is algebraic, such that
`E ⊗[F] K` is a domain, then `E ⊗[F] K` is also a field. It is a corollary of
`Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective` and
`IntermediateField.sup_toSubalgebra_of_isAlgebraic`.
See `Algebra.TensorProduct.isAlgebraic_of_isField` for its converse (in an earlier file). -/
theorem _root_.Algebra.TensorProduct.isField_of_isAlgebraic (K : Type*) [Field K] [Algebra F K] [IsDomain (E ⊗[F] K)]
(halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K) : IsField (E ⊗[F] K) :=
have ⟨L, _, _, fa, fb, hfa, hfb, H⟩ :=
Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective F E K (RingHom.injective _) (RingHom.injective _)
let f : E ⊗[F] K ≃ₐ[F] ↥(fa.fieldRange ⊔ fb.fieldRange) :=
Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa) (AlgEquiv.ofInjective fb hfb) |>.trans
(Subalgebra.LinearDisjoint.mulMap H) |>.trans
(Subalgebra.equivOfEq _ _
(sup_toSubalgebra_of_isAlgebraic fa.fieldRange fb.fieldRange <| by
rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
(AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg).symm)
f.toMulEquiv.isField (Field.toIsField _)
