refactor(group_theory/group_action/big_operators): extract to a new f…

…ile (#13340)

`basic` is a misleading name, as `group_action.basic` imports a lot of things.
For now I'm not renaming it, but I've adding a skeletal docstring.

Splitting out the big operator lemmas allows access to big operators before modules and quotients.

This also performs a drive-by generalization of the typeclasses on `smul_cancel_of_non_zero_divisor`.

Authorship is from #1910

src/algebra/hom/group_action.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import group_theory.group_action.basic
 import algebra.group_ring_action
+import group_theory.group_action.defs
 
 /-!
 # Equivariant homomorphisms
@@ -106,14 +106,6 @@ variables {A B}
                ... = g (f (m • (g x))) : by rw f.map_smul
                ... = m • g x : by rw h₁, }
 
-variables {G} (H)
-
-/-- The canonical map to the left cosets. -/
-def to_quotient : G →[G] G ⧸ H :=
-⟨coe, λ g x, rfl⟩
-
-@[simp] lemma to_quotient_apply (g : G) : to_quotient H g = g := rfl
-
 end mul_action_hom
 
 /-- Equivariant additive monoid homomorphisms. -/

src/algebra/module/basic.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import algebra.big_operators.basic
 import algebra.smul_with_zero
+import group_theory.group_action.big_operators
 import group_theory.group_action.group
 import tactic.norm_num
 

src/data/dfinsupp/interval.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import data.finset.locally_finite
 import data.finset.pointwise
+import data.fintype.card
 import data.dfinsupp.order
 
 /-!

src/data/finset/finsupp.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import data.finset.pointwise
 import data.finsupp.indicator
+import data.fintype.card
 
 /-!
 # Finitely supported product of finsets

src/group_theory/group_action/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
+import algebra.hom.group_action
 import group_theory.group_action.defs
 import group_theory.group_action.group
 import group_theory.quotient_group
@@ -11,6 +12,18 @@ import data.fintype.card
 
 /-!
 # Basic properties of group actions
+
+This file primarily concerns itself with orbits, stabilizers, and other objects defined in terms of
+actions. Despite this file being called `basic`, low-level helper lemmas for algebraic manipulation
+of `•` belong elsewhere.
+
+## Main definitions
+
+* `mul_action.orbit`
+* `mul_action.fixed_points`
+* `mul_action.fixed_by`
+* `mul_action.stabilizer`
+
 -/
 
 universes u v w
@@ -335,6 +348,13 @@ end quotient_action
 
 open quotient_group
 
+/-- The canonical map to the left cosets. -/
+def _root_.mul_action_hom.to_quotient (H : subgroup α) : α →[α] α ⧸ H :=
+⟨coe, quotient.smul_coe H⟩
+
+@[simp] lemma _root_.mul_action_hom.to_quotient_apply (H : subgroup α) (g : α) :
+  mul_action_hom.to_quotient H g = g := rfl
+
 @[to_additive] instance mul_left_cosets_comp_subtype_val (H I : subgroup α) :
   mul_action I (α ⧸ H) :=
 mul_action.comp_hom (α ⧸ H) (subgroup.subtype I)
