Submonoid generated by a set containing inverses

Stream: Is there code for X?

[Oliver Nash]

I don't suppose anyone has this lying around:

@[to_additive]
lemma Subgroup.closure_toSubmonoid_eq_of_inv_mem {G : Type*} [Group G]
    {s : Set G} (hs : ∀ x ∈ s, x⁻¹ ∈ s) :
    (Subgroup.closure s).toSubmonoid = Submonoid.closure s := by
  sorry

[Oliver Nash]

This became my last sorry so I just closed it myself. I'll post here to avoid someone duplicating the effort:

@[to_additive]
lemma Subgroup.closure_toSubmonoid_eq_of_inv_mem {G : Type*} [Group G]
    {s : Set G} (hs : ∀ x ∈ s, x⁻¹ ∈ s) :
    (Subgroup.closure s).toSubmonoid = Submonoid.closure s := by
  -- Maybe this should be a lemma in its own right?
  have (g : G) (hg : g ∈ Submonoid.closure s) : g⁻¹ ∈ Submonoid.closure s := by
    induction hg using Submonoid.closure_induction with
    | mem x hx => exact Submonoid.mem_closure.mpr fun _ h ↦ h (hs x hx)
    | one => simpa using Submonoid.one_mem _
    | mul x y hx hy hx' hy' =>
      rw [mul_inv_rev]
      exact Submonoid.mul_mem _ hy' hx'
  refine le_antisymm ?_ (le_closure_toSubmonoid s)
  let H : Subgroup G :=
    { toSubmonoid := Submonoid.closure s
      inv_mem' hg := this _ hg }
  change Subgroup.closure s ≤ H
  rw [Subgroup.closure_le]
  exact Submonoid.subset_closure

[Riccardo Brasca]

Looking at the API the canonical way of expressing hs is probably s⁻¹ ⊆ s, and the result maybe already there (or almost there)

[Riccardo Brasca]

import Mathlib

@[to_additive]
lemma Subgroup.closure_toSubmonoid_eq_of_inv_mem {G : Type*} [Group G]
    {s : Set G} (hs : s⁻¹ ⊆ s) :
    (Subgroup.closure s).toSubmonoid = Submonoid.closure s :=
  le_antisymm (Subgroup.closure_toSubmonoid s ▸ Submonoid.closure_mono (by simp [hs])) (by simp)

[Riccardo Brasca]

Even better we can extract a sublemma.

import Mathlib

@[simp]
lemma foo {G : Type*} [Group G] {s : Set G} (hs : s⁻¹ ⊆ s) : s⁻¹ = s :=
  le_antisymm hs (fun _ hg ↦ Set.mem_inv.1 <| hs (by simp [hg]))

lemma bar {G : Type*} [Group G] {s : Set G} (hs : s⁻¹ ⊆ s) :
    (Subgroup.closure s).toSubmonoid = Submonoid.closure s := by
  simp [Subgroup.closure_toSubmonoid, hs]

[Anatole Dedecker]

I don't understand why your foo is needed at all here, I would say docs#Subgroup.closure_toSubmonoid and docs#Set.union_eq_left are all you need.

[Riccardo Brasca]

Ah yes :D

[Oliver Nash]

Thanks guys, docs#Subgroup.closure_toSubmonoid was exactly what I was trying to find!