feat(field_theory/intermediate_field): equalities from inclusions and…

… dimension bounds (#4828)

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/field_theory/intermediate_field.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 
 import field_theory.subfield
-import ring_theory.algebra_tower
+import field_theory.tower
 
 /-!
 # Intermediate fields
@@ -42,6 +42,7 @@ A `subalgebra` is closed under all operations except `⁻¹`,
 intermediate field, field extension
 -/
 
+open finite_dimensional
 open_locale big_operators
 
 variables (K L : Type*) [field K] [field L] [algebra K L]
@@ -286,4 +287,39 @@ instance has_lift2 {F : intermediate_field K L} :
 
 end tower
 
+section finite_dimensional
+
+instance finite_dimensional_left [finite_dimensional K L] (F : intermediate_field K L) :
+  finite_dimensional K F :=
+finite_dimensional.finite_dimensional_submodule F.to_subalgebra.to_submodule
+
+instance finite_dimensional_right [finite_dimensional K L] (F : intermediate_field K L) :
+  finite_dimensional F L :=
+right K F L
+
+lemma eq_of_le_of_findim_le [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+  (h_findim : findim K E ≤ findim K F) : F = E :=
+intermediate_field.ext'_iff.mpr (submodule.ext'_iff.mp (eq_of_le_of_findim_le
+  (show F.to_subalgebra.to_submodule ≤ E.to_subalgebra.to_submodule, by exact h_le) h_findim))
+
+lemma eq_of_le_of_findim_eq [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+  (h_findim : findim K F = findim K E) : F = E :=
+eq_of_le_of_findim_le h_le h_findim.ge
+
+lemma eq_of_le_of_findim_le' [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+  (h_findim : findim F L ≤ findim E L) : F = E :=
+begin
+  apply eq_of_le_of_findim_le h_le,
+  have h1 := findim_mul_findim K F L,
+  have h2 := findim_mul_findim K E L,
+  have h3 : 0 < findim E L := findim_pos,
+  nlinarith,
+end
+
+lemma eq_of_le_of_findim_eq' [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+  (h_findim : findim F L = findim E L) : F = E :=
+eq_of_le_of_findim_le' h_le h_findim.le
+
+end finite_dimensional
+
 end intermediate_field

src/linear_algebra/finite_dimensional.lean

@@ -656,14 +656,19 @@ end linear_equiv
 
 namespace finite_dimensional
 
+lemma eq_of_le_of_findim_le {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ ≤ S₂)
+  (hd : findim K S₂ ≤ findim K S₁) : S₁ = S₂ :=
+begin
+  rw ←linear_equiv.findim_eq (submodule.comap_subtype_equiv_of_le hle) at hd,
+  exact le_antisymm hle (submodule.comap_subtype_eq_top.1 (eq_top_of_findim_eq
+    (le_antisymm (comap (submodule.subtype S₂) S₁).findim_le hd))),
+end
+
 /-- If a submodule is less than or equal to a finite-dimensional
 submodule with the same dimension, they are equal. -/
 lemma eq_of_le_of_findim_eq {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ ≤ S₂)
   (hd : findim K S₁ = findim K S₂) : S₁ = S₂ :=
-begin
-  rw ←linear_equiv.findim_eq (submodule.comap_subtype_equiv_of_le hle) at hd,
-  exact le_antisymm hle (submodule.comap_subtype_eq_top.1 (eq_top_of_findim_eq hd))
-end
+eq_of_le_of_findim_le hle hd.ge
 
 end finite_dimensional