English
The submonoid fixing a set s under a monoid action consists of all elements of the monoid that act trivially on every element of s.
Русский
Подмоноид, фиксирующий множество s при действии моидного множества, состоит из всех элементов моидного множества, которые действуют тривиально на каждое x ∈ s.
LaTeX
$$$\\operatorname{FixingSubmonoid}(M,s) = \\{\\varphi \\in M \\mid \\forall x \\in s:\\; \\varphi \\cdot x = x\\}$$$
Lean4
/-- The submonoid fixing a set under a `MulAction`. -/
@[to_additive /-- The additive submonoid fixing a set under an `AddAction`. -/
]
def fixingSubmonoid (s : Set α) : Submonoid M
where
carrier := {ϕ : M | ∀ x : s, ϕ • (x : α) = x}
one_mem' _ := one_smul _ _
mul_mem' {x y} hx hy z := by rw [mul_smul, hy z, hx z]
