feat(field_theory/adjoin): lemmas about infs of `intermediate_field…

…`s (#10997)

This adjusts the data in the `galois_insertion` slightly such that this new lemma is true by `rfl`, to match how we handle this in `subalgebra`. As a result, `top_to_subalgebra` is now refl, but `adjoin_univ` is no longer refl.

This also adds a handful of trivial simp lemmas.

src/field_theory/adjoin.lean

@@ -53,32 +53,75 @@ lemma gc : galois_connection (adjoin F : set E → intermediate_field F E) coe :
 
 /-- Galois insertion between `adjoin` and `coe`. -/
 def gi : galois_insertion (adjoin F : set E → intermediate_field F E) coe :=
-{ choice := λ S _, adjoin F S,
+{ choice := λ s hs, (adjoin F s).copy s $ le_antisymm (gc.le_u_l s) hs,
   gc := intermediate_field.gc,
   le_l_u := λ S, (intermediate_field.gc (S : set E) (adjoin F S)).1 $ le_refl _,
-  choice_eq := λ _ _, rfl }
+  choice_eq := λ _ _, copy_eq _ _ _ }
 
 instance : complete_lattice (intermediate_field F E) :=
 galois_insertion.lift_complete_lattice intermediate_field.gi
 
 instance : inhabited (intermediate_field F E) := ⟨⊤⟩
 
-lemma mem_bot {x : E} : x ∈ (⊥ : intermediate_field F E) ↔ x ∈ set.range (algebra_map F E) :=
+lemma coe_bot : ↑(⊥ : intermediate_field F E) = set.range (algebra_map F E) :=
 begin
-  suffices : set.range (algebra_map F E) = (⊥ : intermediate_field F E),
-  { rw this, refl },
-  { change set.range (algebra_map F E) = subfield.closure (set.range (algebra_map F E) ∪ ∅),
-    simp [←set.image_univ, ←ring_hom.map_field_closure] }
+  change ↑(subfield.closure (set.range (algebra_map F E) ∪ ∅)) = set.range (algebra_map F E),
+  simp [←set.image_univ, ←ring_hom.map_field_closure]
 end
 
-lemma mem_top {x : E} : x ∈ (⊤ : intermediate_field F E) :=
-subfield.subset_closure $ or.inr trivial
+lemma mem_bot {x : E} : x ∈ (⊥ : intermediate_field F E) ↔ x ∈ set.range (algebra_map F E) :=
+set.ext_iff.mp coe_bot x
 
 @[simp] lemma bot_to_subalgebra : (⊥ : intermediate_field F E).to_subalgebra = ⊥ :=
 by { ext, rw [mem_to_subalgebra, algebra.mem_bot, mem_bot] }
 
+@[simp] lemma coe_top : ↑(⊤ : intermediate_field F E) = (set.univ : set E) := rfl
+
+@[simp] lemma mem_top {x : E} : x ∈ (⊤ : intermediate_field F E) :=
+trivial
+
 @[simp] lemma top_to_subalgebra : (⊤ : intermediate_field F E).to_subalgebra = ⊤ :=
-by { ext, rw [mem_to_subalgebra, iff_true_right algebra.mem_top], exact mem_top }
+rfl
+
+@[simp] lemma top_to_subfield : (⊤ : intermediate_field F E).to_subfield = ⊤ :=
+rfl
+
+@[simp, norm_cast]
+lemma coe_inf (S T : intermediate_field F E) : (↑(S ⊓ T) : set E) = S ∩ T := rfl
+
+@[simp]
+lemma mem_inf {S T : intermediate_field F E} {x : E} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T := iff.rfl
+
+@[simp] lemma inf_to_subalgebra (S T : intermediate_field F E) :
+  (S ⊓ T).to_subalgebra = S.to_subalgebra ⊓ T.to_subalgebra :=
+rfl
+
+@[simp] lemma inf_to_subfield (S T : intermediate_field F E) :
+  (S ⊓ T).to_subfield = S.to_subfield ⊓ T.to_subfield :=
+rfl
+
+@[simp, norm_cast]
+lemma coe_Inf (S : set (intermediate_field F E)) : (↑(Inf S) : set E) = Inf (coe '' S) := rfl
+
+@[simp] lemma Inf_to_subalgebra (S : set (intermediate_field F E)) :
+  (Inf S).to_subalgebra = Inf (to_subalgebra '' S) :=
+set_like.coe_injective $ by simp [set.sUnion_image]
+
+@[simp] lemma Inf_to_subfield (S : set (intermediate_field F E)) :
+  (Inf S).to_subfield = Inf (to_subfield '' S) :=
+set_like.coe_injective $ by simp [set.sUnion_image]
+
+@[simp, norm_cast]
+lemma coe_infi {ι : Sort*} (S : ι → intermediate_field F E) : (↑(infi S) : set E) = ⋂ i, (S i) :=
+by simp [infi]
+
+@[simp] lemma infi_to_subalgebra {ι : Sort*} (S : ι → intermediate_field F E) :
+  (infi S).to_subalgebra = ⨅ i, (S i).to_subalgebra :=
+set_like.coe_injective $ by simp [infi]
+
+@[simp] lemma infi_to_subfield {ι : Sort*} (S : ι → intermediate_field F E) :
+  (infi S).to_subfield = ⨅ i, (S i).to_subfield :=
+set_like.coe_injective $ by simp [infi]
 
 /--  Construct an algebra isomorphism from an equality of intermediate fields -/
 @[simps apply]
@@ -179,6 +222,10 @@ lemma subset_adjoin_of_subset_right {T : set E} (H : T ⊆ S) : T ⊆ adjoin F S
   adjoin F (∅ : set E) = ⊥ :=
 eq_bot_iff.mpr (adjoin_le_iff.mpr (set.empty_subset _))
 
+@[simp] lemma adjoin_univ (F E : Type*) [field F] [field E] [algebra F E] :
+  adjoin F (set.univ : set E) = ⊤ :=
+eq_top_iff.mpr $ subset_adjoin _ _
+
 /-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`. -/
 lemma adjoin_le_subfield {K : subfield E} (HF : set.range (algebra_map F E) ⊆ K)
   (HS : S ⊆ K) : (adjoin F S).to_subfield ≤ K :=

src/field_theory/intermediate_field.lean

@@ -115,6 +115,24 @@ theorem inv_mem : ∀ {x : L}, x ∈ S → x⁻¹ ∈ S := S.inv_mem'
 theorem div_mem {x y : L} (hx : x ∈ S) (hy : y ∈ S) : x / y ∈ S :=
 S.to_subfield.div_mem hx hy
 
+/-- Copy of an intermediate field with a new `carrier` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
+  intermediate_field K L :=
+{ to_subalgebra := S.to_subalgebra.copy s (hs : s = (S.to_subalgebra).carrier),
+  neg_mem' :=
+    have hs' : (S.to_subalgebra.copy s hs).carrier = (S.to_subalgebra).carrier := hs,
+    hs'.symm ▸ S.neg_mem',
+  inv_mem' :=
+    have hs' : (S.to_subalgebra.copy s hs).carrier = (S.to_subalgebra).carrier := hs,
+    hs'.symm ▸ S.inv_mem' }
+
+@[simp] lemma coe_copy (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
+  (S.copy s hs : set L) = s := rfl
+
+lemma copy_eq (S : intermediate_field K L) (s : set L) (hs : s = ↑S) : S.copy s hs = S :=
+set_like.coe_injective hs
+
 /-- Product of a list of elements in an intermediate_field is in the intermediate_field. -/
 lemma list_prod_mem {l : list L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S :=
 S.to_subfield.list_prod_mem

src/field_theory/normal.lean

@@ -264,13 +264,14 @@ variables {F} {K} (E : Type*) [field E] [algebra F E] [algebra K E] [is_scalar_t
   an algebra homomorphism `ϕ : K →ₐ[F] K` to `ϕ.lift_normal E : E →ₐ[F] E`. -/
 noncomputable def alg_hom.lift_normal [h : normal F E] : E →ₐ[F] E :=
 @alg_hom.restrict_scalars F K E E _ _ _ _ _ _
-  ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra _ _ _ _
-  (nonempty.some (@intermediate_field.alg_hom_mk_adjoin_splits' K E E _ _ _ _
-  ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra ⊤ rfl
+  ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra _ _ _ _ $ nonempty.some $
+  @intermediate_field.alg_hom_mk_adjoin_splits' _ _ _ _ _ _ _
+  ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra _
+  (intermediate_field.adjoin_univ _ _)
   (λ x hx, ⟨is_integral_of_is_scalar_tower x (h.out x).1,
-  splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
-  (by { rw [splits_map_iff, ←is_scalar_tower.algebra_map_eq], exact (h.out x).2 })
-  (minpoly.dvd_map_of_is_scalar_tower F K x)⟩)))
+    splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
+    (by { rw [splits_map_iff, ←is_scalar_tower.algebra_map_eq], exact (h.out x).2 })
+    (minpoly.dvd_map_of_is_scalar_tower F K x)⟩)
 
 @[simp] lemma alg_hom.lift_normal_commutes [normal F E] (x : K) :
   ϕ.lift_normal E (algebra_map K E x) = algebra_map K E (ϕ x) :=