feat(src/group_theory/subgroup): add closure.submonoid.closure (#7328)

`subgroup.closure S` equals `submonoid.closure (S ∪ S⁻¹)`.

Author: riccardobrasca

src/group_theory/subgroup.lean

@@ -151,6 +151,9 @@ lemma mem_carrier {s : subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s := iff.
 @[simp, to_additive]
 lemma coe_to_submonoid (K : subgroup G) : (K.to_submonoid : set G) = K := rfl
 
+@[simp, to_additive]
+lemma mem_to_submonoid (K : subgroup G) (x : G) : x ∈ K.to_submonoid ↔ x ∈ K := iff.rfl
+
 @[to_additive]
 instance (K : subgroup G) [d : decidable_pred (∈ K)] [fintype G] : fintype K :=
 show fintype {g : G // g ∈ K}, from infer_instance
@@ -619,6 +622,52 @@ end
 lemma closure_singleton_one : closure ({1} : set G) = ⊥ :=
 by simp [eq_bot_iff_forall, mem_closure_singleton]
 
+@[simp, to_additive] lemma inv_subset_closure (S : set G) : S⁻¹ ⊆ closure S :=
+begin
+  intros s hs,
+  rw [set_like.mem_coe, ←subgroup.inv_mem_iff],
+  exact subset_closure (mem_inv.mp hs),
+end
+
+@[simp, to_additive] lemma closure_inv (S : set G) : closure S⁻¹ = closure S :=
+begin
+  refine le_antisymm ((subgroup.closure_le _).2 _) ((subgroup.closure_le _).2 _),
+  { exact inv_subset_closure S },
+  { simpa only [set.inv_inv] using inv_subset_closure S⁻¹ },
+end
+
+@[to_additive]
+lemma closure_to_submonoid (S : set G) :
+  (closure S).to_submonoid = submonoid.closure (S ∪ S⁻¹) :=
+begin
+  refine le_antisymm _ (submonoid.closure_le.2 _),
+  { intros x hx,
+    refine closure_induction hx (λ x hx, submonoid.closure_mono (subset_union_left S S⁻¹)
+      (submonoid.subset_closure hx)) (submonoid.one_mem _) (λ x y hx hy, submonoid.mul_mem _ hx hy)
+      (λ x hx, _),
+    rwa [←submonoid.mem_closure_inv, set.union_inv, set.inv_inv, set.union_comm] },
+  { simp only [true_and, coe_to_submonoid, union_subset_iff, subset_closure, inv_subset_closure] }
+end
+
+/-- An induction principle for closure membership. If `p` holds for `1` and all elements of
+`k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of
+the closure of `k`. -/
+@[to_additive "An induction principle for additive closure membership. If `p` holds for `0` and all
+elements of `k` and their negation, and is preserved under addition, then `p` holds for all
+elements of the additive closure of `k`."]
+lemma closure_induction'' {p : G → Prop} {x} (h : x ∈ closure k)
+  (Hk : ∀ x ∈ k, p x) (Hk_inv : ∀ x ∈ k, p x⁻¹) (H1 : p 1)
+  (Hmul : ∀ x y, p x → p y → p (x * y)) : p x :=
+begin
+  rw [← mem_to_submonoid, closure_to_submonoid k] at h,
+  refine submonoid.closure_induction h (λ x hx, _) H1 (λ x y hx hy, Hmul x y hx hy),
+  { rw [mem_union, mem_inv] at hx,
+    cases hx with mem invmem,
+    { exact Hk x mem },
+    { rw [← inv_inv x],
+      exact Hk_inv _ invmem } },
+end
+
 @[to_additive]
 lemma mem_supr_of_directed {ι} [hι : nonempty ι] {K : ι → subgroup G} (hK : directed (≤) K)
   {x : G} :

src/group_theory/submonoid/membership.lean

@@ -7,6 +7,7 @@ Amelia Livingston, Yury Kudryashov
 import group_theory.submonoid.operations
 import algebra.big_operators.basic
 import algebra.free_monoid
+import algebra.pointwise
 
 /-!
 # Submonoids: membership criteria
@@ -315,6 +316,24 @@ lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ add_submonoid.closure
   a * b ∈ add_submonoid.closure (S : set R) :=
 S.mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb
 
+@[to_additive]
+lemma mem_closure_inv {G : Type*} [group G] (S : set G) (x : G) :
+  x ∈ submonoid.closure S⁻¹ ↔ x⁻¹ ∈ submonoid.closure S :=
+begin
+  suffices : ∀ (S : set G) (x : G), x ∈ submonoid.closure S⁻¹ → x⁻¹ ∈ submonoid.closure S,
+  { refine ⟨this S x, _⟩,
+    have := this S⁻¹ x⁻¹,
+    rw [inv_inv, set.inv_inv] at this,
+    exact this, },
+  intros S x hx,
+  refine submonoid.closure_induction hx (λ x hx, _) _ (λ x y hx hy, _),
+  { exact submonoid.subset_closure (set.mem_inv.mp hx), },
+  { rw one_inv,
+    exact submonoid.one_mem _ },
+  { rw mul_inv_rev x y,
+    exact submonoid.mul_mem _ hy hx },
+end
+
 end submonoid
 
 section mul_add