Linearly disjoint fields

This file contains basics about the linearly disjoint fields. We adapt the definitions in https://en.wikipedia.org/wiki/Linearly_disjoint. See the file Mathlib/LinearAlgebra/LinearDisjoint.lean and Mathlib/RingTheory/LinearDisjoint.lean for details.

Main definitions

• IntermediateField.LinearDisjoint: an intermediate field A of E / F and an abstract field L between E / F (as a special case, two intermediate fields) are linearly disjoint over F, if they are linearly disjoint as subalgebras (Subalgebra.LinearDisjoint).

Implementation notes

The Subalgebra.LinearDisjoint is stated for two Subalgebras. The original design of IntermediateField.LinearDisjoint is also stated for two IntermediateFields (see IntermediateField.linearDisjoint_iff' for the original statement). But it's probably useful if one of them can be generalized to an abstract field (see https://github.com/leanprover-community/mathlib4/pull/9651#discussion_r1464070324). This leads to the current design of IntermediateField.LinearDisjoint which is for one IntermediateField and one abstract field. It is not generalized to two abstract fields as this will break the dot notation.

Main results

Equivalent characterization of linear disjointness

• IntermediateField.LinearDisjoint.linearIndependent_left: if A and L are linearly disjoint, then any F-linearly independent family on A remains linearly independent over L.

• IntermediateField.LinearDisjoint.of_basis_left: conversely, if there exists an F-basis of A which remains linearly independent over L, then A and L are linearly disjoint.

• IntermediateField.LinearDisjoint.linearIndependent_right: IntermediateField.LinearDisjoint.linearIndependent_right': if A and L are linearly disjoint, then any F-linearly independent family on L remains linearly independent over A.

• IntermediateField.LinearDisjoint.of_basis_right: IntermediateField.LinearDisjoint.of_basis_right': conversely, if there exists an F-basis of L which remains linearly independent over A, then A and L are linearly disjoint.

• IntermediateField.LinearDisjoint.linearIndependent_mul: IntermediateField.LinearDisjoint.linearIndependent_mul': if A and L are linearly disjoint, then for any family of F-linearly independent elements { a_i } of A, and any family of F-linearly independent elements { b_j } of L, the family { a_i * b_j } in S is also F-linearly independent.

• IntermediateField.LinearDisjoint.of_basis_mul: IntermediateField.LinearDisjoint.of_basis_mul': conversely, if { a_i } is an F-basis of A, if { b_j } is an F-basis of L, such that the family { a_i * b_j } in E is F-linearly independent, then A and L are linearly disjoint.

Equivalent characterization by IsDomain or IsField of tensor product

The following results are related to the equivalent characterizations in https://mathoverflow.net/questions/8324.

• IntermediateField.LinearDisjoint.isDomain', IntermediateField.LinearDisjoint.exists_field_of_isDomain: if A and B are field extensions of F, then A ⊗[F] B is a domain if and only if there exists a field extension of F that A and B embed into with linearly disjoint images.

• IntermediateField.LinearDisjoint.isField_of_forall, IntermediateField.LinearDisjoint.of_isField': if A and B are field extensions of F, then A ⊗[F] B is a field if and only if for any field extension of F that A and B embed into, their images are linearly disjoint.

• Algebra.TensorProduct.isField_of_isAlgebraic: 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 also a field. See Algebra.TensorProduct.isAlgebraic_of_isField for its converse (in an earlier file).

• IntermediateField.LinearDisjoint.isField_of_isAlgebraic, IntermediateField.LinearDisjoint.isField_of_isAlgebraic': if A and B are field extensions of F, one of them is algebraic, such that they are linearly disjoint (more generally, if there exists a field extension of F that they embed into with linearly disjoint images), then A ⊗[F] B is a field.

Other main results

• IntermediateField.LinearDisjoint.symm, IntermediateField.linearDisjoint_comm: linear disjointness is symmetric.

• IntermediateField.LinearDisjoint.map: linear disjointness is preserved by algebra homomorphism.

• IntermediateField.LinearDisjoint.rank_sup, IntermediateField.LinearDisjoint.finrank_sup: if A and B are linearly disjoint, then the rank of A ⊔ B is equal to the product of the rank of A and B.

• IntermediateField.LinearDisjoint.of_finrank_sup: conversely, if A and B are finite extensions, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.

• IntermediateField.LinearDisjoint.of_finrank_coprime: if the rank of A and B are coprime, then A and B are linearly disjoint.

• IntermediateField.LinearDisjoint.inf_eq_bot: if A and B are linearly disjoint, then they are disjoint.

• IntermediateField.LinearDisjoint.algEquiv_of_isAlgebraic: linear disjointness is preserved by isomorphisms, provided that one of the field is algebraic.

Tags

linearly disjoint, linearly independent, tensor product

@[reducible, inline]

abbrev IntermediateField.LinearDisjoint {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) (L : Type w) [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] : Prop

If A is an intermediate field of E / F, and E / L / F is a field extension tower, then A and L are linearly disjoint, if they are linearly disjoint as subalgebras of E (Subalgebra.LinearDisjoint).

Equations

• A.LinearDisjoint L = A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range

theorem IntermediateField.linearDisjoint_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) (L : Type w) [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] : A.LinearDisjoint L ↔ A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range

theorem IntermediateField.linearDisjoint_iff' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} : A.LinearDisjoint ↥B ↔ A.LinearDisjoint B.toSubalgebra

Two intermediate fields are linearly disjoint if and only if they are linearly disjoint as subalgebras.

theorem IntermediateField.LinearDisjoint.symm {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) : B.LinearDisjoint ↥A

Linear disjointness is symmetric.

theorem IntermediateField.linearDisjoint_comm {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} : A.LinearDisjoint ↥B ↔ B.LinearDisjoint ↥A

Linear disjointness is symmetric.

theorem IntermediateField.LinearDisjoint.symm' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {L' : Type u_1} [Field L'] [Algebra F L'] [Algebra L' E] [IsScalarTower F L' E] (H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L') : (IsScalarTower.toAlgHom F L' E).fieldRange.LinearDisjoint L

