refactor(*): unify group/monoid_action, make semimodule extend action (…

…#850)

* refactor(*): unify group/monoid_action, use standard names, make semimodule extend action

* Rename action to mul_action

* Generalize lemmas. Also, add class for multiplicative action on additive structure

* Add pi-instances

* Dirty hacky fix

* Remove #print and set_option pp.all

* clean up proof, avoid diamonds

* Fix some build issues

* Fix build

* Rename mul_action_add to distrib_mul_action

* Bump up the type class search depth in some places

src/algebra/module.lean

@@ -23,24 +23,16 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
   (where `r : α` and `x : β`) with some natural associativity and
   distributivity axioms similar to those on a ring. -/
 class semimodule (α : Type u) (β : Type v) [semiring α]
-  [add_comm_monoid β] extends has_scalar α β :=
-(smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y)
+  [add_comm_monoid β] extends distrib_mul_action α β :=
 (add_smul : ∀(r s : α) (x : β), (r + s) • x = r • x + s • x)
-(mul_smul : ∀(r s : α) (x : β), (r * s) • x = r • s • x)
-(one_smul : ∀x : β, (1 : α) • x = x)
 (zero_smul : ∀x : β, (0 : α) • x = 0)
-(smul_zero {} : ∀(r : α), r • (0 : β) = 0)
 
 section semimodule
 variables [R:semiring α] [add_comm_monoid β] [semimodule α β] (r s : α) (x y : β)
 include R
 
-theorem smul_add : r • (x + y) = r • x + r • y := semimodule.smul_add r x y
 theorem add_smul : (r + s) • x = r • x + s • x := semimodule.add_smul r s x
-theorem mul_smul : (r * s) • x = r • s • x := semimodule.mul_smul r s x
-@[simp] theorem smul_zero : r • (0 : β) = 0 := semimodule.smul_zero r
 variables (α)
-@[simp] theorem one_smul : (1 : α) • x = x := semimodule.one_smul α x
 @[simp] theorem zero_smul : (0 : α) • x = 0 := semimodule.zero_smul α x
 
 lemma smul_smul : r • s • x = (r * s) • x := (mul_smul _ _ _).symm
@@ -315,6 +307,8 @@ variables (p p' : submodule α β)
 variables {r : α} {x y : β}
 include R
 
+set_option class.instance_max_depth 36
+
 theorem smul_mem_iff (r0 : r ≠ 0) : r • x ∈ p ↔ x ∈ p :=
 ⟨λ h, by simpa [smul_smul, inv_mul_cancel r0] using p.smul_mem (r⁻¹) h,
  p.smul_mem r⟩

src/algebra/pi_instances.lean

@@ -61,16 +61,28 @@ instance add_comm_group     [∀ i, add_comm_group     $ f i] : add_comm_group
 instance ring               [∀ i, ring               $ f i] : ring               (Π i : I, f i) := by pi_instance
 instance comm_ring          [∀ i, comm_ring          $ f i] : comm_ring          (Π i : I, f i) := by pi_instance
 
-instance semimodule   (α) {r : semiring α}       [∀ i, add_comm_monoid $ f i] [∀ i, semimodule α $ f i]   : semimodule α (Π i : I, f i)   :=
+instance mul_action     (α) {m : monoid α}                                      [∀ i, mul_action α $ f i]     : mul_action α (Π i : I, f i) :=
 { smul := λ c f i, c • f i,
-  smul_add := λ c f g, funext $ λ i, smul_add _ _ _,
-  add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
   mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
-  one_smul := λ f, funext $ λ i, one_smul α _,
+  one_smul := λ f, funext $ λ i, one_smul α _ }
+
+instance distrib_mul_action (α) {m : monoid α}         [∀ i, add_monoid $ f i]      [∀ i, distrib_mul_action α $ f i] : distrib_mul_action α (Π i : I, f i) :=
+{ smul_zero := λ c, funext $ λ i, smul_zero _,
+  smul_add := λ c f g, funext $ λ i, smul_add _ _ _,
+  ..pi.mul_action _ }
+
+variables (I f)
+
+instance semimodule     (α) {r : semiring α}       [∀ i, add_comm_monoid $ f i] [∀ i, semimodule α $ f i]     : semimodule α (Π i : I, f i) :=
+{ add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
   zero_smul := λ f, funext $ λ i, zero_smul α _,
-  smul_zero := λ c, funext $ λ i, smul_zero _ }
-instance module       (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]       : module α (Π i : I, f i)       := {..pi.semimodule α}
-instance vector_space (α) {r : discrete_field α} [∀ i, add_comm_group $ f i]  [∀ i, vector_space α $ f i] : vector_space α (Π i : I, f i) := {..pi.module α}
+  ..pi.distrib_mul_action _ }
+
+variables {I f}
+
+instance module         (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]         : module α (Π i : I, f i)       := {..pi.semimodule I f α}
+
+instance vector_space   (α) {r : discrete_field α} [∀ i, add_comm_group $ f i]  [∀ i, vector_space α $ f i]   : vector_space α (Π i : I, f i) := {..pi.module α}
 
 instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] : left_cancel_semigroup (Π i : I, f i) :=
 by pi_instance

