feat(algebra/graded_monoid): add lemmas about power and product membe…

…rship (#10627)

This adds:
* `set_like.graded_monoid.pow_mem`
* `set_like.graded_monoid.list_prod_map_mem`
* `set_like.graded_monoid.list_prod_of_fn_mem`

It doesn't bother to add the multiset and finset versions for now, because these are not imported at this point, and require the ring to be commutative.

src/algebra/graded_monoid.lean

@@ -3,10 +3,12 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import group_theory.group_action.defs
+import algebra.group.inj_surj
+import data.list.big_operators
+import data.list.range
 import data.set_like.basic
 import data.sigma.basic
-import algebra.group.inj_surj
+import group_theory.group_action.defs
 
 /-!
 # Additively-graded multiplicative structures
@@ -336,6 +338,36 @@ instance set_like.ghas_mul {S : Type*} [set_like S R] [has_mul R] [has_add ι] (
 class set_like.graded_monoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   (A : ι → S) extends set_like.has_graded_one A, set_like.has_graded_mul A : Prop
 
+namespace set_like.graded_monoid
+variables {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
+variables {A : ι → S} [set_like.graded_monoid A]
+
+lemma pow_mem (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i) :=
+begin
+  induction n,
+  { rw [pow_zero, zero_nsmul], exact one_mem },
+  { rw [pow_succ', succ_nsmul'], exact mul_mem n_ih h },
+end
+
+lemma list_prod_map_mem {ι'} (l : list ι') (i : ι' → ι) (r : ι' → R) (h : ∀ j ∈ l, r j ∈ A (i j)) :
+  (l.map r).prod ∈ A (l.map i).sum :=
+begin
+  induction l,
+  { rw [list.map_nil, list.map_nil, list.prod_nil, list.sum_nil],
+    exact one_mem },
+  { rw [list.map_cons, list.map_cons, list.prod_cons, list.sum_cons],
+    exact mul_mem (h _ $ list.mem_cons_self _ _) (l_ih $ λ j hj, h _ $ list.mem_cons_of_mem _ hj) },
+end
+
+lemma list_prod_of_fn_mem {n} (i : fin n → ι) (r : fin n → R) (h : ∀ j, r j ∈ A (i j)) :
+  (list.of_fn r).prod ∈ A (list.of_fn i).sum :=
+begin
+  rw [list.of_fn_eq_map, list.of_fn_eq_map],
+  exact list_prod_map_mem _ _ _ (λ _ _, h _),
+end
+
+end set_like.graded_monoid
+
 /-- Build a `gmonoid` instance for a collection of subobjects. -/
 instance set_like.gmonoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S)
   [set_like.graded_monoid A] :
@@ -344,17 +376,13 @@ instance set_like.gmonoid {S : Type*} [set_like S R] [monoid R] [add_monoid ι]
   mul_one := λ ⟨i, a, h⟩, sigma.subtype_ext (add_zero _) (mul_one _),
   mul_assoc := λ ⟨i, a, ha⟩ ⟨j, b, hb⟩ ⟨k, c, hc⟩,
     sigma.subtype_ext (add_assoc _ _ _) (mul_assoc _ _ _),
-  gnpow := λ n i a, ⟨a ^ n, begin
-    induction n,
-    { rw [pow_zero, zero_nsmul], exact set_like.has_graded_one.one_mem },
-    { rw [pow_succ', succ_nsmul'], exact set_like.has_graded_mul.mul_mem n_ih a.prop },
-  end⟩,
+  gnpow := λ n i a, ⟨a ^ n, set_like.graded_monoid.pow_mem n a.prop⟩,
   gnpow_zero' := λ n, sigma.subtype_ext (zero_nsmul _) (pow_zero _),
   gnpow_succ' := λ n a, sigma.subtype_ext (succ_nsmul _ _) (pow_succ _ _),
   ..set_like.ghas_one A,
   ..set_like.ghas_mul A }
 
-@[simp] lemma set_like.coe_gpow {S : Type*} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S)
+@[simp] lemma set_like.coe_gnpow {S : Type*} [set_like S R] [monoid R] [add_monoid ι] (A : ι → S)
   [set_like.graded_monoid A] {i : ι} (x : A i) (n : ℕ) :
     ↑(@graded_monoid.gmonoid.gnpow _ (λ i, A i) _ _ n _ x) = (x ^ n : R) := rfl