Documentation

TauCeti.GroupTheory.ArtinCoefficient

The Artin coefficients of a finite group, and Artin's identity for fixed points #

Attach to every subgroup C of a finite group G the integer

C.artinCoeff = ∑_{D cyclic, C ≤ D} μ [D : C],

the Möbius function of arithmetic summed over the relative indices of the cyclic subgroups above C. It vanishes unless C is cyclic, because a subgroup of a cyclic group is cyclic. These are the coefficients of Artin's identity: for every g : G,

∑_C C.artinCoeff * |C| * |(G ⧸ C)^g| = |G|.

Two inputs carry the proof. The first is combinatorial: for a cyclic subgroup D and a subgroup E ≤ D the map C ↦ [D : C] is a bijection from the subgroups between E and D onto the divisors of [D : E], so ∑_{E ≤ C ≤ D} μ [D : C] is ∑_{d ∣ [D : E]} μ d, which is 1 when E = D and 0 otherwise. When E ≰ D no subgroup lies between E and D at all, so that sum is empty, hence again 0. Summing over the cyclic D leaves the single term D = ⟨y⟩, so the Artin coefficients of the subgroups containing a fixed element add up to 1 (TauCeti.sum_artinCoeff_of_mem). The second is a count, taken from TauCeti.GroupTheory.QuotientGroup.Basic: the preimage in G of the g-fixed points of G ⧸ C is the set of x with x⁻¹ g x ∈ C, and it is a union of cosets of C, so it has |C| * |(G ⧸ C)^g| elements (Subgroup.natCard_mul_natCard_fixedBy). Exchanging the two summations then replaces the inner sum by 1 for each of the |G| elements x.

The identity is stated over ℤ rather than in a coefficient field, so that it can be transferred to Grothendieck groups of modular representations, where the order of the group need not be invertible.

Artin's induction theorem, TauCeti.ClassFunction.natCard_nsmul_one_mem_indVirtualCharacters_isCyclic (TauCeti.RepresentationTheory.Induction.Artin.Basic), is the in-repository consumer: it reads TauCeti.sum_artinCoeff_of_mem over the cyclic subgroups, the noncyclic ones contributing nothing by Subgroup.artinCoeff_eq_zero_of_not_isCyclic, and maps the coefficients into its field.

Main declarations #

References #

Möbius sums over the subgroups of a cyclic group #

source
theorem Subgroup.sum_moebius_index {K : Type u_1} [Group K] [Finite K] [IsCyclic K] (F₀ : Subgroup K) :
∑ᶠ (F : Subgroup K) (_ : F₀ ≤ F), ArithmeticFunction.moebius F.index = if F₀ = ⊤ then 1 else 0

In a finite cyclic group the Möbius function of the index, summed over the subgroups above a fixed subgroup F₀, is 1 if F₀ is everything and 0 otherwise: the subgroups above F₀ are indexed by their indices, which run over the divisors of [K : F₀].

source
theorem TauCeti.sum_moebius_relIndex {G : Type u_1} [Group G] {E D : Subgroup G} [Finite ↥D] (hD : IsCyclic ↥D) :
∑ᶠ (C : Subgroup G) (_ : E ≤ C ∧ C ≤ D), ArithmeticFunction.moebius (C.relIndex D) = if E = D then 1 else 0

The Möbius function of the relative index in a cyclic subgroup D, summed over the subgroups between E and D, is 1 if E = D and 0 otherwise. This is Subgroup.sum_moebius_index read through the correspondence, available when E ≤ D, between the subgroups of G lying between E and D and the subgroups of D above E.subgroupOf D; when E ≰ D the interval is empty and both sides vanish. Only D need be finite, since every contributing subgroup lies below it.

The Artin coefficients #

source
noncomputable def Subgroup.artinCoeff {G : Type u_1} [Group G] [Finite G] (C : Subgroup G) :
ℤ

The Artin coefficient of a subgroup C of a finite group, the sum of μ [D : C] over the cyclic subgroups D containing C. It vanishes unless C is cyclic.

The outer sum runs over all of Subgroup G, which is finite, while the inner one restricts to the cyclic subgroups above C; Subgroup.artinCoeff_def rewrites the pair as a single conditional finsum.

Instances For
    source
    theorem Subgroup.artinCoeff_def {G : Type u_1} [Group G] [Finite G] (C : Subgroup G) :
    C.artinCoeff = ∑ᶠ (D : Subgroup G) (_ : IsCyclic ↥D ∧ C ≤ D), ArithmeticFunction.moebius (C.relIndex D)

    Subgroup.artinCoeff unfolded: the Möbius function of the relative index, summed over the cyclic subgroups above C.

    source
    @[simp]
    theorem Subgroup.artinCoeff_eq_zero_of_not_isCyclic {G : Type u_1} [Group G] [Finite G] {C : Subgroup G} (hC : ¬IsCyclic ↥C) :
    C.artinCoeff = 0

    A subgroup of a cyclic group is cyclic, so a noncyclic subgroup lies below no cyclic subgroup and its Artin coefficient vanishes.

    source
    theorem TauCeti.sum_artinCoeff_of_mem {G : Type u_1} [Group G] [Finite G] (y : G) :
    ∑ᶠ (C : Subgroup G) (_ : y ∈ C), C.artinCoeff = 1

    The Artin coefficients of the subgroups containing an element add up to one. This is the combinatorial half of Artin's identity for fixed points.

    Artin's identity for fixed points #

    source
    theorem TauCeti.sum_artinCoeff_mul_card_fixedBy {G : Type u_1} [Group G] [Finite G] (g : G) :
    ∑ᶠ (C : Subgroup G), C.artinCoeff * ↑(Nat.card ↥C) * ↑(Nat.card ↑(MulAction.fixedBy (G ⧸ C) g)) = ↑(Nat.card G)

    Artin's identity for fixed points: weighting the permutation character of G ⧸ C by C.artinCoeff * |C| and summing over all subgroups gives |G|, at every g : G.