Linearly disjoint fields

This file contains basics about the linearly disjoint fields.

Linear disjoint intermediate fields

We adapt the definitions in https://en.wikipedia.org/wiki/Linearly_disjoint. See the file Mathlib/LinearAlgebra/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.

Other main results:

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

• IntermediateField.LinearDisjoint.rank_sup_of_isAlgebraic, 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.

  TODO: remove the algebraic assumptions (the proof becomes complicated).

• 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.

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.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_of_isAlgebraic {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (H : A.LinearDisjoint ↥B) (halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F ↥B) : Module.rank F ↥(A ⊔ B) = Module.rank F ↥A * Module.rank F ↥B

If A and B are linearly disjoint over F, and at least one them are algebraic, then the rank of A ⊔ B is equal to the product of that of A and B. Note that this result is also true without algebraic assumption, but the proof becomes very complicated.

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.