Centralizers and maximal commutative subgroups

Centralizers of a group of units are computed on the underlying monoid: a unit centralizes another exactly when their values commute. Mathlib has both halves — Subgroup.mem_centralizer_singleton_iff turns membership into an equation, and Commute.units_val_iff transports that equation between Mˣ and M — but not their combination, which is the form every concrete centralizer computation in a matrix group starts from.

Main results

• TauCeti.mem_centralizer_singleton_iff_commute_val: a unit lies in the centralizer of a unit g exactly when the two commute as elements of the monoid.
• Subgroup.eq_of_centralizer_eq_self_of_le_of_isMulCommutative: a self-centralizing subgroup is maximal among commutative subgroups.

theorem TauCeti.mem_centralizer_singleton_iff_commute_val {M : Type u_1} [Monoid M] {g h : Mˣ} : h ∈ Subgroup.centralizer {g} ↔ Commute ↑g ↑h

Membership in the centralizer of a unit g, read on the underlying monoid.

theorem Subgroup.eq_of_centralizer_eq_self_of_le_of_isMulCommutative {G : Type u_1} [Group G] {S H : Subgroup G} (hS : centralizer ↑S = S) [IsMulCommutative ↥H] (hle : S ≤ H) : H = S

A self-centralizing subgroup is maximal among commutative subgroups.