src/analysis/asymptotics.lean

@@ -589,6 +589,8 @@ scalar multiplication is multiplication.
 section
 variables {K : Type*} [normed_field K] [normed_space K β] [normed_group γ]
 
+set_option class.instance_max_depth 43
+
 theorem is_O_const_smul_left {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) (c : K) :
   is_O (λ x, c • f x) g l :=
 begin
@@ -628,6 +630,8 @@ end
 section
 variables {K : Type*} [normed_group β] [normed_field K] [normed_space K γ]
 
+set_option class.instance_max_depth 43
+
 theorem is_O_const_smul_right {f : α → β} {g : α → γ} {l : filter α} {c : K} (hc : c ≠ 0) :
   is_O f (λ x, c • g x) l ↔ is_O f g l :=
 begin
@@ -649,6 +653,8 @@ end
 section
 variables {K : Type*} [normed_field K] [normed_space K β] [normed_space K γ]
 
+set_option class.instance_max_depth 43
+
 theorem is_O_smul {k : α → K} {f : α → β} {g : α → γ} {l : filter α} (h : is_O f g l) :
   is_O (λ x, k x • f x) (λ x, k x • g x) l :=
 begin

src/analysis/normed_space/basic.lean

@@ -340,6 +340,8 @@ instance normed_field.to_normed_space : normed_space α α :=
 { dist_eq := normed_field.dist_eq,
   norm_smul := normed_field.norm_mul }
 
