StarkCharacters.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Simple zeros in cyclic Artin factorizations

The cyclic step in Stark's exceptional-zero argument uses finite, nonnegative orders of the Hecke factors. If their product has a simple zero, exactly one factor has order one. Its zero-order character is therefore a one-dimensional character, expressed using the actual meromorphic orders in the cyclic factorization.

theorem OAI.DukePrimeDegree.sum_nat_one_support line 19

theorem OAI.DukePrimeDegree.unique_factor_order_of_simple_product line 46

Source documentation

A simple zero of a product of holomorphic nonzero factors comes from exactly one simple factor. The finite nonnegative order hypothesis is supplied by the proved Hecke continuation theorems.

theorem unique_factor_order_of_simple_product
    {I : Type*} [Fintype I] (f : I → ℂ → ℂ) (β : ℂ)
    (hf : ∀ i, MeromorphicAt (f i) β)
    (hord : ∀ i, ∃ m : ℕ, meromorphicOrderAt (f i) β = (m : WithTop ℤ))
    (hsimple : meromorphicOrderAt (fun z => ∏ i, f i z) β = 1) :
    ∃ i, meromorphicOrderAt (f i) β = 1 ∧
      ∀ j, j ≠ i → meromorphicOrderAt (f j) β = 0 := by
…

theorem OAI.DukePrimeDegree.cyclic_zero_order_character line 70

Source documentation

The zero-order sum on a cyclic group is one linear character once the orders of its factors sum to one.

theorem cyclic_zero_order_character
    {C : Type*} [Group C] [Fintype (C →* ℂˣ)]
    (m : (C →* ℂˣ) → ℕ) (hm : ∑ χ, m χ = 1) :
    ∃ χ : C →* ℂˣ, ∀ g : C,
      (∑ ψ : C →* ℂˣ, (m ψ : ℂ) * (ψ g : ℂ)) = (χ g : ℂ) := by
…

def OAI.DukePrimeDegree.conjugateLinearCharacter line 85
Source documentation
Complex conjugation of a one-dimensional character.
```
def conjugateLinearCharacter {C : Type*} [Group C] (χ : C →* ℂˣ) : C →* ℂˣ :=
…
```
theorem OAI.DukePrimeDegree.conjugateLinearCharacter_apply line 88

theorem OAI.DukePrimeDegree.real_character_of_simple_conjugate_orders line 94

Source documentation

At a real simple zero, conjugation-invariance of the factor orders forces the unique character supporting that zero to be real-valued.

theorem real_character_of_simple_conjugate_orders
    {C : Type*} [Group C] [Fintype (C →* ℂˣ)]
    (m : (C →* ℂˣ) → ℕ) (hm : ∑ χ, m χ = 1)
    (hc : ∀ χ, m (conjugateLinearCharacter χ) = m χ) :
    ∃ χ : C →* ℂˣ, m χ = 1 ∧
      (∀ ψ, ψ ≠ χ → m ψ = 0) ∧ ∀ g, (χ g : ℂ).im = 0 := by
…

Mentions: OAI.DukePrimeDegree.conjugateLinearCharacter

def OAI.DukePrimeDegree.realLinearCharacter line 113
Source documentation
A real-valued complex linear character regarded as a real character.
```
def realLinearCharacter {C : Type*} [Group C] (χ : C →* ℂˣ)
    (hr : ∀ g, (χ g : ℂ).im = 0) : C →* ℝˣ where
…
```
theorem OAI.DukePrimeDegree.realLinearCharacter_apply line 135