Inversion and powers of conjugacy classes, and the size of a class

Inversion of a group is compatible with conjugacy: x and y are conjugate exactly when x⁻¹ and y⁻¹ are (TauCeti.isConj_inv_iff). So inversion descends to the conjugacy classes, where it is an involution, recorded here as an InvolutiveInv (ConjClasses G) instance; C⁻¹ is the class of the inverses of the members of C, and it has the same size as C. A class fixed by this involution is a real class (TauCeti.IsRealClass).

Powering likewise commutes with conjugation, so for a monoid M it too descends to the conjugacy classes: ConjClasses.pow C j, written C ^ j, is the class of the j-th powers of the members of C.

The other fact collected here is that the size of a conjugacy class is the index of the centralizer of any of its members, and so divides the order of the group: the orbit-stabilizer theorem for the conjugation action.

Main statements

• TauCeti.isConj_inv_iff: conjugacy is inherited by inverses in both directions.
• ConjClasses.inv_mk: the inverse of the class of g is the class of g⁻¹.
• TauCeti.IsRealClass: a class containing an element conjugate to its own inverse, with TauCeti.isRealClass_iff_inv_eq identifying it with being fixed by inversion.
• ConjClasses.ncard_carrier_inv and ConjClasses.card_carrier_inv: a conjugacy class and its inverse have the same size, in Set.ncard and in Nat.card form.
• ConjClasses.ncard_carrier_mk and ConjClasses.card_carrier_mk: the size of a conjugacy class is the index of the centralizer of any of its members, in Set.ncard and in Nat.card form.
• ConjClasses.ncard_carrier_mk_of_mem_center: the class of a central element is a single point.
• ConjClasses.card_carrier_mul_orderOf_dvd: the class size times the order of a member divides the order of the group, so the quotient below is an exact ratio.
• ConjClasses.card_div_card_carrier_mul_orderOf_pos: for a finite group that ratio is positive.
• ConjClasses.card_div_card_carrier_mul_orderOf_eq_card_centralizer_div_orderOf: that quotient equals the order of the centralizer divided by the order of the member.
• ConjClasses.one_div_orderOf_div_card_div_card_carrier_mul_orderOf: dividing 1 / orderOf σ by that quotient, in a semifield of characteristic zero, leaves #C / #G.
• ConjClasses.ncard_carrier_mk_eq_card_filter and ConjClasses.card_carrier_mk_eq_card_filter: the size of a conjugacy class as the cardinality of a Finset, which makes it computable.
• ConjClasses.card_carrier_dvd_card: the size of a conjugacy class divides the order of the group, with ConjClasses.card_carrier_cast_ne_zero the consequence that the size of a class is nonzero in any semiring where the group order is, and ConjClasses.card_carrier_div_card_ne_zero the nonvanishing of #C / #G for a finite group.
• ConjClasses.pow: the power operation itself, with C ^ j its notation.
• ConjClasses.mem_pow_iff: an element lies in C ^ j exactly when it is a j-th power of a member of C, with ConjClasses.mk_pow the computation rule.
• ConjClasses.pow_zero, ConjClasses.pow_one and ConjClasses.pow_mul: the identity and composition laws for that power.
• ConjClasses.map_mk: the computation rule for ConjClasses.map on representatives, with ConjClasses.map_pow the consequence that the power is natural in the monoid.
• MulEquiv.conjClassesEquiv: a multiplicative equivalence induces an equivalence of conjugacy classes, compatible with representatives, powers, inversion, composition, and multiplicative automorphisms acting on conjugacy classes.
• MulAut.smul_conjClasses_mk: an automorphism acts on a conjugacy class by mapping its representative; inner automorphisms fix every class.
• ConjClasses.mk_ne_mk_of_orderOf_ne: elements of different orders lie in different conjugacy classes.

The automorphism action lemmas are in the MulAut namespace, so dot notation applies: φ.smul_conjClasses_mk x computes on a representative, φ.smul_conjClasses_pow C n handles powers, and φ.smul_conjClasses_inv C handles inversion. The representative and power formulas apply to monoids; the inversion formula and triviality of the inner action require a group.

Implementation notes

The inversion is an instance rather than a plain function so that the notation C⁻¹, the involutivity lemma inv_inv and the reindexing equivalence Equiv.inv are all available for conjugacy classes. Powering is instead a named definition ConjClasses.pow with a Pow instance delegating to it, so that the roadmap's C.pow j and the notation C ^ j are the same function; the lemmas below are all stated in the ^ form. There is still no multiplication on ConjClasses M — Pow (ConjClasses M) ℕ is a bare power operation, not the npow field of a monoid structure, and none of the lemmas here presuppose one.

