CyclicIntegerOrders.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integer fixed-field orders at a simple cyclic zero

For a cyclic extension with the actual even ray realizations, a simple zero selects one real character. Every intermediate-field zero order is the indicator that this character is trivial on the fixing subgroup.

lemma OAI.DukePrimeDegree.realLinearCharacter_eq_one_iff line 20
lemma OAI.DukePrimeDegree.realLinearCharacter_ker line 36

theorem OAI.DukePrimeDegree.zetaMultiplicity_le_of_cyclic_ray_family line 51

Source documentation

Nonnegative orders in the cyclic factorization show that the base field's zero multiplicity cannot exceed the extension's.

theorem zetaMultiplicity_le_of_cyclic_ray_family
    {N : ℕ} [NeZero N]
    (ψ : ((E ≃ₐ[F] E) →* ℂˣ) → EvenRayCharacter F N)
    (hid : ∀ χ, (ψ χ).idealHom = idealHom F E χ)
    (hψ : ∀ χ, χ ≠ 1 → (ψ χ).IsNonprincipal)
    (hD : (NumberField.discr E).natAbs ∣ N)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) :
    zetaMultiplicity F β ≤ zetaMultiplicity E β := by
…

Mentions: OAI.DukePrimeDegree.zetaMultiplicity

theorem OAI.DukePrimeDegree.exists_real_character_of_simple_zeta line 79

Source documentation

The cyclic analytic step expressed with the actual integer zeta multiplicities used in odd-degree descent.

theorem exists_real_character_of_simple_zeta
    {N : ℕ} [NeZero N]
    (ψ : ((E ≃ₐ[F] E) →* ℂˣ) → EvenRayCharacter F N)
    (hid : ∀ χ, (ψ χ).idealHom = idealHom F E χ)
    (hψ : ∀ χ, χ ≠ 1 → (ψ χ).IsNonprincipal)
    (hD : (NumberField.discr E).natAbs ∣ N)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (hsimple : zetaMultiplicity E β = 1) :
    ∃ χ : (E ≃ₐ[F] E) →* ℝˣ,
      ∀ L : IntermediateField F E,
        zetaMultiplicity L β = if L.fixingSubgroup ≤ χ.ker then 1 else 0 := by
…

Mentions: OAI.DukePrimeDegree.zetaMultiplicity