CyclicInduction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Cyclic subgroup coefficients for Stark descent

Möbius inversion on the finite poset of cyclic subgroups expresses the constant function as an integer combination of their indicators. Averaging conjugates gives the denominator-cleared cyclic permutation identity used to compare Dedekind zeta orders.

theorem OAI.DukePrimeDegree.finite_poset_upper_weights line 18
abbrev OAI.DukePrimeDegree.CyclicSubgroups line 54
Source documentation
The finite set of cyclic subgroups, retaining their actual subgroup carrier. No choice of generators enters the coefficients.
```
abbrev CyclicSubgroups (G : Type*) [Group G] :=
…
```
instance OAI.DukePrimeDegree.instFintypeCyclicSubgroups line 57

theorem OAI.DukePrimeDegree.exists_cyclic_indicator_coefficients line 61

Source documentation

Integer cyclic-subgroup indicator coefficients.

theorem exists_cyclic_indicator_coefficients
    (G : Type*) [Group G] [Finite G] :
    ∃ a : CyclicSubgroups G → ℤ, ∀ g : G,
      (∑ C, if g ∈ C.val then a C else 0) = 1 := by
…

Mentions: OAI.DukePrimeDegree.CyclicSubgroups

theorem OAI.DukePrimeDegree.exists_cyclic_conjugacy_coefficients line 79
Source documentation
Conjugacy averaging gives the denominator-cleared cyclic induction identity, with coefficients independent of the group element.
```
theorem exists_cyclic_conjugacy_coefficients
    (G : Type*) [Group G] [Fintype G] :
    ∃ a : CyclicSubgroups G → ℤ, ∀ g : G,
      (∑ C, a C * ∑ x : G, if x⁻¹ * g * x ∈ C.val then (1 : ℤ) else 0) =
        Fintype.card G := by
…
```
Mentions: OAI.DukePrimeDegree.CyclicSubgroups

theorem OAI.DukePrimeDegree.permutation_character_eq_fixed_sum line 97

Source documentation

The permutation character counts fixed points in the actual coset representation used by the Artin Euler factors.

theorem permutation_character_eq_fixed_sum
    {G Ω : Type*} [Monoid G] [Fintype Ω] [MulAction G Ω] (g : G) :
    (Representation.ofMulAction ℂ G Ω).character g =
      ∑ x : Ω, if g • x = x then (1 : ℂ) else 0 := by
…

theorem OAI.DukePrimeDegree.conjugacy_indicator_sum_eq_card_mul_character line 112

Source documentation

Conjugacy counting and the coset permutation character differ by exactly the subgroup order.

theorem conjugacy_indicator_sum_eq_card_mul_character
    {G : Type*} [Group G] [Fintype G] (H : Subgroup G) (g : G) :
    (∑ x : G, if x⁻¹ * g * x ∈ H then (1 : ℂ) else 0) =
      Fintype.card H * (Representation.ofMulAction ℂ G (G ⧸ H)).character g := by
…

theorem OAI.DukePrimeDegree.exists_cyclic_permutation_character_identity line 144

Source documentation

Artin's cyclic permutation identity with integer coefficients after clearing the single denominator card G.

theorem exists_cyclic_permutation_character_identity
    (G : Type*) [Group G] [Fintype G] :
    ∃ b : CyclicSubgroups G → ℤ, ∀ g : G,
      (∑ C, (b C : ℂ) *
        (Representation.ofMulAction ℂ G (G ⧸ C.val)).character g) =
          Fintype.card G := by
…

Mentions: OAI.DukePrimeDegree.CyclicSubgroups