The power operation is developed for the Chebotarev roadmap (Chebotarev/README.md Layer 1, "consumed Frobenius classes and powers of conjugacy classes", whose Suggested.lean pins these signatures); its consumer there is the von Mangoldt fibre, which sums over the classes C ^ j. That is also why a pow_two_cyclicFour regression is kept: a group of exponent two has no proper nonidentity square, so it cannot separate a correct power operation from one that collapses to the identity. It is private, being a check on this development rather than reusable conjugacy-class API. This operation is not adapted from the Birkbeck–Brasca chebotarev-density development, which works with ConjClasses.mk and Subgroup.zpowers directly and never forms C ^ j.

The two arithmetic statements concern the quotient #G / (#C * orderOf σ). The first says the division is exact — #C is the index of the centralizer of σ, and orderOf σ divides that centralizer's order, so their product divides #G — and the second evaluates the quotient as the centralizer's order over orderOf σ. Neither asserts that either side counts anything; a caller wanting a cardinality interpretation must supply it.

theorem TauCeti.isConj_inv_iff {G : Type u_1} [Group G] {x y : G} : IsConj x⁻¹ y⁻¹ ↔ IsConj x y

Conjugacy is inherited by inverses in both directions.

Not @[simp]: Mathlib's isConj_iff is itself simp, so the left-hand side simplifies to ∃ c, c * x⁻¹ * c⁻¹ = y⁻¹ and the simp normal form linter rejects the pair.

@[instance_reducible]

instance TauCeti.instInvolutiveInvConjClasses {G : Type u_1} [Group G] : InvolutiveInv (ConjClasses G)

Inversion of conjugacy classes. Inversion of the group respects conjugacy, so it descends to the conjugacy classes; there it is an involution, because it is one on the group.

Equations

• TauCeti.instInvolutiveInvConjClasses = { inv := Quotient.lift (fun (g : G) => ConjClasses.mk g⁻¹) ⋯, inv_inv := ⋯ }

@[simp]

theorem ConjClasses.inv_mk {G : Type u_1} [Group G] (g : G) : (ConjClasses.mk g)⁻¹ = ConjClasses.mk g⁻¹

The inverse of the conjugacy class of g is the conjugacy class of g⁻¹.

@[simp]

theorem ConjClasses.inv_one {G : Type u_1} [Group G] : 1⁻¹ = 1

The class of the identity is its own inverse.

@[simp]

theorem ConjClasses.mem_carrier_inv_iff {G : Type u_1} [Group G] {C : ConjClasses G} {x : G} : x ∈ C⁻¹.carrier ↔ x⁻¹ ∈ C.carrier

An element lies in the inverse of a conjugacy class exactly when its inverse lies in the class.

@[simp]

theorem ConjClasses.ncard_carrier_inv {G : Type u_1} [Group G] (C : ConjClasses G) : C⁻¹.carrier.ncard = C.carrier.ncard

A conjugacy class and its inverse have the same size, inversion of the group restricting to a bijection between them.

This is the Set.ncard form, which is the simp normal form: Mathlib's Nat.card_coe_set_eq is itself simp. See ConjClasses.card_carrier_inv for the Nat.card form.

theorem ConjClasses.card_carrier_inv {G : Type u_1} [Group G] (C : ConjClasses G) : Nat.card ↑C⁻¹.carrier = Nat.card ↑C.carrier

A conjugacy class and its inverse have the same size, in Nat.card form.

Not @[simp]: Mathlib's Nat.card_coe_set_eq is itself simp, so the left-hand side simplifies to (C⁻¹).carrier.ncard and the simp normal form linter rejects the pair; that normalized form is ConjClasses.ncard_carrier_inv.

theorem ConjClasses.ncard_carrier_mk {G : Type u_1} [Group G] (g : G) : (ConjClasses.mk g).carrier.ncard = (Subgroup.centralizer {g}).index

The size of a conjugacy class is the index of the centralizer of any of its members. The class is the orbit of g under the conjugation action and the centralizer is the stabilizer, so this is the orbit-stabilizer theorem.

@[simp]

theorem ConjClasses.ncard_carrier_mk_of_mem_center {G : Type u_1} [Group G] {g : G} (hg : g ∈ Subgroup.center G) : (ConjClasses.mk g).carrier.ncard = 1

The conjugacy class of a central element is a single point: nothing moves it.

theorem ConjClasses.card_carrier_mk {G : Type u_1} [Group G] (g : G) : Nat.card ↑(ConjClasses.mk g).carrier = (Subgroup.centralizer {g}).index

