English
Let A and B be field extensions of F embedded in a common ambient extension. If for every field K containing F and every pair of F-algebra embeddings A → K and B → K the images of A and B in K are linearly disjoint over F, then the tensor product A ⊗F B is a field.
Русский
Пусть A и B — поле расширения F, встроенные в общую «окружение». Если для всякого поля K над F и для всяких вложений A → K и B → K образы A и B в K линейно независимы друг от друга над F, то A ⊗F B является полем.
LaTeX
$$$\\Big( \\forall K \\ [\\text{Field }K] \\ [\\text{Algebra }F K], \\forall fa:A \\to_{F} K, fb:B \\to_{F} K, fa.fieldRange \\ LinearDisjoint fb.fieldRange \\Big) \\Rightarrow IsField(A \\otimes_{F} B)$$$
Lean4
/-- If for any field extension `K` of `F` that `A` and `B` embed into, their images are
linearly disjoint, then `A ⊗[F] B` is a field. (In the proof we choose `K` to be the quotient
of `A ⊗[F] B` by a maximal ideal.) -/
theorem isField_of_forall (A : Type v) [Field A] (B : Type w) [Field B] [Algebra F A] [Algebra F B]
(H :
∀ (K : Type (max v w)) [Field K] [Algebra F K],
∀ (fa : A →ₐ[F] K) (fb : B →ₐ[F] K), fa.fieldRange.LinearDisjoint fb.fieldRange) :
IsField (A ⊗[F] B) := by
obtain ⟨M, hM⟩ := Ideal.exists_maximal (A ⊗[F] B)
apply not_imp_not.1 (Ring.ne_bot_of_isMaximal_of_not_isField hM)
let K : Type (max v w) := A ⊗[F] B ⧸ M
letI : Field K := Ideal.Quotient.field _
let i := IsScalarTower.toAlgHom F (A ⊗[F] B) K
let fa := i.comp (Algebra.TensorProduct.includeLeft : A →ₐ[F] _)
let fb := i.comp (Algebra.TensorProduct.includeRight : B →ₐ[F] _)
replace H := H K fa fb
simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra, Subalgebra.linearDisjoint_iff_injective] at H
have hi :
i =
(fa.range.mulMap fb.range).comp
(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa fa.injective) (AlgEquiv.ofInjective fb fb.injective)) :=
by ext <;> simp [fa, fb]
replace H : Function.Injective i := by
simpa only [hi, AlgHom.coe_comp, AlgHom.coe_coe, EquivLike.injective_comp, fa, this, K, fb]
change Function.Injective (Ideal.Quotient.mk M) at H
rwa [RingHom.injective_iff_ker_eq_bot, Ideal.mk_ker] at H
