Sizes of conjugacy classes

Two elementary facts about the carrier of a conjugacy class: the class of the identity is the singleton {1}, and every class of a finite monoid is nonempty.

Main results

• TauCeti.ConjClasses.carrier_mk_one: the class of 1 is {1}, with its counting form TauCeti.ConjClasses.card_carrier_mk_one.
• TauCeti.ConjClasses.card_carrier_pos: a conjugacy class of a finite monoid has positive size.

@[simp]

theorem TauCeti.ConjClasses.carrier_mk_one {G : Type u_1} [Monoid G] : (ConjClasses.mk 1).carrier = {1}

The conjugacy class of the identity is the singleton {1}: an element conjugate to 1 is 1.

theorem TauCeti.ConjClasses.card_carrier_mk_one {G : Type u_1} [Monoid G] : Nat.card ↑(ConjClasses.mk 1).carrier = 1

The identity conjugacy class has exactly one element. This is the weight that normalizes the identity column of a character table.

This is not a @[simp] lemma: Nat.card of a coerced set is not in simp normal form, Set.ncard being what Nat.card_coe_set_eq rewrites it to.

theorem TauCeti.ConjClasses.card_carrier_pos {G : Type u_1} [Monoid G] [Finite G] (C : ConjClasses G) : 0 < Nat.card ↑C.carrier

A conjugacy class of a finite monoid has positive size.