Linear disjointness is symmetric.

theorem IntermediateField.linearDisjoint_comm' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {L' : Type u_1} [Field L'] [Algebra F L'] [Algebra L' E] [IsScalarTower F L' E] : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L' ↔ (IsScalarTower.toAlgHom F L' E).fieldRange.LinearDisjoint L

Linear disjointness is symmetric.

theorem IntermediateField.LinearDisjoint.map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) {K : Type u_1} [Field K] [Algebra F K] (f : E →ₐ[F] K) : (IntermediateField.map f A).LinearDisjoint ↥(IntermediateField.map f B)

Linear disjointness of intermediate fields is preserved by algebra homomorphisms.

theorem IntermediateField.LinearDisjoint.map' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) (K : Type u_1) [Field K] [Algebra F K] [Algebra L K] [IsScalarTower F L K] [Algebra E K] [IsScalarTower F E K] [IsScalarTower L E K] : (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L

Linear disjointness of an intermediate field with a tower of field embeddings is preserved by algebra homomorphisms.

theorem IntermediateField.LinearDisjoint.map'' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {L' : Type u_1} [Field L'] [Algebra F L'] [Algebra L' E] [IsScalarTower F L' E] (H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L') (K : Type u_2) [Field K] [Algebra F K] [Algebra L K] [IsScalarTower F L K] [Algebra L' K] [IsScalarTower F L' K] [Algebra E K] [IsScalarTower F E K] [IsScalarTower L E K] [IsScalarTower L' E K] : (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'

Linear disjointness is preserved by algebra homomorphism.

theorem IntermediateField.LinearDisjoint.self_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) : A.LinearDisjoint F

theorem IntermediateField.LinearDisjoint.bot_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) : A.LinearDisjoint ↥⊥

theorem IntermediateField.LinearDisjoint.bot_left (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : Type w) [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] : ⊥.LinearDisjoint L

theorem IntermediateField.LinearDisjoint.linearIndependent_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) {ι : Type u_1} {a : ι → ↥A} (ha : LinearIndependent F a) : LinearIndependent L (⇑A.val ∘ a)

If A and L are linearly disjoint, then any F-linearly independent family on A remains linearly independent over L.

theorem IntermediateField.LinearDisjoint.of_basis_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {ι : Type u_1} (a : Basis ι F ↥A) (H : LinearIndependent L (⇑A.val ∘ ⇑a)) : A.LinearDisjoint L

If there exists an F-basis of A which remains linearly independent over L, then A and L are linearly disjoint.

theorem IntermediateField.LinearDisjoint.linearIndependent_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) {ι : Type u_1} {b : ι → ↥B} (hb : LinearIndependent F b) : LinearIndependent (↥A) (⇑B.val ∘ b)

If A and B are linearly disjoint, then any F-linearly independent family on B remains linearly independent over A.

theorem IntermediateField.LinearDisjoint.of_basis_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} {ι : Type u_1} (b : Basis ι F ↥B) (H : LinearIndependent (↥A) (⇑B.val ∘ ⇑b)) : A.LinearDisjoint ↥B

