Breadth of a finite group

DefinitionBreadth of an element#✓fully proved

Let \(G\) be a finite group, \(p\) a natural number and \(g \in G\), and write \(g^G\) for the conjugacy class of \(g\). When \(p \ge 2\), the breadth \(\operatorname{br}_p(g)\) of \(g\) is \(\lfloor \log_p |g^G| \rfloor\), the largest natural number \(k\) with \(p^k \le |g^G|\); when \(p \le 1\), it is \(0\).

If \(p\) is prime and \(G\) is a \(p\)-group, then \(|g^G|\) is a power of \(p\), so \(p^{\operatorname{br}_p(g)} = |g^G|\).

noncomputable def elementBreadth [Finite G] (p : ℕ) (g : G) : ℕ :=
  Nat.log p (Nat.card (ConjClasses.mk g).carrier)

Used by 6

Used byBreadth of a finite group · Breadth from an exact class size · Element breadth is at most the group breadth · Breadth of the identity · The group breadth is attained · Class sizes in a \(p\)-group via breadth

DefinitionBreadth of a finite group#✓fully proved

For a finite group \(G\) and a natural number \(p\), the breadth \(\operatorname{br}_p(G)\) of \(G\) is the maximum of the element breadths \(\operatorname{br}_p(g)\) over all \(g \in G\).

noncomputable def breadth (p : ℕ) (G : Type*) [Group G] [Fintype G] : ℕ :=
  Finset.univ.sup (fun g : G ↦ elementBreadth p g)

Uses 1 · Used by 2

Statement usesBreadth of an element

Used byElement breadth is at most the group breadth · The group breadth is attained

TheoremConjugacy class sizes divide the group order#✓fully proved

In a finite group \(G\), the number of elements of the conjugacy class of any \(g \in G\) divides the order \(|G|\).

theorem card_carrier_dvd_card [Finite G] (g : G) :
    Nat.card (ConjClasses.mk g).carrier ∣ Nat.card G

Used by 1

Used byConjugacy classes of a finite \(p\)-group have \(p\)-power size

TheoremConjugacy classes of a finite \(p\)-group have \(p\)-power size#✓fully proved

Let \(p\) be a prime and \(G\) a finite \(p\)-group. For every \(g \in G\) there is a natural number \(k\) such that the conjugacy class of \(g\) has exactly \(p^k\) elements.

theorem exists_card_carrier_eq_pow (p : ℕ) [Finite G] [Fact p.Prime]
    (hG : IsPGroup p G) (g : G) :
    ∃ k : ℕ, Nat.card (ConjClasses.mk g).carrier = p ^ k

Uses 1 · Used by 1

Proof usesConjugacy class sizes divide the group order

Used byClass sizes in a \(p\)-group via breadth

TheoremBreadth from an exact class size#✓fully proved

Let \(G\) be a finite group, \(p\) a prime, \(k\) a natural number and \(g \in G\). If the conjugacy class of \(g\) has exactly \(p^k\) elements, then the breadth \(\operatorname{br}_p(g)\) of \(g\) equals \(k\).

theorem elementBreadth_eq_of_card_eq [Finite G] {p k : ℕ} (hp : p.Prime) (g : G)
    (h : Nat.card (ConjClasses.mk g).carrier = p ^ k) :
    elementBreadth p g = k

Uses 1 · Used by 1

Statement usesBreadth of an element

Used byClass sizes in a \(p\)-group via breadth

TheoremClass sizes in a \(p\)-group via breadth#✓fully proved

Let \(p\) be a prime, \(G\) a finite \(p\)-group and \(g \in G\), and write \(g^G\) for the conjugacy class of \(g\). Then the breadth \(\operatorname{br}_p(g)\) of \(g\) satisfies \(p^{\operatorname{br}_p(g)} = |g^G|\).

theorem pow_elementBreadth_eq_card (p : ℕ) [Finite G] [Fact p.Prime]
    (hG : IsPGroup p G) (g : G) :
    p ^ elementBreadth p g = Nat.card (ConjClasses.mk g).carrier

Uses 3

Statement usesBreadth of an element

Proof usesBreadth from an exact class size · Conjugacy classes of a finite \(p\)-group have \(p\)-power size

TheoremThe conjugacy class of the identity#✓fully proved

In every group, the conjugacy class of the identity element \(1\) is the singleton \(\{1\}\).

theorem carrier_mk_one : (ConjClasses.mk (1 : G)).carrier = {1}

Used by 1

Used byBreadth of the identity

TheoremBreadth of the identity#✓fully proved

In a finite group, the breadth \(\operatorname{br}_p(1)\) of the identity element \(1\) is \(0\) for every natural number \(p\).

theorem elementBreadth_one [Finite G] (p : ℕ) : elementBreadth p (1 : G) = 0

Uses 2

Statement usesBreadth of an element

Proof usesThe conjugacy class of the identity

TheoremElement breadth is at most the group breadth#✓fully proved

Let \(G\) be a finite group and \(p\) a natural number. For every \(g \in G\), the breadth \(\operatorname{br}_p(g)\) of \(g\) is at most the breadth \(\operatorname{br}_p(G)\) of \(G\).

theorem elementBreadth_le_breadth (p : ℕ) [Fintype G] (g : G) :
    elementBreadth p g ≤ breadth p G

Uses 2

Statement usesBreadth of a finite group · Breadth of an element

TheoremThe group breadth is attained#✓fully proved

Let \(G\) be a finite group and \(p\) a natural number. There is an element \(g \in G\) whose breadth \(\operatorname{br}_p(g)\) equals the breadth \(\operatorname{br}_p(G)\) of \(G\).

theorem exists_breadth_eq_elementBreadth (p : ℕ) [Fintype G] [Nonempty G] :
    ∃ g : G, breadth p G = elementBreadth p g

Uses 2

Statement usesBreadth of a finite group · Breadth of an element

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.