feat(algebra/add_submonoid_closure): the additive closure of a multip…

…licative submonoid is a subsemiring (#6860)

This file is extracted from PR #6705

src/group_theory/submonoid/membership.lean

@@ -276,6 +276,47 @@ attribute [to_additive add_submonoid.multiples_subset] submonoid.powers_subset
 
 end add_submonoid
 
+/-! Lemmas about additive closures of `submonoid`. -/
+namespace submonoid
+
+variables {R : Type*} [semiring R] (S : submonoid R) {a b : R}
+
+/-- The product of an element of the additive closure of a multiplicative submonoid `M`
+and an element of `M` is contained in the additive closure of `M`. -/
+lemma mul_right_mem_add_closure
+  (ha : a ∈ add_submonoid.closure (S : set R)) (hb : b ∈ S) :
+  a * b ∈ add_submonoid.closure (S : set R) :=
+begin
+  revert b,
+  refine add_submonoid.closure_induction ha _ _ _; clear ha a,
+  { exact λ r hr b hb, add_submonoid.mem_closure.mpr (λ y hy, hy (S.mul_mem hr hb)) },
+  { exact λ b hb, by simp only [zero_mul, (add_submonoid.closure (S : set R)).zero_mem] },
+  { simp_rw add_mul,
+    exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
+end
+
+/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
+additive closure of `M`. -/
+lemma mul_mem_add_closure
+  (ha : a ∈ add_submonoid.closure (S : set R)) (hb : b ∈ add_submonoid.closure (S : set R)) :
+  a * b ∈ add_submonoid.closure (S : set R) :=
+begin
+  revert a,
+  refine add_submonoid.closure_induction hb _ _ _; clear hb b,
+  { exact λ r hr b hb, S.mul_right_mem_add_closure hb hr },
+  { exact λ b hb, by simp only [mul_zero, (add_submonoid.closure (S : set R)).zero_mem] },
+  { simp_rw mul_add,
+    exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
+end
+
+/-- The product of an element of `S` and an element of the additive closure of a multiplicative
+submonoid `S` is contained in the additive closure of `S`. -/
+lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ add_submonoid.closure (S : set R)) :
+  a * b ∈ add_submonoid.closure (S : set R) :=
+S.mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb
+
+end submonoid
+
 section mul_add
 
 lemma of_mul_image_powers_eq_multiples_of_mul [monoid M] {x : M} :

src/ring_theory/subsemiring.lean

@@ -21,6 +21,7 @@ open_locale big_operators
 universes u v w
 
 variables {R : Type u} {S : Type v} {T : Type w} [semiring R] [semiring S] [semiring T]
+  (M : submonoid R)
 
 set_option old_structure_cmd true
 
@@ -339,6 +340,66 @@ lemma closure_eq_of_le {s : set R} {t : subsemiring R} (h₁ : s ⊆ t) (h₂ :
   closure s = t :=
 le_antisymm (closure_le.2 h₁) h₂
 
+end subsemiring
+
+namespace submonoid
+
+/-- The additive closure of a submonoid is a subsemiring. -/
+def subsemiring_closure (M : submonoid R) : subsemiring R :=
+{ one_mem' := add_submonoid.mem_closure.mpr (λ y hy, hy M.one_mem),
+  mul_mem' := λ x y, M.mul_mem_add_closure,
+  ..add_submonoid.closure (M : set R)}
+
+lemma subsemiring_closure_coe :
+  (M.subsemiring_closure : set R) = add_submonoid.closure (M : set R) := rfl
+
+lemma subsemiring_closure_to_add_submonoid :
+  M.subsemiring_closure.to_add_submonoid = add_submonoid.closure (M : set R) := rfl
+
+/-- The `subsemiring` generated by a multiplicative submonoid coincides with the
+`subsemiring.closure` of the submonoid itself . -/
+lemma subsemiring_closure_eq_closure : M.subsemiring_closure = subsemiring.closure (M : set R) :=
+begin
+  ext,
+  refine ⟨λ hx, _, λ hx, (subsemiring.mem_closure.mp hx) M.subsemiring_closure (λ s sM, _)⟩;
+  rintros - ⟨H1, rfl⟩;
+  rintros - ⟨H2, rfl⟩,
+  { exact add_submonoid.mem_closure.mp hx H1.to_add_submonoid H2 },
+  { exact H2 sM }
+end
+
+end submonoid
+
+namespace subsemiring
+
+@[simp]
+lemma closure_submonoid_closure (s : set R) : closure ↑(submonoid.closure s) = closure s :=
+le_antisymm
+  (closure_le.mpr (λ y hy, (submonoid.mem_closure.mp hy) (closure s).to_submonoid subset_closure))
+  (closure_mono (submonoid.subset_closure))
+
+/-- The elements of the subsemiring closure of `M` are exactly the elements of the additive closure
+of a multiplicative submonoid `M`. -/
+lemma coe_closure_eq (s : set R) :
+  (closure s : set R) = add_submonoid.closure (submonoid.closure s : set R) :=
+by simp [← submonoid.subsemiring_closure_to_add_submonoid, submonoid.subsemiring_closure_eq_closure]
+
+lemma mem_closure_iff {s : set R} {x} :
+  x ∈ closure s ↔ x ∈ add_submonoid.closure (submonoid.closure s : set R) :=
+set.ext_iff.mp (coe_closure_eq s) x
+
+@[simp]
+lemma closure_add_submonoid_closure {s : set R} : closure ↑(add_submonoid.closure s) = closure s :=
+begin
+  ext x,
+  refine ⟨λ hx, _, λ hx, closure_mono add_submonoid.subset_closure hx⟩,
+  rintros - ⟨H, rfl⟩,
+  rintros - ⟨J, rfl⟩,
+  refine (add_submonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.to_add_submonoid (λ y hy, _),
+  refine (submonoid.mem_closure.mp hy) H.to_submonoid (λ z hz, _),
+  exact (add_submonoid.mem_closure.mp hz) H.to_add_submonoid (λ w hw, J hw),
+end
+
 /-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
 of `s`, and is preserved under addition and multiplication, then `p` holds for all elements
 of the closure of `s`. -/
@@ -348,24 +409,6 @@ lemma closure_induction {s : set R} {p : R → Prop} {x} (h : x ∈ closure s)
   (Hadd : ∀ x y, p x → p y → p (x + y)) (Hmul : ∀ x y, p x → p y → p (x * y)) : p x :=
 (@closure_le _ _ _ ⟨p, H1, Hmul, H0, Hadd⟩).2 Hs h
 
-lemma mem_closure_iff {s : set R} {x} :
-  x ∈ closure s ↔ x ∈ add_submonoid.closure (submonoid.closure s : set R) :=
-⟨λ h, closure_induction h (λ x hx, add_submonoid.subset_closure $ submonoid.subset_closure hx)
-  (add_submonoid.zero_mem _)
-  (add_submonoid.subset_closure $ submonoid.one_mem $ submonoid.closure s)
-  (λ _ _, add_submonoid.add_mem _)
-  (λ x y ihx ihy, add_submonoid.closure_induction ihy
-    (λ q hq, add_submonoid.closure_induction ihx
-      (λ p hp, add_submonoid.subset_closure $ (submonoid.closure s).mul_mem hp hq)
-      ((zero_mul q).symm ▸ add_submonoid.zero_mem _)
-      (λ p₁ p₂ ihp₁ ihp₂, (add_mul p₁ p₂ q).symm ▸ add_submonoid.add_mem _ ihp₁ ihp₂))
-    ((mul_zero x).symm ▸ add_submonoid.zero_mem _)
-    (λ q₁ q₂ ihq₁ ihq₂, (mul_add x q₁ q₂).symm ▸ add_submonoid.add_mem _ ihq₁ ihq₂)),
-λ h, add_submonoid.closure_induction h
-  (λ x hx, submonoid.closure_induction hx subset_closure (one_mem _) (λ _ _, mul_mem _))
-  (zero_mem _)
-  (λ _ _, add_mem _)⟩
-
 lemma mem_closure_iff_exists_list {s : set R} {x} : x ∈ closure s ↔
   ∃ L : list (list R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map list.prod).sum = x :=
 ⟨λ hx, add_submonoid.closure_induction (mem_closure_iff.1 hx)