chore(algebra/module/linear_map): Derive linear_map from mul_action_h…

…om (#4888)


Note that this required some stuff about polynomials to move to cut import cycles.

src/algebra/group_action_hom.lean

@@ -255,27 +255,6 @@ 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
 
 section

src/algebra/group_ring_action.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau
 
 import group_theory.group_action
 import data.equiv.ring
-import data.polynomial.monic
+import deprecated.subring
 
 /-!
 # Group action on rings
@@ -122,58 +122,6 @@ nat.rec_on n (smul_one x) $ λ n ih, (smul_mul' x m (m ^ n)).trans $ congr_arg _
 
 end simp_lemmas
 
-namespace polynomial
-
-noncomputable instance [mul_semiring_action M S] : mul_semiring_action M (polynomial S) :=
-{ 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 coeff_map (mul_semiring_action.to_semiring_hom M S _) },
-    exact mul_smul m n (p.coeff i) },
-  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), }
-
-noncomputable instance [faithful_mul_semiring_action M S] :
-  faithful_mul_semiring_action M (polynomial S) :=
-{ eq_of_smul_eq_smul' := λ m₁ m₂ h, eq_of_smul_eq_smul S $ λ s, C_inj.1 $
-    calc  C (m₁ • s)
-        = m₁ • C s : (map_C $ mul_semiring_action.to_semiring_hom M S m₁).symm
-    ... = m₂ • C s : h (C s)
-    ... = C (m₂ • s) : map_C _,
-  .. polynomial.mul_semiring_action M S }
-
-variables [mul_semiring_action M S]
-
-@[simp] lemma coeff_smul' (m : M) (p : polynomial S) (n : ℕ) :
-  (m • p).coeff n = m • p.coeff n :=
-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
@@ -205,35 +153,9 @@ 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 : subgroup G) : 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]⟩)
-
-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]
-
 end comm_ring

src/algebra/module/linear_map.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
 -/
 import algebra.group.hom
 import algebra.module.basic
+import algebra.group_action_hom
 
 /-!
 # Linear maps and linear equivalences
@@ -49,14 +50,16 @@ the notation `M →ₗ[R] M₂`) are bundled versions of such maps. An unbundled
 the predicate `is_linear_map`, but it should be avoided most of the time. -/
 structure linear_map (R : Type u) (M : Type v) (M₂ : Type w)
   [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
-  extends add_hom M M₂ :=
-(map_smul' : ∀ (c : R) x, to_fun (c • x) = c • to_fun x)
+  extends add_hom M M₂, M →[R] M₂
 
 end
 
 /-- The `add_hom` underlying a `linear_map`. -/
 add_decl_doc linear_map.to_add_hom
 
+/-- The `mul_action_hom` underlying a `linear_map`. -/
+add_decl_doc linear_map.to_mul_action_hom
+
 infixr ` →ₗ `:25 := linear_map _
 notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := linear_map R M M₂
 

src/algebra/polynomial/group_ring_action.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import data.polynomial.monic
+import algebra.group_ring_action
+import algebra.group_action_hom
+
+/-!
+# Group action on rings applied to polynomials
+
+This file contains instances and definitions relating `mul_semiring_action` to `polynomial`.
+-/
+
+variables (M : Type*) [monoid M]
+
+namespace polynomial
+
+variables (R : Type*) [semiring R]
+
+noncomputable instance [mul_semiring_action M R] : mul_semiring_action M (polynomial R) :=
+{ smul := λ m, map $ mul_semiring_action.to_semiring_hom M R 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 coeff_map (mul_semiring_action.to_semiring_hom M R _) },
+    exact mul_smul m n (p.coeff i) },
+  smul_add := λ m p q, map_add (mul_semiring_action.to_semiring_hom M R m),
+  smul_zero := λ m, map_zero (mul_semiring_action.to_semiring_hom M R m),
+  smul_one := λ m, map_one (mul_semiring_action.to_semiring_hom M R m),
+  smul_mul := λ m p q, map_mul (mul_semiring_action.to_semiring_hom M R m), }
+
+noncomputable instance [faithful_mul_semiring_action M R] :
+  faithful_mul_semiring_action M (polynomial R) :=
+{ eq_of_smul_eq_smul' := λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ s, C_inj.1 $
+    calc  C (m₁ • s)
+        = m₁ • C s : (map_C $ mul_semiring_action.to_semiring_hom M R m₁).symm
+    ... = m₂ • C s : h (C s)
+    ... = C (m₂ • s) : map_C _,
+  .. polynomial.mul_semiring_action M R }
+
+variables {M R}
+
+variables [mul_semiring_action M R]
+
+@[simp] lemma coeff_smul' (m : M) (p : polynomial R) (n : ℕ) :
+  (m • p).coeff n = m • p.coeff n :=
+coeff_map _ _
+
+@[simp] lemma smul_C (m : M) (r : R) : m • C r = C (m • r) :=
+map_C _
+
+@[simp] lemma smul_X (m : M) : (m • X : polynomial R) = X :=
+map_X _
+
+variables (S : Type*) [comm_semiring S] [mul_semiring_action M S]
+
+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])
+
+variables (G : Type*) [group G]
+
+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
+
+section comm_ring
+
+variables (G : Type*) [group G] [fintype G]
+variables (R : Type*) [comm_ring R] [mul_semiring_action G R]
+open mul_action
+open_locale classical
+
+/-- 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]⟩)
+
+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]
+
+end comm_ring
+
+namespace mul_semiring_action_hom
+variables {M}
+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

src/field_theory/fixed.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import algebra.group_action_hom
+import algebra.polynomial.group_ring_action
 import deprecated.subfield
 import field_theory.normal
 import field_theory.separable

src/group_theory/sylow.lean

@@ -33,6 +33,9 @@ begin
       ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
 end
 
+-- This instance causes `exact card_quotient_dvd_card _` to timeout.
+local attribute [-instance] quotient_group.quotient.fintype
+
 lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points G α)]
   (p : ℕ) {n : ℕ} [hp : fact p.prime] (h : card G = p ^ n) :
   card α ≡ card (fixed_points G α) [MOD p] :=
@@ -51,7 +54,7 @@ begin
         simp only [quotient.eq']; congr)),
   { refine quotient.induction_on' b (λ b _ hb, _),
     have : card (orbit G b) ∣ p ^ n,
-    { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)];
+    { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)],
       exact card_quotient_dvd_card _ },
     rcases (nat.dvd_prime_pow hp).1 this with ⟨k, _, hk⟩,
     have hb' :¬ p ^ 1 ∣ p ^ k,
@@ -207,7 +210,7 @@ let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd in
 have hcard : card (quotient H) = s * p :=
   (nat.mul_left_inj (show card H > 0, from fintype.card_pos_iff.2
       ⟨⟨1, H.one_mem⟩⟩)).1
-    (by rwa [← card_eq_card_quotient_mul_card_subgroup, hH2, hs,
+    (by rwa [← card_eq_card_quotient_mul_card_subgroup H, hH2, hs,
       pow_succ', mul_assoc, mul_comm p]),
 have hm : s * p % p =
   card (quotient (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H)) % p :=