+set_option class.instance_max_depth 43
+
 lemma norm_smul [normed_space α β] (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
 normed_space.norm_smul s x
 

src/analysis/normed_space/bounded_linear_maps.lean

@@ -54,7 +54,7 @@ lemma zero : is_bounded_linear_map k (λ (x:E), (0:F)) :=
 lemma id : is_bounded_linear_map k (λ (x:E), x) :=
 linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
 
-set_option class.instance_max_depth 40
+set_option class.instance_max_depth 43
 lemma smul {f : E → F} (c : k) : is_bounded_linear_map k f → is_bounded_linear_map k (λ e, c • f e)
 | ⟨hf, ⟨M, hM, h⟩⟩ := (c • hf.mk' f).is_linear.with_bound (∥c∥ * M) $ assume x,
   calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
@@ -118,6 +118,8 @@ end
 
 end is_bounded_linear_map
 
+set_option class.instance_max_depth 34
+
 -- Next lemma is stated for real normed space but it would work as soon as the base field is an extension of ℝ
 lemma bounded_continuous_linear_map
   {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F] {L : E → F}

src/analysis/normed_space/deriv.lean

@@ -152,6 +152,8 @@ theorem has_fderiv_at_const (c : F) (x : E) :
   has_fderiv_at K (λ x, c) (λ y, 0) x :=
 has_fderiv_at_filter_const _ _ _
 
+set_option class.instance_max_depth 43
+
 theorem has_fderiv_at_filter_smul {f : E → F} {f' : E → F} {x : E} {L : filter E}
     (c : K) (h : has_fderiv_at_filter K f f' x L) :
   has_fderiv_at_filter K (λ x, c • f x) (λ x, c • f' x) x L :=
@@ -297,6 +299,8 @@ variables {E : Type*} [normed_space ℝ E]
 variables {F : Type*} [normed_space ℝ F]
 variables {G : Type*} [normed_space ℝ G]
 
+set_option class.instance_max_depth 34
+
 theorem has_fderiv_at_filter_real_equiv {f : E → F} {f' : E → F} {x : E} {L : filter E}
     (bf' : is_bounded_linear_map ℝ f') :
   tendsto (λ x' : E, ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) L (nhds 0) ↔

src/analysis/normed_space/operator_norm.lean

@@ -106,6 +106,8 @@ let ⟨c, _, _⟩ := (exists_bound A : ∃ c, c > 0 ∧ ∀ x : E, ∥ A x ∥ 
 have ∥A x∥ ∈ (image (norm ∘ A) {x | ∥x∥ ≤ 1}), from mem_image_of_mem _ $ le_of_eq ‹∥x∥ = 1›,
 le_cSup (norm_of_unit_ball_bdd_above A) ‹∥A x∥ ∈ _›
 
+set_option class.instance_max_depth 34
+
 /-- This is the fundamental property of the operator norm: ∥A x∥ ≤ ∥A∥ * ∥x∥. -/
 theorem bounded_by_operator_norm {A : L(E,F)} {x : E} : ∥A x∥ ≤ ∥A∥ * ∥x∥ :=
 have A 0 = 0, from (to_linear_map A).map_zero,

src/field_theory/mv_polynomial.lean

@@ -58,6 +58,7 @@ begin
   exact degrees_X _
 end
 
+set_option class.instance_max_depth 50
 lemma indicator_mem_restrict_degree (c : σ → α) :
   indicator c ∈ restrict_degree σ α (fintype.card α - 1) :=
 begin

src/group_theory/group_action.lean

@@ -13,13 +13,24 @@ class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)
 
 infixr ` • `:73 := has_scalar.smul
 
-class monoid_action (α : Type u) (β : Type v) [monoid α] extends has_scalar α β :=
-(one : ∀ b : β, (1 : α) • b = b)
-(mul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)
+/-- Typeclass for multiplictive actions by monoids. This generalizes group actions. -/
+class mul_action (α : Type u) (β : Type v) [monoid α] extends has_scalar α β :=
+(one_smul : ∀ b : β, (1 : α) • b = b)
+(mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)
 
-namespace monoid_action
+section
+variables [monoid α] [mul_action α β]
+
+theorem mul_smul (a₁ a₂ : α) (b : β) : (a₁ * a₂) • b = a₁ • a₂ • b := mul_action.mul_smul _ _ _
 
-variables (α) [monoid α] [monoid_action α β]
+variable (α)
+@[simp] theorem one_smul (b : β) : (1 : α) • b = b := mul_action.one_smul α _
+
+end
+
+namespace mul_action
+
+variables (α) [monoid α] [mul_action α β]
 
 def orbit (b : β) := set.range (λ x : α, x • b)
 
@@ -32,7 +43,7 @@ iff.rfl
 ⟨x, rfl⟩
 
 @[simp] lemma mem_orbit_self (b : β) : b ∈ orbit α b :=
-⟨1, by simp [monoid_action.one]⟩
+⟨1, by simp [mul_action.one_smul]⟩
 
 instance orbit_fintype (b : β) [fintype α] [decidable_eq β] :
   fintype (orbit α b) := set.fintype_range _
@@ -62,33 +73,31 @@ lemma mem_fixed_points' {b : β} : b ∈ fixed_points α β ↔
 λ h b, mem_stabilizer_iff.2 (h _ (mem_orbit _ _))⟩
 
 def comp_hom [monoid γ] (g : γ → α) [is_monoid_hom g] :
-  monoid_action γ β :=
+  mul_action γ β :=
 { smul := λ x b, (g x) • b,
-  one := by simp [is_monoid_hom.map_one g, monoid_action.one],
-  mul := by simp [is_monoid_hom.map_mul g, monoid_action.mul] }
+  one_smul := by simp [is_monoid_hom.map_one g, mul_action.one_smul],
+  mul_smul := by simp [is_monoid_hom.map_mul g, mul_action.mul_smul] }
 
-end monoid_action
+end mul_action
 
-class group_action (α : Type u) (β : Type v) [group α] extends monoid_action α β
-
-namespace group_action
-variables [group α] [group_action α β]
+namespace mul_action
+variables [group α] [mul_action α β]
 
 section
-open monoid_action quotient_group
+open mul_action quotient_group
 
 variables (α) (β)
 
 def to_perm (g : α) : equiv.perm β :=
 { to_fun := (•) g,
   inv_fun := (•) g⁻¹,
-  left_inv := λ a, by rw [← monoid_action.mul, inv_mul_self, monoid_action.one],
-  right_inv := λ a, by rw [← monoid_action.mul, mul_inv_self, monoid_action.one] }
+  left_inv := λ a, by rw [← mul_action.mul_smul, inv_mul_self, mul_action.one_smul],
+  right_inv := λ a, by rw [← mul_action.mul_smul, mul_inv_self, mul_action.one_smul] }
 
 variables {α} {β}
 
 instance : is_group_hom (to_perm α β) :=
-{ mul := λ x y, equiv.ext _ _ (λ a, monoid_action.mul x y a) }
+{ mul := λ x y, equiv.ext _ _ (λ a, mul_action.mul_smul x y a) }
 
 lemma bijective (g : α) : function.bijective (λ b : β, g • b) :=
 (to_perm α β g).bijective
@@ -97,25 +106,21 @@ lemma orbit_eq_iff {a b : β} :
    orbit α a = orbit α b ↔ a ∈ orbit α b:=
 ⟨λ h, h ▸ mem_orbit_self _,
 λ ⟨x, (hx : x • b = a)⟩, set.ext (λ c, ⟨λ ⟨y, (hy : y • a = c)⟩, ⟨y * x,
-  show (y * x) • b = c, by rwa [monoid_action.mul, hx]⟩,
+  show (y * x) • b = c, by rwa [mul_action.mul_smul, hx]⟩,
   λ ⟨y, (hy : y • b = c)⟩, ⟨y * x⁻¹,
     show (y * x⁻¹) • a = c, by
       conv {to_rhs, rw [← hy, ← mul_one y, ← inv_mul_self x, ← mul_assoc,
-        monoid_action.mul, hx]}⟩⟩)⟩
+        mul_action.mul_smul, hx]}⟩⟩)⟩
 
 instance (b : β) : is_subgroup (stabilizer α b) :=
-{ one_mem := monoid_action.one _ _,
+{ one_mem := mul_action.one_smul _ _,
   mul_mem := λ x y (hx : x • b = b) (hy : y • b = b),
-    show (x * y) • b = b, by rw monoid_action.mul; simp *,
+    show (x * y) • b = b, by rw mul_action.mul_smul; simp *,
   inv_mem := λ x (hx : x • b = b), show x⁻¹ • b = b,
-    by rw [← hx, ← monoid_action.mul, inv_mul_self, monoid_action.one, hx] }
-
-variables (β)
+    by rw [← hx, ← mul_action.mul_smul, inv_mul_self, mul_action.one_smul, hx] }
 
-def comp_hom [group γ] (g : γ → α) [is_group_hom g] :
-  group_action γ β := { ..monoid_action.comp_hom β g }
 
-variables (α)
+variables (α) (β)
 
 def orbit_rel : setoid β :=
 { r := λ a b, a ∈ orbit α b,
@@ -131,35 +136,51 @@ noncomputable def orbit_equiv_quotient_stabilizer (b : β) :
 equiv.symm (@equiv.of_bijective _ _
   (λ x : quotient (stabilizer α b), quotient.lift_on' x
     (λ x, (⟨x • b, mem_orbit _ _⟩ : orbit α b))
-    (λ g h (H : _ = _), subtype.eq $ (group_action.bijective (g⁻¹)).1
+    (λ g h (H : _ = _), subtype.eq $ (mul_action.bijective (g⁻¹)).1
       $ show g⁻¹ • (g • b) = g⁻¹ • (h • b),
-      by rw [← monoid_action.mul, ← monoid_action.mul,
-        H, inv_mul_self, monoid_action.one]))
+      by rw [← mul_action.mul_smul, ← mul_action.mul_smul,
+        H, inv_mul_self, mul_action.one_smul]))
 ⟨λ g h, quotient.induction_on₂' g h (λ g h H, quotient.sound' $
   have H : g • b = h • b := subtype.mk.inj H,
   show (g⁻¹ * h) • b = b,
-  by rw [monoid_action.mul, ← H, ← monoid_action.mul, inv_mul_self, monoid_action.one]),
+  by rw [mul_action.mul_smul, ← H, ← mul_action.mul_smul, inv_mul_self, mul_action.one_smul]),
   λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩)
 
 end
 
