refactor(FieldTheory/Adjoin): provide a better defeq for ⊥ (#7957)

This means `(⊥ : IntermediateField F E).toSubalgebra = ⊥` is true by definition.

Also adds `IntermediateField.map_bot` now that the proof is trivial.

Author: eric-wieser

Mathlib/FieldTheory/Adjoin.lean

@@ -75,26 +75,29 @@ def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E)
   choice_eq _ _ := copy_eq _ _ _
 #align intermediate_field.gi IntermediateField.gi
 
-instance : CompleteLattice (IntermediateField F E) :=
-  GaloisInsertion.liftCompleteLattice IntermediateField.gi
+instance : CompleteLattice (IntermediateField F E) where
+  __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi
+  bot :=
+    { toSubalgebra := ⊥
+      inv_mem' := fun x (hx : x ∈ (⊥ : Subalgebra F E)) => show x⁻¹ ∈ (⊥ : Subalgebra F E) by
+        rw [Algebra.mem_bot] at hx ⊢
+        obtain ⟨r, rfl⟩ := hx
+        exact ⟨r⁻¹, map_inv₀ _ _⟩ }
+  bot_le x := (bot_le : ⊥ ≤ x.toSubalgebra)
 
 instance : Inhabited (IntermediateField F E) :=
   ⟨⊤⟩
 
-theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) := by
-  change ↑(Subfield.closure (Set.range (algebraMap F E) ∪ ∅)) = Set.range (algebraMap F E)
-  rw [Set.union_empty, ← Set.image_univ, ← RingHom.map_field_closure]
-  simp
+theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) :=
+  Algebra.coe_bot
 #align intermediate_field.coe_bot IntermediateField.coe_bot
 
 theorem mem_bot {x : E} : x ∈ (⊥ : IntermediateField F E) ↔ x ∈ Set.range (algebraMap F E) :=
-  Set.ext_iff.mp coe_bot x
+  Algebra.mem_bot
 #align intermediate_field.mem_bot IntermediateField.mem_bot
 
 @[simp]
-theorem bot_toSubalgebra : (⊥ : IntermediateField F E).toSubalgebra = ⊥ := by
-  ext
-  rw [mem_toSubalgebra, Algebra.mem_bot, mem_bot]
+theorem bot_toSubalgebra : (⊥ : IntermediateField F E).toSubalgebra = ⊥ := rfl
 #align intermediate_field.bot_to_subalgebra IntermediateField.bot_toSubalgebra
 
 @[simp]
@@ -269,6 +272,11 @@ theorem restrictScalars_top {K : Type*} [Field K] [Algebra K E] [Algebra K F]
   rfl
 #align intermediate_field.restrict_scalars_top IntermediateField.restrictScalars_top
 
+@[simp]
+theorem map_bot {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) :
+    IntermediateField.map f ⊥ = ⊥ :=
+  toSubalgebra_injective <| Algebra.map_bot _
+
 theorem _root_.AlgHom.fieldRange_eq_map {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) :
     f.fieldRange = IntermediateField.map f ⊤ :=
   SetLike.ext' Set.image_univ.symm