StarkOddDegree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Odd-degree descent for real cyclic zero characters

For the application to Stark's argument it is enough to know the restrictions of the zero character to cyclic subgroups. A real class function with these restrictions and average one on an odd-index subgroup is identically one. The proof uses a Sylow two-subgroup acting on the odd set of cosets; it does not require a global Artin character.

theorem OAI.DukePrimeDegree.cyclic_real_classFunction_trivial_of_odd_index line 22

Source documentation

A real class function whose cyclic restrictions are linear characters is trivial if it is trivial on an odd-index subgroup.

theorem cyclic_real_classFunction_trivial_of_odd_index
    {G : Type*} [Group G] [Finite G]
    (f : G → ℝˣ)
    (hconj : ∀ a g, f (a * g * a⁻¹) = f g)
    (hcyclic : ∀ g : G, ∃ χ : Subgroup.zpowers g →* ℝˣ,
      ∀ x : Subgroup.zpowers g, χ x = f (x : G))
    (H : Subgroup G) (hodd : Odd H.index)
    (hH : ∀ g ∈ H, f g = 1) : ∀ g, f g = 1 := by
…

theorem OAI.DukePrimeDegree.cyclic_real_classFunction_trivial_of_odd_average line 64

Source documentation

Average one on a subgroup forces all its values to be one, since each real finite-order character takes only the values one and minus one.

theorem cyclic_real_classFunction_trivial_of_odd_average
    {G : Type*} [Group G] [Finite G]
    (f : G → ℝˣ)
    (hconj : ∀ a g, f (a * g * a⁻¹) = f g)
    (hcyclic : ∀ g : G, ∃ χ : Subgroup.zpowers g →* ℝˣ,
      ∀ x : Subgroup.zpowers g, χ x = f (x : G))
    (H : Subgroup G) [Fintype H] (hodd : Odd H.index)
    (havg : ∑ h : H, (f h : ℝ) = Fintype.card H) :
    ∀ g, f g = 1 := by
…