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

Author: jcommelin

src/algebra/module.lean

@@ -23,11 +23,9 @@ 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 α β :=
+  [add_comm_monoid β] extends action α β :=
 (smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y)
 (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)
 
@@ -37,10 +35,10 @@ 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
+theorem mul_smul : (r * s) • x = r • s • x := action.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 one_smul : (1 : α) • x = x := action.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

src/group_theory/group_action.lean

@@ -13,13 +13,15 @@ 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)
+class 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
+namespace action
 
-variables (α) [monoid α] [monoid_action α β]
+variables (α) [monoid α] [action α β]
+
+attribute [simp] one_smul
 
 def orbit (b : β) := set.range (λ x : α, x • b)
 
@@ -32,7 +34,7 @@ iff.rfl
 ⟨x, rfl⟩
 
 @[simp] lemma mem_orbit_self (b : β) : b ∈ orbit α b :=
-⟨1, by simp [monoid_action.one]⟩
+⟨1, by simp [action.one_smul]⟩
 
 instance orbit_fintype (b : β) [fintype α] [decidable_eq β] :
   fintype (orbit α b) := set.fintype_range _
@@ -62,33 +64,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 γ β :=
+  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] }
-
-end monoid_action
+  one_smul := by simp [is_monoid_hom.map_one g, action.one_smul],
+  mul_smul := by simp [is_monoid_hom.map_mul g, action.mul_smul] }
 
-class group_action (α : Type u) (β : Type v) [group α] extends monoid_action α β
+end action
 
-namespace group_action
-variables [group α] [group_action α β]
+namespace action
+variables [group α] [action α β]
 
 section
-open monoid_action quotient_group
+open 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 [← action.mul_smul, inv_mul_self, action.one_smul],
+  right_inv := λ a, by rw [← action.mul_smul, mul_inv_self, 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, action.mul_smul x y a) }
 
 lemma bijective (g : α) : function.bijective (λ b : β, g • b) :=
 (to_perm α β g).bijective
@@ -97,25 +97,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 [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]}⟩⟩)⟩
+        action.mul_smul, hx]}⟩⟩)⟩
 
 instance (b : β) : is_subgroup (stabilizer α b) :=
-{ one_mem := monoid_action.one _ _,
+{ one_mem := 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 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] }
+    by rw [← hx, ← action.mul_smul, inv_mul_self, action.one_smul, hx] }
 
-variables (β)
 
-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 +127,35 @@ 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 $ (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 [← action.mul_smul, ← action.mul_smul,
+        H, inv_mul_self, 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 [action.mul_smul, ← H, ← action.mul_smul, inv_mul_self, action.one_smul]),
   λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩)
 
 end
 
-open quotient_group  monoid_action is_subgroup
+open quotient_group 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] : 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 → α)
+  action I (quotient H) :=
+action.comp_hom (quotient H) (subtype.val : I → α)
 
-end group_action
+end action

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 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 action
+variables [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 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.action (n : ℕ+) :
+  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 : _ = _ := @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 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 :=

src/ring_theory/algebra.lean

@@ -381,10 +381,10 @@ instance algebra : algebra R S :=
     by rw algebra.smul_def; exact @@is_submonoid.mul_mem _ S.2.2 (S.3 ⟨c, rfl⟩) x.2⟩,
   smul_add := λ c x y, subtype.eq $ by apply _inst_3.1.1.2,
   add_smul := λ c x y, subtype.eq $ by apply _inst_3.1.1.3,
-  mul_smul := λ c x y, subtype.eq $ by apply _inst_3.1.1.4,
-  one_smul := λ x, subtype.eq $ by apply _inst_3.1.1.5,
-  zero_smul := λ x, subtype.eq $ by apply _inst_3.1.1.6,
-  smul_zero := λ x, subtype.eq $ by apply _inst_3.1.1.7,
+  mul_smul := λ c x y, subtype.eq $ by simp [mul_smul],
+  one_smul := λ x, subtype.eq $ by simp [one_smul],
+  zero_smul := λ x, subtype.eq $ by apply _inst_3.1.1.4,
+  smul_zero := λ x, subtype.eq $ by apply _inst_3.1.1.5,
   to_fun := λ r, ⟨algebra_map A r, S.range_le ⟨r, rfl⟩⟩,
   hom := ⟨subtype.eq $ algebra.map_one R A, λ x y, subtype.eq $ algebra.map_mul A x y,
     λ x y, subtype.eq $ algebra.map_add A x y⟩,