CyclicGluing.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Gluing the real characters selected by a simple zeta zero

A zero-order function on subgroups determines each cyclic restriction by its values on the subgroups generated by single elements. Conjugacy of these orders then gives precisely the class function used in odd-degree descent. No global irreducible-character decomposition is needed.

def OAI.DukePrimeDegree.cyclicZeroSign line 23
Source documentation
The sign detected by the zero order of the cyclic fixed field.
```
def cyclicZeroSign (m : Subgroup G → ℤ) (g : G) : ℝˣ :=
…
```
theorem OAI.DukePrimeDegree.cyclicZeroSign_eq_character line 26
theorem OAI.DukePrimeDegree.cyclicZeroSign_cyclic_restriction line 40
theorem OAI.DukePrimeDegree.cyclicZeroSign_conjugate line 50

theorem OAI.DukePrimeDegree.sum_realLinearCharacter line 62

Source documentation

The average of a finite real character detects its being principal.

theorem sum_realLinearCharacter {C : Type*} [Group C] [Fintype C]
    (χ : C →* ℝˣ) :
    (∑ g, (χ g : ℝ)) = if χ = 1 then (Fintype.card C : ℝ) else 0 := by
…

theorem OAI.DukePrimeDegree.sum_cyclicZeroSign line 79

theorem OAI.DukePrimeDegree.sum_real_eq_cyclic_sums line 89

Source documentation

The scalar form of cyclic indicator inversion for real observables.

theorem sum_real_eq_cyclic_sums
    {G : Type*} [Group G] [Fintype G]
    (a : CyclicSubgroups G → ℤ)
    (ha : ∀ g : G, (∑ C, if g ∈ C.val then a C else 0) = 1)
    (f : G → ℝ) :
    (∑ g, f g) = ∑ C : CyclicSubgroups G, (a C : ℝ) * ∑ g : C.val, f g := by
…

Mentions: OAI.DukePrimeDegree.CyclicSubgroups

theorem OAI.DukePrimeDegree.cyclicZeroSign_trivial_of_odd_average line 120

Source documentation

Once the cyclic averages recover the subgroup order, odd-index descent forces all signs to be principal.

theorem cyclicZeroSign_trivial_of_odd_average
    (m : Subgroup G → ℤ)
    (hconj : ∀ (C : Subgroup G) (a : G), m (C.map (MulAut.conj a).toMonoidHom) = m C)
    (hcyclic : ∀ C : Subgroup G, IsCyclic C → ∃ χ : C →* ℝˣ,
      ∀ x : C, m (Subgroup.zpowers (x : G)) = if χ x = 1 then 1 else 0)
    (H : Subgroup G) [Fintype H] (hodd : Odd H.index)
    (havg : ∑ h : H, (cyclicZeroSign m (h : G) : ℝ) = Fintype.card H) :
    ∀ g, cyclicZeroSign m g = 1 :=
…

Mentions: OAI.DukePrimeDegree.cyclicZeroSign