[Merged by Bors] - refactor(FieldTheory/KrullTopology): clean up KrullTopology.lean

Mathlib/FieldTheory/AbelRuffini.lean

@@ -25,7 +25,7 @@ that is solvable by radicals has a solvable Galois group.
 
 noncomputable section
 
-open Polynomial IntermediateField
+open Polynomial
 
 section AbelRuffini
 
@@ -295,6 +295,8 @@ theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (
       rw [sub_comp, X_comp, C_comp]
       exact gal_X_pow_sub_C_isSolvable n q
 
+open IntermediateField
+
 /-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
 theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ := by
   let p := minpoly F α

Mathlib/FieldTheory/Galois/Basic.lean

@@ -186,32 +186,57 @@ def FixedPoints.intermediateField (M : Type*) [Monoid M] [MulSemiringAction M E]
 
 namespace IntermediateField
 
-/-- The intermediate field fixed by a subgroup -/
+/-- The intermediate field fixed by a subgroup. -/
 def fixedField : IntermediateField F E :=
   FixedPoints.intermediateField H
 
-theorem mem_fixedField_iff (x) :
+@[simp] lemma mem_fixedField_iff (x) :
     x ∈ fixedField H ↔ ∀ f ∈ H, f x = x := by
   show x ∈ MulAction.fixedPoints H E ↔ _
   simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]
 
+@[simp] lemma fixedField_bot : fixedField (⊥ : Subgroup (E ≃ₐ[F] E)) = ⊤ := by
+  ext
+  simp
+
 theorem finrank_fixedField_eq_card [FiniteDimensional F E] [DecidablePred (· ∈ H)] :
     finrank (fixedField H) E = Fintype.card H :=
   FixedPoints.finrank_eq_card H E
 
-/-- The subgroup fixing an intermediate field -/
+/-- The subgroup fixing an intermediate field. -/
 nonrec def fixingSubgroup : Subgroup (E ≃ₐ[F] E) :=
   fixingSubgroup (E ≃ₐ[F] E) (K : Set E)
 
 theorem le_iff_le : K ≤ fixedField H ↔ H ≤ fixingSubgroup K :=
   ⟨fun h g hg x => h (Subtype.mem x) ⟨g, hg⟩, fun h x hx g => h (Subtype.mem g) ⟨x, hx⟩⟩
 