-open quotient_group  monoid_action is_subgroup
+open quotient_group mul_action is_subgroup
 
 def mul_left_cosets (H : set α) [is_subgroup H]
   (x : α) (y : quotient H) : quotient H :=
 quotient.lift_on' y (λ y, quotient_group.mk ((x : α) * y))
   (λ a b (hab : _ ∈ H), quotient_group.eq.2
     (by rwa [mul_inv_rev, ← mul_assoc, mul_assoc (a⁻¹), inv_mul_self, mul_one]))
 
-instance (H : set α) [is_subgroup H] : group_action α (quotient H) :=
+instance (H : set α) [is_subgroup H] : mul_action α (quotient H) :=
 { smul := mul_left_cosets H,
-  one := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2
+  one_smul := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2
     (by simp [is_submonoid.one_mem])),
-  mul := λ x y a, quotient.induction_on' a (λ a, quotient_group.eq.2
+  mul_smul := λ x y a, quotient.induction_on' a (λ a, quotient_group.eq.2
     (by simp [mul_inv_rev, is_submonoid.one_mem, mul_assoc])) }
 
 instance mul_left_cosets_comp_subtype_val (H I : set α) [is_subgroup H] [is_subgroup I] :
-  group_action I (quotient H) :=
-group_action.comp_hom (quotient H) (subtype.val : I → α)
+  mul_action I (quotient H) :=
+mul_action.comp_hom (quotient H) (subtype.val : I → α)
+
+end mul_action
+
+/-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
+class distrib_mul_action (α : Type u) (β : Type v) [monoid α] [add_monoid β] extends mul_action α β :=
+(smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y)
+(smul_zero {} : ∀(r : α), r • (0 : β) = 0)
+
+section
+variables [monoid α] [add_monoid β] [distrib_mul_action α β]
+
+theorem smul_add (a : α) (b₁ b₂ : β) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
+distrib_mul_action.smul_add _ _ _
 
