feat(field_theory/fixed): a field is normal over the fixed subfield u…

…nder a group action (#3520)

From my Galois theory repo.

src/algebra/group_action_hom.lean

@@ -255,4 +255,36 @@ ext $ λ x, by rw [comp_apply, id_apply]
 @[simp] lemma comp_id (f : R →+*[M] S) : f.comp (mul_semiring_action_hom.id M) = f :=
 ext $ λ x, by rw [comp_apply, id_apply]
 
+variables {P : Type*} [comm_semiring P] [mul_semiring_action M P]
+variables {Q : Type*} [comm_semiring Q] [mul_semiring_action M Q]
+open polynomial
+
+/-- An equivariant map induces an equivariant map on polynomials. -/
+protected noncomputable def polynomial (g : P →+*[M] Q) : polynomial P →+*[M] polynomial Q :=
+{ to_fun := map g,
+  map_smul' := λ m p, polynomial.induction_on p
+    (λ b, by rw [smul_C, map_C, coe_fn_coe, g.map_smul, map_C, coe_fn_coe, smul_C])
+    (λ p q ihp ihq, by rw [smul_add, polynomial.map_add, ihp, ihq, polynomial.map_add, smul_add])
+    (λ n b ih, by rw [smul_mul', smul_C, smul_pow, smul_X, polynomial.map_mul, map_C,
+        polynomial.map_pow, map_X, coe_fn_coe, g.map_smul, polynomial.map_mul, map_C,
+        polynomial.map_pow, map_X, smul_mul', smul_C, smul_pow, smul_X, coe_fn_coe]),
+  map_zero' := polynomial.map_zero g,
+  map_add' := λ p q, polynomial.map_add g,
+  map_one' := polynomial.map_one g,
+  map_mul' := λ p q, polynomial.map_mul g }
+
+@[simp] theorem coe_polynomial (g : P →+*[M] Q) : (g.polynomial : polynomial P → polynomial Q) = map g :=
+rfl
+
 end mul_semiring_action_hom
+
+variables (M) {R'} (U : set R') [is_subring U] [is_invariant_subring M U]
+
+/-- The canonical inclusion from an invariant subring. -/
+def is_invariant_subring.subtype_hom : U →+*[M] R' :=
+{ map_smul' := λ m s, rfl, .. is_subring.subtype U }
+
+@[simp] theorem is_invariant_subring.coe_subtype_hom : (is_invariant_subring.subtype_hom M U : U → R') = coe := rfl
+
+@[simp] theorem is_invariant_subring.coe_subtype_hom' :
+  (is_invariant_subring.subtype_hom M U : U →+* R') = is_subring.subtype U := rfl

src/algebra/group_ring_action.lean

@@ -8,29 +8,34 @@ Group action on rings.
 
 import group_theory.group_action
 import data.equiv.ring
-import data.polynomial.eval
+import data.polynomial.monic
 
 universes u v
-
-variables (M G : Type u) [monoid M] [group G]
-variables (A R S F : Type v) [add_monoid A] [semiring R] [comm_semiring S] [field F]
+open_locale big_operators
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
 
 /-- Typeclass for multiplicative actions by monoids on semirings. -/
-class mul_semiring_action extends distrib_mul_action M R :=
+class mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R]
+  extends distrib_mul_action M R :=
 (smul_one : ∀ (g : M), (g • 1 : R) = 1)
 (smul_mul : ∀ (g : M) (x y : R), g • (x * y) = (g • x) * (g • y))
 
 end prio
 
 export mul_semiring_action (smul_one)
 
+section semiring
+
+variables (M G : Type u) [monoid M] [group G]
+variables (A R S F : Type v) [add_monoid A] [semiring R] [comm_semiring S] [field F]
+
 variables {M R}
 lemma smul_mul' [mul_semiring_action M R] (g : M) (x y : R) :
   g • (x * y) = (g • x) * (g • y) :=
 mul_semiring_action.smul_mul g x y
+
 variables (M R)
 
 /-- Each element of the monoid defines a additive monoid homomorphism. -/
@@ -87,6 +92,21 @@ def mul_semiring_action.to_semiring_equiv [mul_semiring_action G R] (x : G) : R
 { .. distrib_mul_action.to_add_equiv G R x,
   .. mul_semiring_action.to_semiring_hom G R x }
 
+section prod
+variables [mul_semiring_action M R] [mul_semiring_action M S]
+
+lemma list.smul_prod (g : M) (L : list R) : g • L.prod = (L.map $ (•) g).prod :=
+monoid_hom.map_list_prod (mul_semiring_action.to_semiring_hom M R g : R →* R) L
+
+lemma multiset.smul_prod (g : M) (m : multiset S) : g • m.prod = (m.map $ (•) g).prod :=
+monoid_hom.map_multiset_prod (mul_semiring_action.to_semiring_hom M S g : S →* S) m
+
+lemma smul_prod (g : M) {ι : Type*} (f : ι → S) (s : finset ι) :
+  g • ∏ i in s, f i = ∏ i in s, g • f i :=
+monoid_hom.map_prod (mul_semiring_action.to_semiring_hom M S g : S →* S) f s
+
+end prod
+
 section simp_lemmas
 
 variables {M G A R}
@@ -102,25 +122,108 @@ nat.rec_on n (smul_one x) $ λ n ih, (smul_mul' x m (m ^ n)).trans $ congr_arg _
 
 end simp_lemmas
 
+namespace polynomial
+
 variables [mul_semiring_action M S]
 
 noncomputable instance : mul_semiring_action M (polynomial S) :=
-{ smul := λ m, polynomial.map $ mul_semiring_action.to_semiring_hom M S m,
-  one_smul := λ p, by { ext n, erw polynomial.coeff_map, exact one_smul M (p.coeff n) },
+{ smul := λ m, map $ mul_semiring_action.to_semiring_hom M S m,
+  one_smul := λ p, by { ext n, erw coeff_map, exact one_smul M (p.coeff n) },
   mul_smul := λ m n p, by { ext i,
-    iterate 3 { rw polynomial.coeff_map (mul_semiring_action.to_semiring_hom M S _) },
+    iterate 3 { rw coeff_map (mul_semiring_action.to_semiring_hom M S _) },
     exact mul_smul m n (p.coeff i) },
-  smul_add := λ m p q, polynomial.map_add (mul_semiring_action.to_semiring_hom M S m),
-  smul_zero := λ m, polynomial.map_zero (mul_semiring_action.to_semiring_hom M S m),
-  smul_one := λ m, polynomial.map_one (mul_semiring_action.to_semiring_hom M S m),
-  smul_mul := λ m p q, polynomial.map_mul (mul_semiring_action.to_semiring_hom M S m), }
+  smul_add := λ m p q, map_add (mul_semiring_action.to_semiring_hom M S m),
+  smul_zero := λ m, map_zero (mul_semiring_action.to_semiring_hom M S m),
+  smul_one := λ m, map_one (mul_semiring_action.to_semiring_hom M S m),
+  smul_mul := λ m p q, map_mul (mul_semiring_action.to_semiring_hom M S m), }
 
-@[simp] lemma polynomial.coeff_smul' (m : M) (p : polynomial S) (n : ℕ) :
+@[simp] lemma coeff_smul' (m : M) (p : polynomial S) (n : ℕ) :
   (m • p).coeff n = m • p.coeff n :=
-polynomial.coeff_map _ _
+coeff_map _ _
+
+@[simp] lemma smul_C (m : M) (r : S) : m • C r = C (m • r) :=
+map_C _
+
+@[simp] lemma smul_X (m : M) : (m • X : polynomial S) = X :=
+map_X _
+
+theorem smul_eval_smul (m : M) (f : polynomial S) (x : S) :
+  (m • f).eval (m • x) = m • f.eval x :=
+polynomial.induction_on f
+  (λ r, by rw [smul_C, eval_C, eval_C])
+  (λ f g ihf ihg, by rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add])
+  (λ n r ih, by rw [smul_mul', smul_pow, smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X,
+      eval_mul, eval_C, eval_pow, eval_X, smul_mul', smul_pow])
+
+theorem eval_smul' [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
+  f.eval (g • x) = g • (g⁻¹ • f).eval x :=
+by rw [← smul_eval_smul, mul_action.smul_inv_smul]
+
+theorem smul_eval [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
+  (g • f).eval x = g • f.eval (g⁻¹ • x) :=
+by rw [← smul_eval_smul, mul_action.smul_inv_smul]
+
+end polynomial
+
+end semiring
+
+section ring
+
+variables (M : Type u) [monoid M] {R : Type v} [ring R] [mul_semiring_action M R]
+variables (S : set R) [is_subring S]
+open mul_action
+
+set_option old_structure_cmd false
+
+/-- A subring invariant under the action. -/
+class is_invariant_subring : Prop :=
+(smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S)
+
+variables [is_invariant_subring M S]
+
+instance is_invariant_subring.to_mul_semiring_action : mul_semiring_action M S :=
+{ smul := λ m x, ⟨m • x, is_invariant_subring.smul_mem m x.2⟩,
+  one_smul := λ s, subtype.eq $ one_smul M s,
+  mul_smul := λ m₁ m₂ s, subtype.eq $ mul_smul m₁ m₂ s,
+  smul_add := λ m s₁ s₂, subtype.eq $ smul_add m s₁ s₂,
+  smul_zero := λ m, subtype.eq $ smul_zero m,
+  smul_one := λ m, subtype.eq $ smul_one m,
+  smul_mul := λ m s₁ s₂, subtype.eq $ smul_mul' m s₁ s₂ }
+
+end ring
+
+section comm_ring
+
+variables (G : Type u) [group G] [fintype G]
+variables (R : Type v) [comm_ring R] [mul_semiring_action G R]
+open mul_action
+open_locale classical
+
+noncomputable instance (s : set G) [is_subgroup s] : fintype (quotient_group.quotient s) :=
+quotient.fintype _
+
+/-- the product of `(X - g • x)` over distinct `g • x`. -/
+noncomputable def prod_X_sub_smul (x : R) : polynomial R :=
+(finset.univ : finset (quotient_group.quotient $ mul_action.stabilizer G x)).prod $
+λ g, polynomial.X - polynomial.C (of_quotient_stabilizer G x g)
+
+theorem prod_X_sub_smul.monic (x : R) : (prod_X_sub_smul G R x).monic :=
+polynomial.monic_prod_of_monic _ _ $ λ g _, polynomial.monic_X_sub_C _
+
+theorem prod_X_sub_smul.eval (x : R) : (prod_X_sub_smul G R x).eval x = 0 :=
+(finset.prod_hom _ (polynomial.eval x)).symm.trans $ finset.prod_eq_zero (finset.mem_univ $ quotient_group.mk 1) $
+by rw [of_quotient_stabilizer_mk, one_smul, polynomial.eval_sub, polynomial.eval_X, polynomial.eval_C, sub_self]
+
+theorem prod_X_sub_smul.smul (x : R) (g : G) :
+  g • prod_X_sub_smul G R x = prod_X_sub_smul G R x :=
+(smul_prod _ _ _ _ _).trans $ finset.prod_bij (λ g' _, g • g') (λ _ _, finset.mem_univ _)
+  (λ g' _, by rw [of_quotient_stabilizer_smul, smul_sub, polynomial.smul_X, polynomial.smul_C])
+  (λ _ _ _ _ H, (mul_action.bijective g).1 H)
+  (λ g' _, ⟨g⁻¹ • g', finset.mem_univ _, by rw [smul_smul, mul_inv_self, one_smul]⟩)
 
-@[simp] lemma polynomial.smul_C (m : M) (r : S) : m • polynomial.C r = polynomial.C (m • r) :=
-polynomial.map_C _
+theorem prod_X_sub_smul.coeff (x : R) (g : G) (n : ℕ) :
+  g • (prod_X_sub_smul G R x).coeff n =
+  (prod_X_sub_smul G R x).coeff n :=
+by rw [← polynomial.coeff_smul', prod_X_sub_smul.smul]
 
-@[simp] lemma polynomial.smul_X (m : M) : (m • polynomial.X : polynomial S) = polynomial.X :=
-polynomial.map_X _
+end comm_ring

src/algebra/module/basic.lean

@@ -144,14 +144,6 @@ by letI := H.to_has_scalar; exact
   smul_zero := λ r, (add_monoid_hom.mk' ((•) r) (H.smul_add r)).map_zero,
   ..H }
 
-variable [semimodule R M]
-
-@[simp] theorem smul_neg (r : R) (x : M) : r • (-x) = -(r • x) :=
-eq_neg_of_add_eq_zero (by simp [← smul_add])
-
-theorem smul_sub (r : R) (x y : M) : r • (x - y) = r • x - r • y :=
-by simp [smul_add, sub_eq_add_neg]; rw smul_neg
-
 end add_comm_group
 
 /--

src/data/polynomial/div.lean

@@ -486,6 +486,15 @@ lemma dvd_iff_mod_by_monic_eq_zero (hq : monic q) : p %ₘ q = 0 ↔ q ∣ p :=
       degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this;
     exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this))⟩
 
+theorem map_dvd_map [comm_ring S] (f : R →+* S) (hf : function.injective f) {x y : polynomial R}
+  (hx : x.monic) : x.map f ∣ y.map f ↔ x ∣ y :=
+begin
+  rw [← dvd_iff_mod_by_monic_eq_zero hx, ← dvd_iff_mod_by_monic_eq_zero (monic_map f hx),
+    ← map_mod_by_monic f hx],
+  exact ⟨λ H, map_injective f hf $ by rw [H, map_zero],
+  λ H, by rw [H, map_zero]⟩
+end
+
 @[simp] lemma mod_by_monic_one (p : polynomial R) : p %ₘ 1 = 0 :=
 (dvd_iff_mod_by_monic_eq_zero (by convert monic_one)).2 (one_dvd _)
 

src/data/polynomial/field_division.lean

@@ -53,6 +53,20 @@ have h₁ : (leading_coeff q)⁻¹ ≠ 0 :=
   inv_ne_zero (mt leading_coeff_eq_zero.1 h),
 by rw [degree_mul, degree_C h₁, add_zero]
 
+theorem irreducible_of_monic {p : polynomial R} (hp1 : p.monic) (hp2 : p ≠ 1) :
+  irreducible p ↔ (∀ f g : polynomial R, f.monic → g.monic → f * g = p → f = 1 ∨ g = 1) :=
+⟨λ hp3 f g hf hg hfg, or.cases_on (hp3.2 f g hfg.symm)
+  (assume huf : is_unit f, or.inl $ eq_one_of_is_unit_of_monic hf huf)
+  (assume hug : is_unit g, or.inr $ eq_one_of_is_unit_of_monic hg hug),
+λ hp3, ⟨mt (eq_one_of_is_unit_of_monic hp1) hp2, λ f g hp,
+have hf : f ≠ 0, from λ hf, by { rw [hp, hf, zero_mul] at hp1, exact not_monic_zero hp1 },
+have hg : g ≠ 0, from λ hg, by { rw [hp, hg, mul_zero] at hp1, exact not_monic_zero hp1 },
+or.imp (λ hf, is_unit_of_mul_eq_one _ _ hf) (λ hg, is_unit_of_mul_eq_one _ _ hg) $
+hp3 (f * C f.leading_coeff⁻¹) (g * C g.leading_coeff⁻¹)
+  (monic_mul_leading_coeff_inv hf) (monic_mul_leading_coeff_inv hg) $
+by rw [mul_assoc, mul_left_comm _ g, ← mul_assoc, ← C_mul, ← mul_inv', ← leading_coeff_mul,
+    ← hp, monic.def.1 hp1, inv_one, C_1, mul_one]⟩⟩
+
 /-- Division of polynomials. See polynomial.div_by_monic for more details.-/
 def div (p q : polynomial R) :=
 C (leading_coeff q)⁻¹ * (p /ₘ (q * C (leading_coeff q)⁻¹))
@@ -232,6 +246,13 @@ by rw dif_neg hp0; exact monic_mul_leading_coeff_inv hp0
 lemma coe_norm_unit (hp : p ≠ 0) : (norm_unit p : polynomial R) = C p.leading_coeff⁻¹ :=
 show ↑(dite _ _ _) = C p.leading_coeff⁻¹, by rw dif_neg hp; refl
 
+theorem map_dvd_map' [field k] (f : R →+* k) {x y : polynomial R} : x.map f ∣ y.map f ↔ x ∣ y :=
+if H : x = 0 then by rw [H, map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero]
+else by rw [← normalize_dvd_iff, ← @normalize_dvd_iff (polynomial R), normalize, normalize,
+    coe_norm_unit H, coe_norm_unit (mt (map_eq_zero _).1 H),
+    leading_coeff_map, ← f.map_inv, ← map_C, ← map_mul,
+    map_dvd_map _ f.injective (monic_mul_leading_coeff_inv H)]
+
 @[simp] lemma degree_normalize : degree (normalize p) = degree p :=
 if hp0 : p = 0 then by simp [hp0]
 else by rw [normalize, degree_mul, degree_eq_zero_of_is_unit (is_unit_unit _), add_zero]

src/data/polynomial/ring_division.lean

@@ -311,6 +311,15 @@ lemma irreducible_of_degree_eq_one_of_monic (hp1 : degree p = 1)
   (hm : monic p) : irreducible p :=
 irreducible_of_prime (prime_of_degree_eq_one_of_monic hp1 hm)
 
+theorem eq_of_monic_of_associated (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
+begin
+  obtain ⟨u, hu⟩ := hpq,
+  unfold monic at hp hq,
+  rw eq_C_of_degree_le_zero (le_of_eq $ degree_coe_units _) at hu,
+  rw [← hu, leading_coeff_mul, hp, one_mul, leading_coeff_C] at hq,
+  rwa [hq, C_1, mul_one] at hu
+end
+
 end integral_domain