chore(field_theory/galois): make `intermediate_field.fixing_subgroup_…

…equiv` computable (#11938)

This also golfs and generalizes some results to reuse infrastructure from elsewhere.

In particular, this generalizes:

* `intermediate_field.fixed_field` to `fixed_points.intermediate_field`, where the latter matches the API of `fixed_points.subfield`
* `intermediate_field.fixing_subgroup` to `fixing_subgroup` and `fixing_submonoid`

This removes `open_locale classical` in favor of ensuring the lemmas take in the necessary decidable / fintype arguments.

src/field_theory/fixed.lean

@@ -100,7 +100,7 @@ polynomial.induction_on p
   (λ n x ih, by rw [smul_mul', polynomial.smul_C, smul, smul_pow', polynomial.smul_X])
 
 instance : algebra (fixed_points.subfield M F) F :=
-algebra.of_subring (fixed_points.subfield M F).to_subring
+by apply_instance
 
 theorem coe_algebra_map :
   algebra_map (fixed_points.subfield M F) F = subfield.subtype (fixed_points.subfield M F) :=

src/field_theory/galois.lean

@@ -32,8 +32,7 @@ Together, these two result prove the Galois correspondence
 - `is_galois.tfae` : Equivalent characterizations of a Galois extension of finite degree
 -/
 
-noncomputable theory
-open_locale classical polynomial
+open_locale polynomial
 
 open finite_dimensional alg_equiv
 
@@ -163,40 +162,48 @@ section galois_correspondence
 variables {F : Type*} [field F] {E : Type*} [field E] [algebra F E]
 variables (H : subgroup (E ≃ₐ[F] E)) (K : intermediate_field F E)
 
+/-- The intermediate field of fixed points fixed by a monoid action that commutes with the
+`F`-action on `E`. -/
+def fixed_points.intermediate_field (M : Type*) [monoid M] [mul_semiring_action M E]
+  [smul_comm_class M F E] : intermediate_field F E :=
+{ carrier := mul_action.fixed_points M E,
+  algebra_map_mem' := λ a g, by rw [algebra.algebra_map_eq_smul_one, smul_comm, smul_one],
+  ..fixed_points.subfield M E }
+
+/-- The submonoid fixing a set under a `mul_action`. -/
+@[to_additive /-" The additive submonoid fixing a set under an `add_action`. "-/]
+def fixing_submonoid (M : Type*) {α} [monoid M] [mul_action M α] (s : set α) : submonoid M :=
+{ carrier := { ϕ : M | ∀ x : s, ϕ • (x : α) = x },
+  one_mem' := λ _, one_smul _ _,
+  mul_mem' := λ x y hx hy z, by rw [mul_smul, hy z, hx z], }
+
+/-- The subgroup fixing a set under a `mul_action`. -/
+@[to_additive /-" The additive subgroup fixing a set under an `add_action`. "-/]
+def fixing_subgroup (M : Type*) {α} [group M] [mul_action M α] (s : set α) : subgroup M :=
+{ inv_mem' := λ _ hx z, by rw [inv_smul_eq_iff, hx z],
+  ..fixing_submonoid M s, }
+
 namespace intermediate_field
 
 /-- The intermediate_field fixed by a subgroup -/
 def fixed_field : intermediate_field F E :=
-{ carrier := mul_action.fixed_points H E,
-  zero_mem' := λ g, smul_zero g,
-  add_mem' := λ a b hx hy g, by rw [smul_add g a b, hx, hy],
-  neg_mem' := λ a hx g, by rw [smul_neg g a, hx],
-  one_mem' := λ g, smul_one g,
-  mul_mem' := λ a b hx hy g, by rw [smul_mul' g a b, hx, hy],
-  inv_mem' := λ a hx g, by rw [smul_inv'' g a, hx],
-  algebra_map_mem' := λ a g, commutes g a }
-
-lemma finrank_fixed_field_eq_card [finite_dimensional F E] :
+fixed_points.intermediate_field H
+
+lemma finrank_fixed_field_eq_card [finite_dimensional F E] [decidable_pred (∈ H)] :
   finrank (fixed_field H) E = fintype.card H :=
 fixed_points.finrank_eq_card H E
 
 /-- The subgroup fixing an intermediate_field -/
 def fixing_subgroup : subgroup (E ≃ₐ[F] E) :=
-{ carrier := λ ϕ, ∀ x : K, ϕ x = x,
-  one_mem' := λ _, rfl,
-  mul_mem' := λ _ _ hx hy _, (congr_arg _ (hy _)).trans (hx _),
-  inv_mem' := λ _ hx _, (equiv.symm_apply_eq (to_equiv _)).mpr (hx _).symm }
+fixing_subgroup (E ≃ₐ[F] E) (K : set E)
 
 lemma le_iff_le : K ≤ fixed_field H ↔ H ≤ fixing_subgroup K :=
 ⟨λ h g hg x, h (subtype.mem x) ⟨g, hg⟩, λ h x hx g, h (subtype.mem g) ⟨x, hx⟩⟩
 
 /-- The fixing_subgroup of `K : intermediate_field F E` is isomorphic to `E ≃ₐ[K] E` -/
 def fixing_subgroup_equiv : fixing_subgroup K ≃* (E ≃ₐ[K] E) :=
-{ to_fun := λ ϕ, of_bijective (alg_hom.mk ϕ (map_one ϕ) (map_mul ϕ)
-    (map_zero ϕ) (map_add ϕ) (ϕ.mem)) (bijective ϕ),
-  inv_fun := λ ϕ, ⟨of_bijective (alg_hom.mk ϕ (ϕ.map_one) (ϕ.map_mul)
-    (ϕ.map_zero) (ϕ.map_add) (λ r, ϕ.commutes (algebra_map F K r)))
-      (ϕ.bijective), ϕ.commutes⟩,
+{ to_fun := λ ϕ, { commutes' := ϕ.mem, ..alg_equiv.to_ring_equiv ↑ϕ },
+  inv_fun := λ ϕ, ⟨ϕ.restrict_scalars _, ϕ.commutes⟩,
   left_inv := λ _, by { ext, refl },
   right_inv := λ _, by { ext, refl },
   map_mul' := λ _ _, by { ext, refl } }
@@ -205,6 +212,7 @@ theorem fixing_subgroup_fixed_field [finite_dimensional F E] :
   fixing_subgroup (fixed_field H) = H :=
 begin
   have H_le : H ≤ (fixing_subgroup (fixed_field H)) := (le_iff_le _ _).mp le_rfl,
+  classical,
   suffices : fintype.card H = fintype.card (fixing_subgroup (fixed_field H)),
   { exact set_like.coe_injective
       (set.eq_of_inclusion_surjective ((fintype.bijective_iff_injective_and_card
@@ -240,12 +248,14 @@ begin
   suffices : finrank K E =
     finrank (intermediate_field.fixed_field (intermediate_field.fixing_subgroup K)) E,
   { exact (intermediate_field.eq_of_le_of_finrank_eq' K_le this).symm },
+  classical,
   rw [intermediate_field.finrank_fixed_field_eq_card,
     fintype.card_congr (intermediate_field.fixing_subgroup_equiv K).to_equiv],
   exact (card_aut_eq_finrank K E).symm,
 end
 
-lemma card_fixing_subgroup_eq_finrank [finite_dimensional F E] [is_galois F E] :
+lemma card_fixing_subgroup_eq_finrank [decidable_pred (∈ intermediate_field.fixing_subgroup K)]
+  [finite_dimensional F E] [is_galois F E] :
   fintype.card (intermediate_field.fixing_subgroup K) = finrank K E :=
 by conv { to_rhs, rw [←fixed_field_fixing_subgroup K,
   intermediate_field.finrank_fixed_field_eq_card] }
@@ -311,6 +321,7 @@ lemma of_fixed_field_eq_bot [finite_dimensional F E]
   (h : intermediate_field.fixed_field (⊤ : subgroup (E ≃ₐ[F] E)) = ⊥) : is_galois F E :=
 begin
   rw [←is_galois_iff_is_galois_bot, ←h],
+  classical,
   exact is_galois.of_fixed_field E (⊤ : subgroup (E ≃ₐ[F] E)),
 end
 
@@ -319,6 +330,7 @@ lemma of_card_aut_eq_finrank [finite_dimensional F E]
 begin
   apply of_fixed_field_eq_bot,
   have p : 0 < finrank (intermediate_field.fixed_field (⊤ : subgroup (E ≃ₐ[F] E))) E := finrank_pos,
+  classical,
   rw [←intermediate_field.finrank_eq_one_iff, ←mul_left_inj' (ne_of_lt p).symm, finrank_mul_finrank,
       ←h, one_mul, intermediate_field.finrank_fixed_field_eq_card],
   apply fintype.card_congr,
@@ -363,6 +375,7 @@ lemma of_separable_splitting_field [sp : p.is_splitting_field F E] (hp : p.separ
   is_galois F E :=
 begin
   haveI hFE : finite_dimensional F E := polynomial.is_splitting_field.finite_dimensional E p,
+  letI := classical.dec_eq E,
   let s := (p.map (algebra_map F E)).roots.to_finset,
   have adjoin_root : intermediate_field.adjoin F ↑s = ⊤,
   { apply intermediate_field.to_subalgebra_injective,

src/field_theory/krull_topology.lean

@@ -88,7 +88,7 @@ lemma intermediate_field.fixing_subgroup.bot {K L : Type*} [field K]
 begin
   ext f,
   refine ⟨λ _, subgroup.mem_top _, λ _, _⟩,
-  rintro ⟨x, hx⟩,
+  rintro ⟨x, hx : x ∈ (⊥ : intermediate_field K L)⟩,
   rw intermediate_field.mem_bot at hx,
   rcases hx with ⟨y, rfl⟩,
   exact f.commutes y,