feat(group_theory/submonoid/pointwise): add the pointwise monoid stru…

…cture on `add_submonoid` (#15052)

This also adds some missing lemmas about powers of submodules.

src/algebra/algebra/operations.lean

@@ -67,6 +67,13 @@ instance : has_one (submodule R A) :=
 theorem one_eq_range :
   (1 : submodule R A) = (algebra.linear_map R A).range := rfl
 
+lemma le_one_to_add_submonoid :
+  1 ≤ (1 : submodule R A).to_add_submonoid :=
+begin
+  rintros x ⟨n, rfl⟩,
+  exact ⟨n, map_nat_cast (algebra_map R A) n⟩,
+end
+
 lemma algebra_map_mem (r : R) : algebra_map R A r ∈ (1 : submodule R A) :=
 linear_map.mem_range_self _ _
 
@@ -83,6 +90,8 @@ begin
   simp only [mem_one, mem_span_singleton, algebra.smul_def, mul_one]
 end
 
+theorem one_eq_span_one_set : (1 : submodule R A) = span R 1 := one_eq_span
+
 theorem one_le : (1 : submodule R A) ≤ P ↔ (1 : A) ∈ P :=
 by simpa only [one_eq_span, span_le, set.singleton_subset_iff]
 
@@ -115,7 +124,8 @@ theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := apply_mem
 
 theorem mul_le : M * N ≤ P ↔ ∀ (m ∈ M) (n ∈ N), m * n ∈ P := map₂_le
 
-lemma mul_to_add_submonoid : (M * N).to_add_submonoid = M.to_add_submonoid * N.to_add_submonoid :=
+lemma mul_to_add_submonoid (M N : submodule R A) :
+  (M * N).to_add_submonoid = M.to_add_submonoid * N.to_add_submonoid :=
 begin
   dsimp [has_mul.mul],
   simp_rw [←algebra.lmul_left_to_add_monoid_hom R, algebra.lmul_left, ←map_to_add_submonoid _ N,
@@ -148,17 +158,7 @@ variables R
 theorem span_mul_span : span R S * span R T = span R (S * T) := map₂_span_span _ _ _ _
 variables {R}
 
-
 variables (M N P Q)
-protected theorem mul_assoc : (M * N) * P = M * (N * P) :=
-le_antisymm (mul_le.2 $ λ mn hmn p hp,
-  suffices M * N ≤ (M * (N * P)).comap (algebra.lmul_right R p), from this hmn,
-  mul_le.2 $ λ m hm n hn, show m * n * p ∈ M * (N * P), from
-  (mul_assoc m n p).symm ▸ mul_mem_mul hm (mul_mem_mul hn hp))
-(mul_le.2 $ λ m hm np hnp,
-  suffices N * P ≤ (M * N * P).comap (algebra.lmul_left R m), from this hnp,
-  mul_le.2 $ λ n hn p hp, show m * (n * p) ∈ M * N * P, from
-  mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp)
 
 @[simp] theorem mul_bot : M * ⊥ = ⊥ := map₂_bot_right _ _
 
@@ -253,24 +253,7 @@ open_locale pointwise
 This is available as an instance in the `pointwise` locale. -/
 protected def has_distrib_pointwise_neg {A} [ring A] [algebra R A] :
   has_distrib_neg (submodule R A) :=
-{ neg := has_neg.neg,
-  neg_mul := λ x y, begin
-    refine le_antisymm
-      (mul_le.2 $ λ m hm n hn, _)
-      ((submodule.neg_le _ _).2 $ mul_le.2 $ λ m hm n hn, _);
-    simp only [submodule.mem_neg, ←neg_mul] at *,
-    { exact mul_mem_mul hm hn,},
-    { exact mul_mem_mul (neg_mem_neg.2 hm) hn },
-  end,
-  mul_neg := λ x y, begin
-    refine le_antisymm
-      (mul_le.2 $ λ m hm n hn, _)
-      ((submodule.neg_le _ _).2 $ mul_le.2 $ λ m hm n hn, _);
-    simp only [submodule.mem_neg, ←mul_neg] at *,
-    { exact mul_mem_mul hm hn,},
-    { exact mul_mem_mul hm (neg_mem_neg.2 hn) },
-  end,
-  ..submodule.has_involutive_pointwise_neg }
+to_add_submonoid_injective.has_distrib_neg _ neg_to_add_submonoid mul_to_add_submonoid
 
 localized "attribute [instance] submodule.has_distrib_pointwise_neg" in pointwise
 
@@ -315,27 +298,47 @@ variables {M N P}
 instance : semiring (submodule R A) :=
 { one_mul       := submodule.one_mul,
   mul_one       := submodule.mul_one,
-  mul_assoc     := submodule.mul_assoc,
   zero_mul      := bot_mul,
   mul_zero      := mul_bot,
   left_distrib  := mul_sup,
   right_distrib := sup_mul,
+  ..to_add_submonoid_injective.semigroup _ (λ m n : submodule R A, mul_to_add_submonoid m n),
   ..add_monoid_with_one.unary,
   ..submodule.pointwise_add_comm_monoid,
   ..submodule.has_one,
   ..submodule.has_mul }
 
 variables (M)
 
+lemma span_pow (s : set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n)
+| 0 := by rw [pow_zero, pow_zero, one_eq_span_one_set]
+| (n + 1) := by rw [pow_succ, pow_succ, span_pow, span_mul_span]
+
+lemma pow_eq_span_pow_set (n : ℕ) : M ^ n = span R ((M : set A) ^ n) := by rw [←span_pow, span_eq]
+
 lemma pow_subset_pow {n : ℕ} : (↑M : set A)^n ⊆ ↑(M^n : submodule R A) :=
+(pow_eq_span_pow_set M n).symm ▸ subset_span
+
+lemma pow_mem_pow {x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n :=
+pow_subset_pow _ $ set.pow_mem_pow hx _
+
+lemma pow_to_add_submonoid {n : ℕ} (h : n ≠ 0) :
+  (M ^ n).to_add_submonoid = M.to_add_submonoid ^ n :=
 begin
   induction n with n ih,
-  { erw [pow_zero, pow_zero, set.singleton_subset_iff],
-    rw [set_like.mem_coe, ← one_le],
-    exact le_rfl },
-  { rw [pow_succ, pow_succ],
-    refine set.subset.trans (set.mul_subset_mul (subset.refl _) ih) _,
-    apply mul_subset_mul }
+  { exact (h rfl).elim },
+  { rw [pow_succ, pow_succ, mul_to_add_submonoid],
+    cases n,
+    { rw [pow_zero, pow_zero, mul_one, ←mul_to_add_submonoid, mul_one] },
+    { rw ih n.succ_ne_zero } },
+end
+
+lemma le_pow_to_add_submonoid {n : ℕ} :
+  M.to_add_submonoid ^ n ≤ (M ^ n).to_add_submonoid :=
+begin
+  obtain rfl | hn := decidable.eq_or_ne n 0,
+  { rw [pow_zero, pow_zero], exact le_one_to_add_submonoid },
+  { exact (pow_to_add_submonoid M hn).ge }
 end
 
 /-- Dependent version of `submodule.pow_induction_on_left`. -/

src/group_theory/submonoid/pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import data.set.pointwise
-import group_theory.submonoid.operations
+import group_theory.submonoid.membership
 
 /-! # Pointwise instances on `submonoid`s and `add_submonoid`s
 
@@ -22,8 +22,13 @@ which matches the action of `mul_action_set`.
 
 These are all available in the `pointwise` locale.
 
-Additionally, it provides `add_submonoid.has_mul`, which is available globally to match
-`submodule.has_mul`.
+Additionally, it provides various degrees of monoid structure:
+* `add_submonoid.has_one`
+* `add_submonoid.has_mul`
+* `add_submonoid.mul_one_class`
+* `add_submonoid.semigroup`
+* `add_submonoid.monoid`
+which is available globally to match the monoid structure implied by `submodule.semiring`.
 
 ## Implementation notes
 
@@ -304,16 +309,40 @@ subset_set_smul_iff₀ ha
 
 end group_with_zero
 
-open_locale pointwise
-
 end add_submonoid
 
-/-! ### Elementwise multiplication of two additive submonoids
+/-! ### Elementwise monoid structure of additive submonoids
 
 These definitions are a cut-down versions of the ones around `submodule.has_mul`, as that API is
 usually more useful. -/
 namespace add_submonoid
 
+open_locale pointwise
+
+section add_monoid_with_one
+variables [add_monoid_with_one R]
+
+instance : has_one (add_submonoid R) :=
+⟨(nat.cast_add_monoid_hom R).mrange⟩
+
+theorem one_eq_mrange :
+  (1 : add_submonoid R) = (nat.cast_add_monoid_hom R).mrange := rfl
+
+lemma nat_cast_mem_one (n : ℕ) : (n : R) ∈ (1 : add_submonoid R) := ⟨_, rfl⟩
+
+@[simp] lemma mem_one {x : R} : x ∈ (1 : add_submonoid R) ↔ ∃ n : ℕ, ↑n = x := iff.rfl
+
+theorem one_eq_closure : (1 : add_submonoid R) = closure {1} :=
+begin
+  simp only [closure_singleton_eq, mul_one, one_eq_mrange],
+  congr' 1 with n,
+  simp,
+end
+
+theorem one_eq_closure_one_set : (1 : add_submonoid R) = closure 1 := one_eq_closure
+end add_monoid_with_one
+
+section non_unital_non_assoc_semiring
 variables [non_unital_non_assoc_semiring R]
 
 /-- Multiplication of additive submonoids of a semiring R. The additive submonoid `S * T` is the
@@ -337,7 +366,6 @@ theorem mul_le {M N P : add_submonoid R} : M * N ≤ P ↔ ∀ (m ∈ M) (n ∈
 
 open_locale pointwise
 
-variables R
 -- this proof is copied directly from `submodule.span_mul_span`
 theorem closure_mul_closure (S T : set R) : closure S * closure T = closure (S * T) :=
 begin
@@ -353,7 +381,9 @@ begin
   { rw closure_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
     exact mul_mem_mul (subset_closure ha) (subset_closure hb) }
 end
-variables {R}
+
+lemma mul_eq_closure_mul_set (M N : add_submonoid R) : M * N = closure (M * N) :=
+by rw [←closure_mul_closure, closure_eq, closure_eq]
 
 @[simp] theorem mul_bot (S : add_submonoid R) : S * ⊥ = ⊥ :=
 eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [add_submonoid.mem_bot] at hn ⊢; rw [hn, mul_zero]
@@ -374,4 +404,85 @@ mul_le_mul (le_refl M) h
 lemma mul_subset_mul {M N : add_submonoid R} : (↑M : set R) * (↑N : set R) ⊆ (↑(M * N) : set R) :=
 by { rintros _ ⟨i, j, hi, hj, rfl⟩, exact mul_mem_mul hi hj }
 
+end non_unital_non_assoc_semiring
+
+section non_unital_non_assoc_ring
+variables [non_unital_non_assoc_ring R]
+
+/-- `add_submonoid.has_pointwise_neg` distributes over multiplication.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def has_distrib_neg : has_distrib_neg (add_submonoid R) :=
+{ neg := has_neg.neg,
+  neg_mul := λ x y, begin
+    refine le_antisymm
+      (mul_le.2 $ λ m hm n hn, _)
+      ((add_submonoid.neg_le _ _).2 $ mul_le.2 $ λ m hm n hn, _);
+    simp only [add_submonoid.mem_neg, ←neg_mul] at *,
+    { exact mul_mem_mul hm hn },
+    { exact mul_mem_mul (neg_mem_neg.2 hm) hn },
+  end,
+  mul_neg := λ x y, begin
+    refine le_antisymm
+      (mul_le.2 $ λ m hm n hn, _)
+      ((add_submonoid.neg_le _ _).2 $ mul_le.2 $ λ m hm n hn, _);
+    simp only [add_submonoid.mem_neg, ←mul_neg] at *,
+    { exact mul_mem_mul hm hn,},
+    { exact mul_mem_mul hm (neg_mem_neg.2 hn) },
+  end,
+  ..add_submonoid.has_involutive_neg }
+
+localized "attribute [instance] add_submonoid.has_distrib_neg" in pointwise
+
+end non_unital_non_assoc_ring
+
+section non_assoc_semiring
+variables [non_assoc_semiring R]
+
+instance : mul_one_class (add_submonoid R) :=
+{ one := 1,
+  mul := (*),
+  one_mul := λ M, by rw [one_eq_closure_one_set, ←closure_eq M, closure_mul_closure, one_mul],
+  mul_one := λ M, by rw [one_eq_closure_one_set, ←closure_eq M, closure_mul_closure, mul_one] }
+
+end non_assoc_semiring
+
+section non_unital_semiring
+variables [non_unital_semiring R]
+
+instance : semigroup (add_submonoid R) :=
+{ mul := (*),
+  mul_assoc := λ M N P,
+    le_antisymm (mul_le.2 $ λ mn hmn p hp,
+      suffices M * N ≤ (M * (N * P)).comap (add_monoid_hom.mul_right p), from this hmn,
+      mul_le.2 $ λ m hm n hn, show m * n * p ∈ M * (N * P), from
+      (mul_assoc m n p).symm ▸ mul_mem_mul hm (mul_mem_mul hn hp))
+    (mul_le.2 $ λ m hm np hnp,
+      suffices N * P ≤ (M * N * P).comap (add_monoid_hom.mul_left m), from this hnp,
+      mul_le.2 $ λ n hn p hp, show m * (n * p) ∈ M * N * P, from
+      mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp) }
+
+end non_unital_semiring
+
+section semiring
+variables [semiring R]
+
+instance : monoid (add_submonoid R) :=
+{ one := 1,
+  mul := (*),
+  ..add_submonoid.semigroup,
+  ..add_submonoid.mul_one_class }
+
+lemma closure_pow (s : set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
+| 0 := by rw [pow_zero, pow_zero, one_eq_closure_one_set]
+| (n + 1) := by rw [pow_succ, pow_succ, closure_pow, closure_mul_closure]
+
+lemma pow_eq_closure_pow_set (s : add_submonoid R) (n : ℕ) : s ^ n = closure ((s : set R) ^ n) :=
+by rw [←closure_pow, closure_eq]
+
+lemma pow_subset_pow {s : add_submonoid R} {n : ℕ} : (↑s : set R)^n ⊆ ↑(s^n) :=
+(pow_eq_closure_pow_set s n).symm ▸ subset_closure
+
+end semiring
+
 end add_submonoid