-end group_action
+@[simp] theorem smul_zero (a : α) : a • (0 : β) = 0 :=
+distrib_mul_action.smul_zero _
+
+end

src/group_theory/sylow.lean

@@ -6,15 +6,15 @@ Authors: Chris Hughes
 import group_theory.group_action group_theory.quotient_group
 import group_theory.order_of_element data.zmod.basic algebra.pi_instances
 
-open equiv fintype finset group_action monoid_action function
+open equiv fintype finset mul_action function
 open equiv.perm is_subgroup list quotient_group
 universes u v w
 variables {G : Type u} {α : Type v} {β : Type w} [group G]
 
 local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable
 
-namespace group_action
-variables [group_action G α]
+namespace mul_action
+variables [mul_action G α]
 
 lemma mem_fixed_points_iff_card_orbit_eq_one {a : α}
   [fintype (orbit G a)] : a ∈ fixed_points G α ↔ card (orbit G a) = 1 :=
@@ -58,7 +58,7 @@ begin
 end
 ... = _ : by simp; refl
 
-end group_action
+end mul_action
 
 lemma quotient_group.card_preimage_mk [fintype G] (s : set G) [is_subgroup s]
   (t : set (quotient s)) : fintype.card (quotient_group.mk ⁻¹' t) =
@@ -98,11 +98,11 @@ def rotate_vectors_prod_eq_one (G : Type*) [group G] (n : ℕ+) (m : multiplicat
   (v : vectors_prod_eq_one G n) : vectors_prod_eq_one G n :=
 ⟨⟨v.1.to_list.rotate m.1, by simp⟩, prod_rotate_eq_one_of_prod_eq_one v.2 _⟩
 
-instance rotate_vectors_prod_eq_one.is_group_action (n : ℕ+) :
-  group_action (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
+instance rotate_vectors_prod_eq_one.mul_action (n : ℕ+) :
+  mul_action (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
 { smul := (rotate_vectors_prod_eq_one G n),
-  one := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list,
-  mul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $
+  one_smul := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list,
+  mul_smul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $
     show v.rotate ((a + b : zmod n).val) = list.rotate (list.rotate v (b.val)) (a.val),
     by rw [zmod.add_val, rotate_rotate, ← rotate_mod _ (b.1 + a.1), add_comm, hv₁] }
 
@@ -128,7 +128,7 @@ have hcard : card (vectors_prod_eq_one G (n + 1)) = card G ^ (n : ℕ),
     set.card_range_of_injective (mk_vector_prod_eq_one_inj _), card_vector],
 have hzmod : fintype.card (multiplicative (zmod p')) =
   (p' : ℕ) ^ 1 := (nat.pow_one p').symm ▸ card_fin _,
-have hmodeq : _ = _ := @group_action.card_modeq_card_fixed_points
+have hmodeq : _ = _ := @mul_action.card_modeq_card_fixed_points
   (multiplicative (zmod p')) (vectors_prod_eq_one G p') _ _ _ _ _ _ 1 hp hzmod,
 have hdvdcard : p ∣ fintype.card (vectors_prod_eq_one G (n + 1)) :=
   calc p ∣ card G ^ 1 : by rwa nat.pow_one
@@ -157,7 +157,7 @@ let ⟨a, ha⟩ := this in
   (hp.2 _ (order_of_dvd_of_pow_eq_one this)).resolve_left
     (λ h, ha1 (order_of_eq_one_iff.1 h))⟩
 
-open is_subgroup is_submonoid is_group_hom group_action
+open is_subgroup is_submonoid is_group_hom mul_action
 
 lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : set G} [is_subgroup H] [fintype H]
   {x : G} : (x : quotient H) ∈ fixed_points H (quotient H) ↔ x ∈ normalizer H :=