The size of a conjugacy class is the index of the centralizer of any of its members, in Nat.card form.

Not @[simp]: Mathlib's Nat.card_coe_set_eq is itself simp, so the left-hand side simplifies to (ConjClasses.mk g).carrier.ncard and the simp normal form linter rejects the pair; that normalized form is ConjClasses.ncard_carrier_mk.

@[simp]

theorem ConjClasses.ncard_carrier_mk_eq_card_filter {M : Type u_2} [Monoid M] [Fintype M] [DecidableEq M] (g : M) : (ConjClasses.mk g).carrier.ncard = {x : M | ConjClasses.mk x = ConjClasses.mk g}.card

The size of a conjugacy class as a Finset cardinality: the members of the class of g are the elements of the monoid whose class is that of g, so in a finite monoid with decidable equality the class size is a count that can be evaluated.

theorem ConjClasses.card_carrier_mk_eq_card_filter {M : Type u_2} [Monoid M] [Fintype M] [DecidableEq M] (g : M) : Nat.card ↑(ConjClasses.mk g).carrier = {x : M | ConjClasses.mk x = ConjClasses.mk g}.card

The size of a conjugacy class as a computable Finset cardinality, in Nat.card form. See ncard_carrier_mk_eq_card_filter for the simp normal form.

theorem ConjClasses.card_carrier_dvd_card {G : Type u_1} [Group G] (C : ConjClasses G) : Nat.card ↑C.carrier ∣ Nat.card G

The size of a conjugacy class divides the order of the group, being the index of a centralizer.

theorem ConjClasses.card_carrier_cast_ne_zero {G : Type u_1} [Group G] {R : Type u_2} [Semiring R] (C : ConjClasses G) (h : ↑(Nat.card G) ≠ 0) : ↑(Nat.card ↑C.carrier) ≠ 0

The size of a conjugacy class is nonzero in any semiring in which the order of the group is nonzero: it divides that order.

theorem ConjClasses.card_carrier_div_card_ne_zero {G : Type u_1} [Group G] {R : Type u_2} [DivisionSemiring R] (C : ConjClasses G) (hG : ↑(Nat.card G) ≠ 0) : ↑(Nat.card ↑C.carrier) / ↑(Nat.card G) ≠ 0

The proportion #C / #G of a conjugacy class is nonzero in a division semiring whenever the order of the group is nonzero there.

def TauCeti.IsRealClass {G : Type u_1} [Group G] (C : ConjClasses G) : Prop

A real conjugacy class: one containing an element conjugate to its own inverse.

Equations

• TauCeti.IsRealClass C = ∃ (g : G), ConjClasses.mk g = C ∧ IsConj g g⁻¹

@[simp]

theorem TauCeti.isRealClass_iff_inv_eq {G : Type u_1} [Group G] {C : ConjClasses G} : IsRealClass C ↔ C⁻¹ = C

A class is real exactly when inversion fixes it.

theorem TauCeti.isRealClass_mk_iff {G : Type u_1} [Group G] {g : G} : IsRealClass (ConjClasses.mk g) ↔ IsConj g g⁻¹

The class of g is real exactly when g is conjugate to g⁻¹.

The size of a class against the order of a member

theorem ConjClasses.card_carrier_mul_orderOf_dvd {G : Type u_1} [Group G] (C : ConjClasses G) (σ : G) (hσ : σ ∈ C.carrier) : Nat.card ↑C.carrier * orderOf σ ∣ Nat.card G

The size of a conjugacy class times the order of a member divides the order of the group.

For a finite group this is what makes Nat.card G / (Nat.card C.carrier * orderOf σ) an exact ratio rather than a truncated division, which card_div_card_carrier_mul_orderOf_eq_card_centralizer_div_orderOf then evaluates. No finiteness is assumed here: for an infinite group Nat.card G is 0, and every natural number divides 0.

theorem ConjClasses.card_div_card_carrier_mul_orderOf_pos {G : Type u_1} [Group G] [Finite G] (C : ConjClasses G) (σ : G) (hσ : σ ∈ C.carrier) : 0 < Nat.card G / (Nat.card ↑C.carrier * orderOf σ)

