feat(algebra/graded_monoid,algebra/direct_sum/ring): provide lemmas a…

…bout powers in graded monoids (#9631)

The key results are `direct_sum.of_pow` and `graded_monoid.mk_pow`.

src/algebra/direct_sum/ring.lean

@@ -192,6 +192,11 @@ gcomm_semiring.of_add_submonoids (λ i, (carriers i).to_add_submonoid) one_mem m
 
 end shorthands
 
+lemma of_eq_of_graded_monoid_eq {A : ι → Type*} [Π (i : ι), add_comm_monoid (A i)]
+  {i j : ι} {a : A i} {b : A j} (h : graded_monoid.mk i a = graded_monoid.mk j b) :
+  direct_sum.of A i a = direct_sum.of A j b :=
+dfinsupp.single_eq_of_sigma_eq h
+
 variables (A : ι → Type*)
 
 /-! ### Instances for `⨁ i, A i` -/
@@ -264,7 +269,7 @@ begin
   apply add_hom_ext, intros i xi,
   unfold has_one.one,
   rw mul_hom_of_of,
-  exact dfinsupp.single_eq_of_sigma_eq (gsemiring.one_mul ⟨i, xi⟩),
+  exact of_eq_of_graded_monoid_eq (one_mul $ graded_monoid.mk i xi),
 end
 
 private lemma mul_one (x : ⨁ i, A i) : x * 1 = x :=
@@ -274,7 +279,7 @@ begin
   apply add_hom_ext, intros i xi,
   unfold has_one.one,
   rw [flip_apply, mul_hom_of_of],
-  exact dfinsupp.single_eq_of_sigma_eq (gsemiring.mul_one ⟨i, xi⟩),
+  exact of_eq_of_graded_monoid_eq (mul_one $ graded_monoid.mk i xi),
 end
 
 private lemma mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) :=
@@ -286,7 +291,7 @@ begin
   ext ai ax bi bx ci cx : 6,
   dsimp only [coe_comp, function.comp_app, comp_hom_apply_apply, flip_apply, flip_hom_apply],
   rw [mul_hom_of_of, mul_hom_of_of, mul_hom_of_of, mul_hom_of_of],