If there exists an F-basis of B which remains linearly independent over A, then A and B are linearly disjoint.

theorem IntermediateField.LinearDisjoint.linearIndependent_right' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) {ι : Type u_1} {b : ι → L} (hb : LinearIndependent F b) : LinearIndependent (↥A) (⇑(algebraMap L E) ∘ b)

If A and L are linearly disjoint, then any F-linearly independent family on L remains linearly independent over A.

theorem IntermediateField.LinearDisjoint.of_basis_right' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {ι : Type u_1} (b : Basis ι F L) (H : LinearIndependent (↥A) (⇑(algebraMap L E) ∘ ⇑b)) : A.LinearDisjoint L

If there exists an F-basis of L which remains linearly independent over A, then A and L are linearly disjoint.

theorem IntermediateField.LinearDisjoint.linearIndependent_mul {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B} (ha : LinearIndependent F a) (hb : LinearIndependent F b) : LinearIndependent F fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)

If A and B are linearly disjoint, then for any F-linearly independent families { u_i }, { v_j } of A, B, the products { u_i * v_j } are linearly independent over F.

theorem IntermediateField.LinearDisjoint.linearIndependent_mul' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → L} (ha : LinearIndependent F a) (hb : LinearIndependent F b) : LinearIndependent F fun (i : κ × ι) => ↑(a i.1) * (algebraMap L E) (b i.2)

If A and L are linearly disjoint, then for any F-linearly independent families { u_i }, { v_j } of A, L, the products { u_i * v_j } are linearly independent over F.

theorem IntermediateField.LinearDisjoint.of_basis_mul {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} {κ : Type u_1} {ι : Type u_2} (a : Basis κ F ↥A) (b : Basis ι F ↥B) (H : LinearIndependent F fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)) : A.LinearDisjoint ↥B

If there are F-bases { u_i }, { v_j } of A, B, such that the products { u_i * v_j } are linearly independent over F, then A and B are linearly disjoint.

theorem IntermediateField.LinearDisjoint.of_basis_mul' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {κ : Type u_1} {ι : Type u_2} (a : Basis κ F ↥A) (b : Basis ι F L) (H : LinearIndependent F fun (i : κ × ι) => ↑(a i.1) * (algebraMap L E) (b i.2)) : A.LinearDisjoint L

If there are F-bases { u_i }, { v_j } of A, L, such that the products { u_i * v_j } are linearly independent over F, then A and L are linearly disjoint.

theorem IntermediateField.LinearDisjoint.of_le_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {A' : IntermediateField F E} (H : A.LinearDisjoint L) (h : A' ≤ A) : A'.LinearDisjoint L

theorem IntermediateField.LinearDisjoint.of_le_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B B' : IntermediateField F E} (H : A.LinearDisjoint ↥B) (h : B' ≤ B) : A.LinearDisjoint ↥B'

theorem IntermediateField.LinearDisjoint.of_le_right' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) (L' : Type u_1) [Field L'] [Algebra F L'] [Algebra L' L] [IsScalarTower F L' L] [Algebra L' E] [IsScalarTower F L' E] [IsScalarTower L' L E] : A.LinearDisjoint L'

Similar to IntermediateField.LinearDisjoint.of_le_right but this is for abstract fields.

theorem IntermediateField.LinearDisjoint.of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B A' B' : IntermediateField F E} (H : A.LinearDisjoint ↥B) (hA : A' ≤ A) (hB : B' ≤ B) : A'.LinearDisjoint ↥B'

If A and B are linearly disjoint, A' and B' are contained in A and B, respectively, then A' and B' are also linearly disjoint.