That quotient is positive. For a finite group the class size times the order of a member divides the group order and both are positive, so the ratio Nat.card G / (#C.carrier * orderOf σ) is a positive natural number rather than a truncation to zero.

Finiteness is needed, and not only for convenience: for an infinite G every one of Nat.card G, Nat.card C.carrier and orderOf σ may be 0, and the quotient is then 0 / 0.

theorem ConjClasses.card_div_card_carrier_mul_orderOf_eq_card_centralizer_div_orderOf {G : Type u_1} [Group G] (C : ConjClasses G) (σ : G) (hσ : σ ∈ C.carrier) (hindex : (Subgroup.centralizer {σ}).index ≠ 0) : Nat.card G / (Nat.card ↑C.carrier * orderOf σ) = Nat.card ↥(Subgroup.centralizer {σ}) / orderOf σ

That quotient in closed form. Dividing the order of the group by the class size times the order of a member leaves the order of the centralizer divided by that same order.

hindex is what lets the centralizer's index cancel from both sides; it holds automatically when G is finite. The statement is an equality of Nat.div values, and no more: for a finite G both divisions are exact and it reads as an equality of ratios, but hindex alone does not give that. An infinite abelian group with an element of infinite order satisfies hindex while Nat.card G, the centralizer's cardinality and orderOf σ are all 0, and the identity is then 0 / 0.

theorem ConjClasses.one_div_orderOf_div_card_div_card_carrier_mul_orderOf {G : Type u_1} [Group G] {K : Type u_2} [Semifield K] [CharZero K] (C : ConjClasses G) (σ : G) (hσ : σ ∈ C.carrier) : 1 / ↑(orderOf σ) / ↑(Nat.card G / (Nat.card ↑C.carrier * orderOf σ)) = ↑(Nat.card ↑C.carrier) / ↑(Nat.card G)

Dividing 1 / orderOf σ by that quotient leaves #C / #G. Since #C.carrier * orderOf σ divides #G, the quotient casts to the exact ratio, and in a semifield of characteristic zero (1 / orderOf σ) / (#G / (#C.carrier * orderOf σ)) = #C.carrier / #G. For infinite groups both sides vanish because Nat.card G = 0.

Powers of a conjugacy class

def ConjClasses.pow {M : Type u_1} [Monoid M] (C : ConjClasses M) (j : ℕ) : ConjClasses M

The j-th power of a conjugacy class. Powering respects conjugacy (IsConj.pow), so it descends to the conjugacy classes of a monoid: C.pow j is the class of the j-th powers of the members of C. The Pow instance below spells it C ^ j, which is the form every lemma here is stated in.

Equations

• C.pow j = Quotient.map (fun (x : M) => x ^ j) ⋯ C

@[instance_reducible]

instance ConjClasses.instPowNat {M : Type u_1} [Monoid M] : Pow (ConjClasses M) ℕ

Equations

• ConjClasses.instPowNat = { pow := ConjClasses.pow }

@[simp]

theorem ConjClasses.mk_pow {M : Type u_1} [Monoid M] (a : M) (j : ℕ) : ConjClasses.mk a ^ j = ConjClasses.mk (a ^ j)

The j-th power of the class of a is the class of a ^ j.

@[simp]

theorem ConjClasses.mem_pow_iff {M : Type u_1} [Monoid M] {C : ConjClasses M} {τ : M} {j : ℕ} : τ ∈ (C ^ j).carrier ↔ ∃ σ ∈ C.carrier, σ ^ j = τ

An element lies in C ^ j exactly when it is a j-th power of a member of C.

@[simp]

theorem ConjClasses.pow_zero {M : Type u_1} [Monoid M] (C : ConjClasses M) : C ^ 0 = 1

The zeroth power of any conjugacy class is the class of 1.

@[simp]

theorem ConjClasses.pow_one {M : Type u_1} [Monoid M] (C : ConjClasses M) : C ^ 1 = C

The first power of a conjugacy class is the class itself.

@[simp]

theorem ConjClasses.pow_mul {M : Type u_1} [Monoid M] (C : ConjClasses M) (i j : ℕ) : (C ^ i) ^ j = C ^ (i * j)

Iterated powers compose: raising C ^ i to the j-th power gives C ^ (i * j). Tagged @[simp] because the single power is the normal form: it rewrites towards C ^ (i * j), which is the direction the rest of this API (pow_zero, pow_one, mk_pow) already normalises to. Note this is the mirror image of Mathlib's root-level pow_mul, which orients the equation the other way for monoid elements.

@[simp]

theorem ConjClasses.map_mk {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (f : M →* N) (a : M) : map f (ConjClasses.mk a) = ConjClasses.mk (f a)

The image of the class of a under ConjClasses.map f is the class of f a.

def MulEquiv.conjClassesEquiv {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) : ConjClasses M ≃ ConjClasses N

A multiplicative equivalence induces an equivalence of conjugacy classes.

Equations

• e.conjClassesEquiv = { toFun := ConjClasses.map e.toMonoidHom, invFun := ConjClasses.map e.symm.toMonoidHom, left_inv := ⋯, right_inv := ⋯ }

theorem MulEquiv.conjClassesEquiv_apply {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) (C : ConjClasses M) : e.conjClassesEquiv C = ConjClasses.map e.toMonoidHom C

The equivalence induced on conjugacy classes is the map induced by the underlying multiplicative homomorphism.

@[simp]

theorem MulEquiv.conjClassesEquiv_mk {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) (a : M) : e.conjClassesEquiv (ConjClasses.mk a) = ConjClasses.mk (e a)

The equivalence on conjugacy classes sends the class of a representative to the class of its image.

@[simp]

theorem MulEquiv.conjClassesEquiv_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (e : M ≃* N) (f : N ≃* P) : (e.trans f).conjClassesEquiv = e.conjClassesEquiv.trans f.conjClassesEquiv

Equivalences on conjugacy classes respect composition of multiplicative equivalences.

@[simp]

theorem MulEquiv.conjClassesEquiv_symm {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) : e.symm.conjClassesEquiv = e.conjClassesEquiv.symm

The equivalence on conjugacy classes induced by an inverse multiplicative equivalence is the inverse equivalence.

@[simp]

theorem MulEquiv.conjClassesEquiv_symm_mk {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) (b : N) : e.conjClassesEquiv.symm (ConjClasses.mk b) = ConjClasses.mk (e.symm b)

The inverse equivalence on conjugacy classes maps a representative by the inverse multiplicative equivalence.

@[simp]

theorem MulEquiv.conjClassesEquiv_refl {M : Type u_1} [Monoid M] : (refl M).conjClassesEquiv = Equiv.refl (ConjClasses M)

The identity multiplicative equivalence induces the identity on conjugacy classes.

@[simp]

theorem ConjClasses.map_pow {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (f : M →* N) (C : ConjClasses M) (j : ℕ) : map f (C ^ j) = map f C ^ j

Powering a conjugacy class is natural in the monoid.

@[simp]

theorem MulEquiv.conjClassesEquiv_pow {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (e : M ≃* N) (C : ConjClasses M) (j : ℕ) : e.conjClassesEquiv (C ^ j) = e.conjClassesEquiv C ^ j

An equivalence induced on conjugacy classes commutes with powers.

@[simp]

theorem MulEquiv.conjClassesEquiv_inv {G : Type u_3} {H : Type u_4} [Group G] [Group H] (e : G ≃* H) (C : ConjClasses G) : e.conjClassesEquiv C⁻¹ = (e.conjClassesEquiv C)⁻¹

An equivalence induced on conjugacy classes of groups commutes with inversion.

theorem ConjClasses.mk_ne_mk_of_orderOf_ne {M : Type u_1} [Monoid M] {a b : M} (h : orderOf a ≠ orderOf b) : ConjClasses.mk a ≠ ConjClasses.mk b

Elements of different orders lie in different conjugacy classes, even in a monoid.

@[instance_reducible]

instance TauCeti.instMulActionMulAutConjClasses {G : Type u_1} [Monoid G] : MulAction (MulAut G) (ConjClasses G)

An automorphism acts on conjugacy classes by mapping representatives.

Equations

• TauCeti.instMulActionMulAutConjClasses = { smul := fun (φ : MulAut G) (c : ConjClasses G) => ConjClasses.map (MulEquiv.toMonoidHom φ) c, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem MulAut.smul_conjClasses_mk {G : Type u_1} [Monoid G] (φ : MulAut G) (x : G) : φ • ConjClasses.mk x = ConjClasses.mk (φ x)

The automorphism action is computed on representatives.

theorem MulAut.conjClassesEquiv_apply {G : Type u_1} [Monoid G] (φ : MulAut G) (C : ConjClasses G) : (MulEquiv.conjClassesEquiv φ) C = φ • C

The equivalence on conjugacy classes induced by an automorphism agrees with the existing automorphism action.

@[simp]

theorem MulAut.smul_conjClasses_pow {G : Type u_1} [Monoid G] (φ : MulAut G) (c : ConjClasses G) (n : ℕ) : φ • c ^ n = (φ • c) ^ n

Automorphisms commute with powering conjugacy classes.

@[simp]

theorem MulAut.smul_conjClasses_inv {G : Type u_1} [Group G] (φ : MulAut G) (c : ConjClasses G) : φ • c⁻¹ = (φ • c)⁻¹

Automorphisms commute with inversion of conjugacy classes.

@[simp]

theorem TauCeti.mulAut_conj_smul_conjClasses {G : Type u_1} [Group G] (g : G) (c : ConjClasses G) : MulAut.conj g • c = c

Inner automorphisms fix every conjugacy class.