-  exact dfinsupp.single_eq_of_sigma_eq (gsemiring.mul_assoc ⟨ai, ax⟩ ⟨bi, bx⟩ ⟨ci, cx⟩),
+  exact of_eq_of_graded_monoid_eq (mul_assoc (graded_monoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩),
 end
 
 /-- The `semiring` structure derived from `gsemiring A`. -/
@@ -300,6 +305,15 @@ instance semiring : semiring (⨁ i, A i) := {
   mul_assoc := mul_assoc A,
   ..direct_sum.non_unital_non_assoc_semiring _, }
 
+lemma of_pow {i} (a : A i) (n : ℕ) :
+  of _ i a ^ n = of _ (n • i) (graded_monoid.gmonoid.gnpow _ a) :=
+begin
+  induction n with n,
+  { exact of_eq_of_graded_monoid_eq (pow_zero $ graded_monoid.mk _ a).symm, },
+  { rw [pow_succ, n_ih, of_mul_of],
+    exact of_eq_of_graded_monoid_eq (pow_succ (graded_monoid.mk _ a) n).symm, },
+end
+
 end semiring
 
 section comm_semiring
@@ -312,7 +326,7 @@ suffices mul_hom A = (mul_hom A).flip,
 begin
   apply add_hom_ext, intros ai ax, apply add_hom_ext, intros bi bx,
   rw [add_monoid_hom.flip_apply, mul_hom_of_of, mul_hom_of_of],
-  exact dfinsupp.single_eq_of_sigma_eq (gcomm_semiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩),
+  exact of_eq_of_graded_monoid_eq (gcomm_semiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩),
 end
 
 /-- The `comm_semiring` structure derived from `gcomm_semiring A`. -/
@@ -377,7 +391,7 @@ section mul
 variables [add_monoid ι] [Π i, add_comm_monoid (A i)] [gnon_unital_non_assoc_semiring A]
 
 @[simp] lemma of_zero_smul {i} (a : A 0) (b : A i) : of _ _ (a • b) = of _ _ a * of _ _ b :=
-(dfinsupp.single_eq_of_sigma_eq (graded_monoid.mk_zero_smul a b)).trans (of_mul_of _ _).symm
+(of_eq_of_graded_monoid_eq (graded_monoid.mk_zero_smul a b)).trans (of_mul_of _ _).symm
 
 @[simp] lemma of_zero_mul (a b : A 0) : of _ 0 (a * b) = of _ 0 a * of _ 0 b:=
 of_zero_smul A a b

src/algebra/graded_monoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import algebra.group.inj_surj
+import algebra.group_power.basic
 import data.set_like.basic
 import data.sigma.basic
 import group_theory.group_action.defs
@@ -101,18 +102,67 @@ lemma mk_mul_mk [has_add ι] [ghas_mul A] {i j} (a : A i) (b : A j) :
   mk i a * mk j b = mk (i + j) (ghas_mul.mul a b) :=
 rfl
 
-/-- A graded version of `monoid`. -/
+namespace gmonoid
+
+variables {A} [add_monoid ι] [ghas_mul A] [ghas_one A]
+
+/-- A default implementation of power on a graded monoid, like `npow_rec`.
+`gmonoid.gnpow` should be used instead. -/
+def gnpow_rec : Π (n : ℕ) {i}, A i → A (n • i)
+| 0 i a := cast (congr_arg A (zero_nsmul i).symm) ghas_one.one
+| (n + 1) i a := cast (congr_arg A (succ_nsmul i n).symm) (ghas_mul.mul a $ gnpow_rec _ a)
+
+@[simp] lemma gnpow_rec_zero (a : graded_monoid A) : graded_monoid.mk _ (gnpow_rec 0 a.snd) = 1 :=
+sigma.ext (zero_nsmul _) (heq_of_cast_eq _ rfl).symm
+
+/-- Tactic used to autofill `graded_monoid.gmonoid.gnpow_zero'` when the default
+`graded_monoid.gmonoid.gnpow_rec` is used. -/
+meta def apply_gnpow_rec_zero_tac : tactic unit := `[apply direct_sum.gmonoid.gnpow_rec_zero]
+
+@[simp] lemma gnpow_rec_succ (n : ℕ) (a : graded_monoid A) :
+  (graded_monoid.mk _ $ gnpow_rec n.succ a.snd) = a * ⟨_, gnpow_rec n a.snd⟩ :=
+sigma.ext (succ_nsmul _ _) (heq_of_cast_eq _ rfl).symm
+
+/-- Tactic used to autofill `graded_monoid.gmonoid.gnpow_succ'` when the default
+`graded_monoid.gmonoid.gnpow_rec` is used. -/
+meta def apply_gnpow_rec_succ_tac : tactic unit := `[apply direct_sum.gmonoid.gnpow_rec_succ]
+
+end gmonoid
+
+/-- A graded version of `monoid`.
+
+Like `monoid.npow`, this has an optional `gmonoid.gnpow` field to allow definitional control of
+natural powers of a graded monoid. -/
 class gmonoid [add_monoid ι]  extends ghas_mul A, ghas_one A :=
 (one_mul (a : graded_monoid A) : 1 * a = a)
 (mul_one (a : graded_monoid A) : a * 1 = a)
 (mul_assoc (a b c : graded_monoid A) : a * b * c = a * (b * c))
+(gnpow : Π (n : ℕ) {i}, A i → A (n • i) := gmonoid.gnpow_rec)
+(gnpow_zero' : Π (a : graded_monoid A), graded_monoid.mk _ (gnpow 0 a.snd) = 1
+  . gmonoid.apply_gnpow_rec_zero_tac)
+(gnpow_succ' : Π (n : ℕ) (a : graded_monoid A),
+  (graded_monoid.mk _ $ gnpow n.succ a.snd) = a * ⟨_, gnpow n a.snd⟩
+  . gmonoid.apply_gnpow_rec_succ_tac)
 
 /-- `gmonoid` implies a `monoid (graded_monoid A)`. -/
 instance gmonoid.to_monoid [add_monoid ι] [gmonoid A] :
   monoid (graded_monoid A) :=
 { one := (1), mul := (*),
+  npow := λ n a, graded_monoid.mk _ (gmonoid.gnpow n a.snd),
+  npow_zero' := λ a, gmonoid.gnpow_zero' a,
+  npow_succ' := λ n a, gmonoid.gnpow_succ' n a,
   one_mul := gmonoid.one_mul, mul_one := gmonoid.mul_one, mul_assoc := gmonoid.mul_assoc }
 
+lemma mk_pow [add_monoid ι] [gmonoid A] {i} (a : A i) (n : ℕ) :
+  mk i a ^ n = mk (n • i) (gmonoid.gnpow _ a) :=
+begin
+  induction n with n,
+  { rw [pow_zero],
+    exact (gmonoid.gnpow_zero' ⟨_, a⟩).symm, },
+  { rw [pow_succ, n_ih, mk_mul_mk],
+    exact (gmonoid.gnpow_succ' n ⟨_, a⟩).symm, },
+end
+
 /-- A graded version of `comm_monoid`. -/
 class gcomm_monoid [add_comm_monoid ι] extends gmonoid A :=
 (mul_comm (a : graded_monoid A) (b : graded_monoid A) : a * b = b * a)
@@ -244,6 +294,13 @@ def gmonoid.of_subobjects {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 one_mem },
+    { rw [pow_succ', succ_nsmul'], exact mul_mem ⟨_, n_ih⟩ a },
+  end⟩,
+  gnpow_zero' := λ n, sigma.subtype_ext (zero_nsmul _) (pow_zero _),
+  gnpow_succ' := λ n a, sigma.subtype_ext (succ_nsmul _ _) (pow_succ _ _),
   ..ghas_one.of_subobjects carriers one_mem,
   ..ghas_mul.of_subobjects carriers mul_mem }
 
@@ -278,10 +335,14 @@ instance has_mul.ghas_mul [has_add ι] [has_mul R] : graded_monoid.ghas_mul (λ
 
 /-- If all grades are the same type and themselves form a monoid, then there is a trivial grading
 structure. -/
+@[simps gnpow]
 instance monoid.gmonoid [add_monoid ι] [monoid R] : graded_monoid.gmonoid (λ i : ι, R) :=
 { one_mul := λ a, sigma.ext (zero_add _) (heq_of_eq (one_mul _)),
   mul_one := λ a, sigma.ext (add_zero _) (heq_of_eq (mul_one _)),
   mul_assoc := λ a b c, sigma.ext (add_assoc _ _ _) (heq_of_eq (mul_assoc _ _ _)),
+  gnpow := λ n i a, a ^ n,
+  gnpow_zero' := λ a, sigma.ext (zero_nsmul _) (heq_of_eq (monoid.npow_zero' _)),
+  gnpow_succ' := λ n ⟨i, a⟩, sigma.ext (succ_nsmul _ _) (heq_of_eq (monoid.npow_succ' _ _)),
   ..has_one.ghas_one ι,
   ..has_mul.ghas_mul ι }