-lemma fixingSubgroup_anti : Antitone (IntermediateField.fixingSubgroup (F := F) (E := E)) := by
-  intro K K' h
-  rw [← le_iff_le]
-  exact le_trans h ((le_iff_le _ _).mpr (le_refl K'.fixingSubgroup))
+/-- The map `K ↦ Gal(E/K)` is inclusion-reversing. -/
+theorem fixingSubgroup_le {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :
+    K2.fixingSubgroup ≤ K1.fixingSubgroup :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩
+
+theorem fixedField_le {H1 H2 : Subgroup (E ≃ₐ[F] E)} (h12 : H1 ≤ H2) :
+    fixedField H2 ≤ fixedField H1 :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩
+
+lemma fixingSubgroup_antitone : Antitone (@fixingSubgroup F _ E _ _) :=
+  fun _ _ ↦ fixingSubgroup_le
+
+lemma fixedField_antitone : Antitone (@fixedField F _ E _ _) :=
+  fun _ _ ↦ fixedField_le
+
+@[simp] lemma mem_fixingSubgroup_iff (σ) : σ ∈ fixingSubgroup K ↔ ∀ x ∈ K, σ x = x :=
+  _root_.mem_fixingSubgroup_iff _
 
-/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E` -/
+@[simp] lemma fixingSubgroup_top : fixingSubgroup (⊤ : IntermediateField F E) = ⊥ := by
+  ext
+  simp [DFunLike.ext_iff]
+
+@[simp] lemma fixingSubgroup_bot : fixingSubgroup (⊥ : IntermediateField F E) = ⊤ := by
+  ext
+  simp [mem_bot]
+
+/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E`. -/
 def fixingSubgroupEquiv : fixingSubgroup K ≃* E ≃ₐ[K] E where
   toFun ϕ := { AlgEquiv.toRingEquiv (ϕ : E ≃ₐ[F] E) with commutes' := ϕ.mem }
   invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩
@@ -264,6 +289,19 @@ theorem fixedField_fixingSubgroup [FiniteDimensional F E] [h : IsGalois F E] :
     Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
   exact (card_aut_eq_finrank K E).symm
 
+@[simp] lemma fixedField_top [IsGalois F E] [FiniteDimensional F E] :
+    fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥ := by
+  rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]
+
+theorem mem_bot_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
+    x ∈ (⊥ : IntermediateField F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x := by
+  rw [← fixedField_top, mem_fixedField_iff]
+  simp only [Subgroup.mem_top, forall_const]
+
+theorem mem_range_algebraMap_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
+    x ∈ Set.range (algebraMap F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x :=
+  mem_bot_iff_fixed x
+
 theorem card_fixingSubgroup_eq_finrank [DecidablePred (· ∈ IntermediateField.fixingSubgroup K)]
     [FiniteDimensional F E] [IsGalois F E] :
     Fintype.card (IntermediateField.fixingSubgroup K) = finrank K E := by
@@ -281,7 +319,7 @@ def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
     rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
     rfl
 
-/-- The Galois correspondence as a `GaloisInsertion` -/
+/-- The Galois correspondence as a `GaloisInsertion`. -/
 def galoisInsertionIntermediateFieldSubgroup [FiniteDimensional F E] :
     GaloisInsertion (OrderDual.toDual ∘
       (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
@@ -292,7 +330,7 @@ def galoisInsertionIntermediateFieldSubgroup [FiniteDimensional F E] :
   le_l_u H := le_of_eq (IntermediateField.fixingSubgroup_fixedField H).symm
   choice_eq _ _ := rfl
 
-/-- The Galois correspondence as a `GaloisCoinsertion` -/
+/-- The Galois correspondence as a `GaloisCoinsertion`. -/
 def galoisCoinsertionIntermediateFieldSubgroup [FiniteDimensional F E] [IsGalois F E] :
     GaloisCoinsertion (OrderDual.toDual ∘
       (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
@@ -315,8 +353,8 @@ open scoped Pointwise
 
 lemma IntermediateField.restrictNormalHom_ker (E : IntermediateField K L) [Normal K E] :
     (restrictNormalHom E).ker = E.fixingSubgroup := by
-  simp [fixingSubgroup, Subgroup.ext_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
-    restrictNormalHom_apply, mem_fixingSubgroup_iff]
+  simp only [Subgroup.ext_iff, MonoidHom.mem_ker, AlgEquiv.ext_iff, one_apply, Subtype.ext_iff,
+    restrictNormalHom_apply, Subtype.forall, mem_fixingSubgroup_iff, implies_true]
 
 namespace IsGalois
 
@@ -478,7 +516,7 @@ theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separ
   refine LinearEquiv.finrank_eq ?_
   rfl
 
-/-- Equivalent characterizations of a Galois extension of finite degree -/
+/-- Equivalent characterizations of a Galois extension of finite degree. -/
 theorem tfae [FiniteDimensional F E] : List.TFAE [
     IsGalois F E,
     IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥,

Mathlib/FieldTheory/Galois/Infinite.lean

@@ -150,7 +150,7 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup (K ≃ₐ[k] K)) [IsGalois k
     apply sub'
     simp only [← muleq, ← eq]
     apply Set.smul_mem_smul_set
-    exact (IntermediateField.fixingSubgroup.antimono (IntermediateField.le_normalClosure L) hτ)
+    exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)
   have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x :=
     fun x hx ↦ ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hσ) x hx.1
   rw [restrict_fixedField H.1 L'.1] at fix

Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

@@ -188,25 +188,6 @@ theorem iSup_toSubfield {ι : Sort*} [Nonempty ι] (S : ι → IntermediateField
     (iSup S).toSubfield = ⨆ i, (S i).toSubfield := by
   simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]
 
-/-- Construct an algebra isomorphism from an equality of intermediate fields -/
-@[simps! apply]
-def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
-  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)
-
-@[simp]
-theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) :
-    (equivOfEq h).symm = equivOfEq h.symm :=
-  rfl
-
-@[simp]
-theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl := by
-  ext; rfl
-
-@[simp]
-theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
-    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
-  rfl
-
 variable (F E)
 
 /-- The bottom intermediate_field is isomorphic to the field. -/
@@ -311,24 +292,6 @@ theorem _root_.AlgEquiv.fieldRange_eq_top (f : E ≃ₐ[F] K) :
 
 end Lattice
 
-section equivMap
-
-variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E]
-  {K : Type*} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K)
-
-theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
-  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
-
-/-- An intermediate field is isomorphic to its image under an `AlgHom`
-(which is automatically injective) -/
-noncomputable def equivMap : L ≃ₐ[F] L.map f :=
-  (AlgEquiv.ofInjective _ (f.comp L.val).injective).trans (equivOfEq (fieldRange_comp_val L f))
-
-@[simp]
-theorem coe_equivMap_apply (x : L) : ↑(equivMap L f x) = f x := rfl
-
-end equivMap
-
 section AdjoinDef
 
 variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (S : Set E)

Mathlib/FieldTheory/IntermediateField/Algebraic.lean

@@ -97,6 +97,12 @@ theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
     (h_finrank : finrank F L = finrank E L) : F = E :=
   eq_of_le_of_finrank_le' h_le h_finrank.le
 
+/-- Mapping a finite dimensional intermediate field along an algebra equivalence gives
+a finite-dimensional intermediate field. -/
+instance finiteDimensional_map (f : L →ₐ[K] L) [FiniteDimensional K E] :
+    FiniteDimensional K (E.map f) :=
+  LinearEquiv.finiteDimensional (IntermediateField.equivMap E f).toLinearEquiv
+
 end FiniteDimensional
 
 theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=

Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -163,7 +163,7 @@ protected theorem mul_mem {x y : L} : x ∈ S → y ∈ S → x * y ∈ S :=
 protected theorem add_mem {x y : L} : x ∈ S → y ∈ S → x + y ∈ S :=
   add_mem
 
-/-- An intermediate field is closed under subtraction -/
+/-- An intermediate field is closed under subtraction. -/
 protected theorem sub_mem {x y : L} : x ∈ S → y ∈ S → x - y ∈ S :=
   sub_mem
 
@@ -242,7 +242,7 @@ instance instSMulMemClass : SMulMemClass (IntermediateField K L) K L where
 
 end IntermediateField
 
-/-- Turn a subalgebra closed under inverses into an intermediate field -/
+/-- Turn a subalgebra closed under inverses into an intermediate field. -/
 def Subalgebra.toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
     IntermediateField K L :=
   { S with
@@ -260,7 +260,7 @@ theorem toIntermediateField_toSubalgebra (S : IntermediateField K L) :
   ext
   rfl
 
-/-- Turn a subalgebra satisfying `IsField` into an intermediate_field -/
+/-- Turn a subalgebra satisfying `IsField` into an intermediate_field. -/
 def Subalgebra.toIntermediateField' (S : Subalgebra K L) (hS : IsField S) : IntermediateField K L :=
   S.toIntermediateField fun x hx => by
     by_cases hx0 : x = 0
@@ -283,15 +283,15 @@ theorem toIntermediateField'_toSubalgebra (S : IntermediateField K L) :
   ext
   rfl
 
-/-- Turn a subfield of `L` containing the image of `K` into an intermediate field -/
+/-- Turn a subfield of `L` containing the image of `K` into an intermediate field. -/
 def Subfield.toIntermediateField (S : Subfield L) (algebra_map_mem : ∀ x, algebraMap K L x ∈ S) :
     IntermediateField K L :=
   { S with
     algebraMap_mem' := algebra_map_mem }
 
 namespace IntermediateField
 
-/-- An intermediate field inherits a field structure -/
+/-- An intermediate field inherits a field structure. -/
 instance toField : Field S :=
   S.toSubfield.toField
 
@@ -404,7 +404,7 @@ instance isScalarTower_mid {R : Type*} [Semiring R] [Algebra L R] [Algebra K R]
     [IsScalarTower K L R] : IsScalarTower K S R :=
   IsScalarTower.subalgebra' _ _ _ S.toSubalgebra
 
-/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L` -/
+/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L`. -/
 instance isScalarTower_mid' : IsScalarTower K S L :=
   inferInstance
 
@@ -444,6 +444,10 @@ theorem toSubalgebra_map (f : L →ₐ[K] L') : (S.map f).toSubalgebra = S.toSub
 theorem toSubfield_map (f : L →ₐ[K] L') : (S.map f).toSubfield = S.toSubfield.map f :=
   rfl
 
+/-- Mapping intermediate fields along the identity does not change them. -/
+theorem map_id : S.map (AlgHom.id K L) = S :=
+  SetLike.coe_injective <| Set.image_id _
+
 theorem map_map {K L₁ L₂ L₃ : Type*} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂]
     [Field L₃] [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
     (E.map f).map g = E.map (g.comp f) :=
@@ -463,7 +467,7 @@ theorem gc_map_comap (f : L →ₐ[K] L') : GaloisConnection (map f) (comap f) :
 
 /-- Given an equivalence `e : L ≃ₐ[K] L'` of `K`-field extensions and an intermediate
 field `E` of `L/K`, `intermediateFieldMap e E` is the induced equivalence
-between `E` and `E.map e` -/
+between `E` and `E.map e`. -/
 def intermediateFieldMap (e : L ≃ₐ[K] L') (E : IntermediateField K L) : E ≃ₐ[K] E.map e.toAlgHom :=
   e.subalgebraMap E.toSubalgebra
 
@@ -603,7 +607,7 @@ variable {S}
 
 section Tower
 
-/-- Lift an intermediate_field of an intermediate_field -/
+/-- Lift an intermediate_field of an intermediate_field. -/
 def lift {F : IntermediateField K L} (E : IntermediateField K F) : IntermediateField K L :=
   E.map (val F)
 
@@ -618,7 +622,7 @@ theorem mem_lift {F : IntermediateField K L} {E : IntermediateField K F} (x : F)
     x.1 ∈ lift E ↔ x ∈ E :=
   Subtype.val_injective.mem_set_image
 
-/-- The algEquiv between an intermediate field and its lift -/
+/-- The algEquiv between an intermediate field and its lift. -/
 def liftAlgEquiv {E : IntermediateField K L} (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F where
   toFun x := ⟨x.1.1, (mem_lift x.1).mpr x.2⟩
   invFun x := ⟨⟨x.1, lift_le F x.2⟩, (mem_lift ⟨x.1, lift_le F x.2⟩).mp x.2⟩
@@ -673,6 +677,43 @@ example {F : IntermediateField K L} {E : IntermediateField F L} : Algebra K E :=
 
 end Tower
 
+section equivMap
+
+variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E]
+  {K : Type*} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K)
+
+/-- Construct an algebra isomorphism from an equality of intermediate fields. -/
+@[simps! apply]
+def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
+  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)
+
+@[simp]
+theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) :
+    (equivOfEq h).symm = equivOfEq h.symm :=
+  rfl
+
+@[simp]
+theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl :=
+  AlgEquiv.ext fun _ ↦ rfl
+
+@[simp]
+theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
+    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
+  rfl
+
+theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
+  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
+
+/-- An intermediate field is isomorphic to its image under an `AlgHom`
+(which is automatically injective). -/
+noncomputable def equivMap : L ≃ₐ[F] L.map f :=
+  (AlgEquiv.ofInjective _ (f.comp L.val).injective).trans (equivOfEq (fieldRange_comp_val L f))
+
+@[simp]
+theorem coe_equivMap_apply (x : L) : ↑(equivMap L f x) = f x := rfl
+
+end equivMap
+
 end IntermediateField
 
 section ExtendScalars