theorem IntermediateField.LinearDisjoint.of_le' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] {A' : IntermediateField F E} (H : A.LinearDisjoint L) (hA : A' ≤ A) (L' : Type u_1) [Field L'] [Algebra F L'] [Algebra L' L] [IsScalarTower F L' L] [Algebra L' E] [IsScalarTower F L' E] [IsScalarTower L' L E] : A'.LinearDisjoint L'

Similar to IntermediateField.LinearDisjoint.of_le but this is for abstract fields.

theorem IntermediateField.LinearDisjoint.inf_eq_bot {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) : A ⊓ B = ⊥

If A and B are linearly disjoint over F, then their intersection is equal to F.

theorem IntermediateField.LinearDisjoint.eq_bot_of_self {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} (H : A.LinearDisjoint ↥A) : A = ⊥

If A and A itself are linearly disjoint over F, then it is equal to F.

theorem IntermediateField.LinearDisjoint.rank_sup {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) : Module.rank F ↥(A ⊔ B) = Module.rank F ↥A * Module.rank F ↥B

If A and B are linearly disjoint over F, then the rank of A ⊔ B is equal to the product of that of A and B.

theorem IntermediateField.LinearDisjoint.finrank_sup {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) : Module.finrank F ↥(A ⊔ B) = Module.finrank F ↥A * Module.finrank F ↥B

If A and B are linearly disjoint over F, then the Module.finrank of A ⊔ B is equal to the product of that of A and B.

theorem IntermediateField.LinearDisjoint.of_finrank_sup {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} [FiniteDimensional F ↥A] [FiniteDimensional F ↥B] (H : Module.finrank F ↥(A ⊔ B) = Module.finrank F ↥A * Module.finrank F ↥B) : A.LinearDisjoint ↥B

If A and B are finite extensions of F, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.

theorem IntermediateField.LinearDisjoint.of_finrank_coprime {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : (Module.finrank F ↥A).Coprime (Module.finrank F L)) : A.LinearDisjoint L

If A and L have coprime degree over F, then they are linearly disjoint.

theorem IntermediateField.LinearDisjoint.isDomain {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) : IsDomain (TensorProduct F (↥A) L)

If A and L are linearly disjoint over F, then A ⊗[F] L is a domain.

theorem IntermediateField.LinearDisjoint.isDomain' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : Type u_1} {B : Type u_2} [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 (TensorProduct F A B)

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 IntermediateField.LinearDisjoint.of_isField {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : IsField (TensorProduct F (↥A) L)) : A.LinearDisjoint L

If A ⊗[F] L is a field, then A and L are linearly disjoint over F.

theorem IntermediateField.LinearDisjoint.of_isField' {F : Type u} [Field F] {A : Type v} [Field A] {B : Type w} [Field B] [Algebra F A] [Algebra F B] (H : IsField (TensorProduct F A B)) {K : Type u_1} [Field K] [Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K) : fa.fieldRange.LinearDisjoint ↥fb.fieldRange

If A and B are field extensions of F, such that A ⊗[F] B is a field, then for any field extension of F that A and B embed into, their images are linearly disjoint.

theorem IntermediateField.LinearDisjoint.exists_field_of_isDomain (F : Type u) [Field F] (A : Type v) [Field A] (B : Type w) [Field B] [Algebra F A] [Algebra F B] [IsDomain (TensorProduct F A B)] : ∃ (K : Type (max v w)) (x : Field K) (x_1 : Algebra F K) (fa : A →ₐ[F] K) (fb : B →ₐ[F] K), fa.fieldRange.LinearDisjoint ↥fb.fieldRange

If A and B are field extensions of F, such that A ⊗[F] B is a domain, then there exists a field extension of F that A and B embed into with linearly disjoint images.

theorem IntermediateField.LinearDisjoint.isField_of_forall (F : Type u) [Field F] (A : Type v) [Field A] (B : Type w) [Field B] [Algebra F A] [Algebra F B] (H : ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K), fa.fieldRange.LinearDisjoint ↥fb.fieldRange) : IsField (TensorProduct F A B)

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 Algebra.TensorProduct.isField_of_isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type u_1) [Field K] [Algebra F K] [IsDomain (TensorProduct F E K)] (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K) : IsField (TensorProduct F E K)

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 IntermediateField.LinearDisjoint.isField_of_isAlgebraic {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) (halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L) : IsField (TensorProduct F (↥A) L)

If A and L are linearly disjoint over F and one of them is algebraic, then A ⊗[F] L is a field.

theorem IntermediateField.LinearDisjoint.isField_of_isAlgebraic' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : Type u_1} {B : Type u_2} [Field A] [Algebra F A] [Field B] [Algebra F B] {fa : A →ₐ[F] E} {fb : B →ₐ[F] E} (H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange) (halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F B) : IsField (TensorProduct F A B)

If A and B are field extensions of F, one of them is algebraic, such that there exists a field E that A and B embeds into with linearly disjoint images, then A ⊗[F] B is a field.

theorem IntermediateField.LinearDisjoint.algEquiv_of_isAlgebraic {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A : IntermediateField F E} {L : Type w} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (H : A.LinearDisjoint L) {E' : Type u_1} [Field E'] [Algebra F E'] (B : IntermediateField F E') (L' : Type u_2) [Field L'] [Algebra F L'] [Algebra L' E'] [IsScalarTower F L' E'] (f1 : ↥A ≃ₐ[F] ↥B) (f2 : L ≃ₐ[F] L') (halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L) : B.LinearDisjoint L'

If A and L are linearly disjoint, one of them is algebraic, then for any B and L' isomorphic to A and L respectively, B and L' are also linearly disjoint.