English
Simplified equivalence: membership in noncenter is equivalent to nontriviality of the carrier.
Русский
Упрощённое эквивалентное выражение: принадлежность к noncenter эквивалентна не тривиальности носителя.
LaTeX
$$g ∈ noncenter G ↔ g.carrier.Nontrivial$$
Lean4
/-- Suppose `G` acts on `M` and `I` is a subgroup of `M`.
The inertia subgroup of `I` is the subgroup of `G` whose action is trivial mod `I`. -/
def inertia {M : Type*} [AddGroup M] (I : AddSubgroup M) (G : Type*) [Group G] [MulAction G M] : Subgroup G
where
carrier := {σ | ∀ x, σ • x - x ∈ I}
mul_mem' {a b} ha hb x := by simpa [mul_smul] using add_mem (ha (b • x)) (hb x)
one_mem' := by simp [zero_mem]
inv_mem' {a} ha x := by simpa using sub_mem_comm_iff.mp (ha (a⁻¹ • x))
