## Stream: new members

### Topic: How to use defining property of a submonoid?

#### Scott Carnahan (Nov 02 2023 at 22:54):

I'm trying to use set-wise stabilizers, but I got suck trying to used the submonoid I defined:

import Mathlib.GroupTheory.GroupAction.Defs

variable (M : Type u) {α : Type v} [Monoid M] [MulAction M α]

def setStabilizerMonoid (s : Set α) : Submonoid M :=
{
carrier := { g | ∀ (x : α), x ∈ s ↔ g • x ∈ s }
one_mem' := by
sorry -- not too hard
mul_mem' := by
sorry -- a little tricky
}

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
sorry -- My normal approach is useless here


#### Eric Wieser (Nov 02 2023 at 22:59):

Does this help?

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
have : ∀ (x : α), x ∈ s ↔ g • x ∈ s := g.prop
sorry


#### Eric Wieser (Nov 02 2023 at 22:59):

Note that docs#stabilizerSubmonoid already exists, but I assume you were writing it as an exercise

#### Eric Wieser (Nov 02 2023 at 23:00):

(also, it seems for your code to work in the latest mathlib, it needs import Mathlib.GroupTheory.GroupAction.Basic)

#### Eric Wieser (Nov 02 2023 at 23:08):

The have there is a bit magic; normally instead of pulling the statement of thin air, you'd write an API lemma:

def setStabilizerMonoid (s : Set α) : Submonoid M where
carrier := { g | ∀ (x : α), x ∈ s ↔ g • x ∈ s }
one_mem' := by
sorry -- not too hard
mul_mem' := by
sorry -- a little tricky

-- this is the API lemma, and you should write it as soon as possible after the def
@[simp]
theorem mem_setStabilizerMonoid_iff {s : Set α} {g : M} :
g ∈ setStabilizerMonoid M s ↔ ∀ (x : α), x ∈ s ↔ g • x ∈ s :=
Iff.rfl

theorem setStabilizerIff (s : Set α) (g : setStabilizerMonoid M s) (x : α) : x ∈ s ↔ g • x ∈ s := by
have := g.prop
rw [mem_setStabilizerMonoid_iff] at this
sorry


Last updated: Dec 20 2023 at 11:08 UTC