@@ -505,17 +525,11 @@ by rw [← fintype.card_prod, ← fintype.card_sigma,
 
 end mul_action
 
-section
-variables [monoid α] [add_monoid β] [distrib_mul_action α β]
-
-lemma list.smul_sum {r : α} {l : list β} :
-  r • l.sum = (l.map ((•) r)).sum :=
-(distrib_mul_action.to_add_monoid_hom β r).map_list_sum l
-
 /-- `smul` by a `k : M` over a ring is injective, if `k` is not a zero divisor.
 The general theory of such `k` is elaborated by `is_smul_regular`.
 The typeclass that restricts all terms of `M` to have this property is `no_zero_smul_divisors`. -/
-lemma smul_cancel_of_non_zero_divisor {M R : Type*} [monoid M] [ring R] [distrib_mul_action M R]
+lemma smul_cancel_of_non_zero_divisor {M R : Type*}
+  [monoid M] [non_unital_non_assoc_ring R] [distrib_mul_action M R]
   (k : M) (h : ∀ (x : R), k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :
   a = b :=
 begin
@@ -524,43 +538,6 @@ begin
   rw [smul_sub, h', sub_self]
 end
 
-end
-
-section
-variables [monoid α] [monoid β] [mul_distrib_mul_action α β]
-
-lemma list.smul_prod {r : α} {l : list β} :
-  r • l.prod = (l.map ((•) r)).prod :=
-(mul_distrib_mul_action.to_monoid_hom β r).map_list_prod l
-
-end
-
-section
-variables [monoid α] [add_comm_monoid β] [distrib_mul_action α β]
-
-lemma multiset.smul_sum {r : α} {s : multiset β} :
-  r • s.sum = (s.map ((•) r)).sum :=
-(distrib_mul_action.to_add_monoid_hom β r).map_multiset_sum s
-
-lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
-  r • ∑ x in s, f x = ∑ x in s, r • f x :=
-(distrib_mul_action.to_add_monoid_hom β r).map_sum f s
-
-end
-
-section
-variables [monoid α] [comm_monoid β] [mul_distrib_mul_action α β]
-
-lemma multiset.smul_prod {r : α} {s : multiset β} :
-  r • s.prod = (s.map ((•) r)).prod :=
-(mul_distrib_mul_action.to_monoid_hom β r).map_multiset_prod s
-
-lemma finset.smul_prod {r : α} {f : γ → β} {s : finset γ} :
-  r • ∏ x in s, f x = ∏ x in s, r • f x :=
-(mul_distrib_mul_action.to_monoid_hom β r).map_prod f s
-
-end
-
 namespace subgroup
 
 variables {G : Type*} [group G] (H : subgroup G)

src/group_theory/group_action/big_operators.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import algebra.big_operators.basic
+import data.finset.basic
+import data.multiset.basic
+import group_theory.group_action.defs
+
+/-!
+# Lemmas about group actions on big operators
+
+Note that analogous lemmas for `module`s like `finset.sum_smul` appear in other files.
+-/
+
+variables {α β γ : Type*}
+
+open_locale big_operators
+
+section
+variables [monoid α] [add_monoid β] [distrib_mul_action α β]
+
+lemma list.smul_sum {r : α} {l : list β} :
+  r • l.sum = (l.map ((•) r)).sum :=
+(distrib_mul_action.to_add_monoid_hom β r).map_list_sum l
+
+end
+
+section
+variables [monoid α] [monoid β] [mul_distrib_mul_action α β]
+
+lemma list.smul_prod {r : α} {l : list β} :
+  r • l.prod = (l.map ((•) r)).prod :=
+(mul_distrib_mul_action.to_monoid_hom β r).map_list_prod l
+
+end
+
+section
+variables [monoid α] [add_comm_monoid β] [distrib_mul_action α β]
+
+lemma multiset.smul_sum {r : α} {s : multiset β} :
+  r • s.sum = (s.map ((•) r)).sum :=
+(distrib_mul_action.to_add_monoid_hom β r).map_multiset_sum s
+
+lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
+  r • ∑ x in s, f x = ∑ x in s, r • f x :=
+(distrib_mul_action.to_add_monoid_hom β r).map_sum f s
+
+end
+
+section
+variables [monoid α] [comm_monoid β] [mul_distrib_mul_action α β]
+
+lemma multiset.smul_prod {r : α} {s : multiset β} :
+  r • s.prod = (s.map ((•) r)).prod :=
+(mul_distrib_mul_action.to_monoid_hom β r).map_multiset_prod s
+
+lemma finset.smul_prod {r : α} {f : γ → β} {s : finset γ} :
+  r • ∏ x in s, f x = ∏ x in s, r • f x :=
+(mul_distrib_mul_action.to_monoid_hom β r).map_prod f s
+
+end