Square roots in a group

The square roots of an element x of a group G are the g with g * g = x. Conjugation carries them bijectively onto the square roots of a conjugate of x (TauCeti.squareRootConjEquiv), so their number depends only on the conjugacy class of x (TauCeti.card_squareRoot_conj). That is what makes the square-root count a class function, and hence expandable in the basis of irreducible characters.

Main statements

• TauCeti.squareRootConjEquiv: conjugation is a bijection between the square roots of x and those of h * x * h⁻¹.
• TauCeti.card_squareRoot_conj: conjugate elements have equally many square roots.

Implementation notes

Nat.card is used for the count, so no finiteness or decidability assumption is needed to state the result. It follows the usual junk-value convention: on a group in which some element has infinitely many square roots, Nat.card returns 0 at that element rather than a cardinal, so the count below is a genuine number of square roots only when that subtype is finite — as it is for a finite group. The statements are unaffected either way, since conjugation is a bijection whether or not the two sides are finite.

def TauCeti.squareRootConjEquiv {G : Type u_1} [Group G] (x h : G) : { g : G // g * g = x } ≃ { g : G // g * g = h * x * h⁻¹ }

Conjugation permutes square roots: g ↦ h * g * h⁻¹ is a bijection from the square roots of x onto the square roots of h * x * h⁻¹. It is the conjugation automorphism MulAut.conj h restricted to the square roots, being multiplicative and injective.

Equations

• TauCeti.squareRootConjEquiv x h = (↑(MulAut.conj h)).subtypeEquiv ⋯

@[simp]

theorem TauCeti.squareRootConjEquiv_apply_coe {G : Type u_1} [Group G] (x h : G) (g : { g : G // g * g = x }) : ↑((squareRootConjEquiv x h) g) = h * ↑g * h⁻¹

Conjugation of square roots is conjugation of group elements.

The definition is not @[expose]d, so this is how it applies outside this file: the generic Equiv.subtypeEquiv_apply cannot fire on the opaque TauCeti.squareRootConjEquiv.

@[simp]

theorem TauCeti.squareRootConjEquiv_symm_apply_coe {G : Type u_1} [Group G] (x h : G) (g : { g : G // g * g = h * x * h⁻¹ }) : ↑((squareRootConjEquiv x h).symm g) = h⁻¹ * ↑g * h

The inverse of TauCeti.squareRootConjEquiv is conjugation by h⁻¹; as with TauCeti.squareRootConjEquiv_apply_coe, this is what the opaque definition needs in place of Equiv.subtypeEquiv_symm.

theorem TauCeti.card_squareRoot_conj {G : Type u_1} [Group G] (x h : G) : Nat.card { g : G // g * g = h * x * h⁻¹ } = Nat.card { g : G // g * g = x }

The number of square roots is a class function of the group element: x and its conjugate h * x * h⁻¹ have equally many square roots. The counts are Nat.cards, hence both 0 in the degenerate case of infinitely many square roots.