CyclicFixedOrders.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cyclic characters on the Galois group of a normal closure

The cyclic factorization over the fixed field of a subgroup gives a character on that subgroup. The tower identification relates its values to the original fixed-field zero multiplicities, as required for gluing.

theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_le_extension line 32

Source documentation

The cyclic fixed field has no larger zero multiplicity than the normal closure itself.

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

Mentions: OAI.DukePrimeDegree.fixedFieldMultiplicity, OAI.DukePrimeDegree.zetaMultiplicity

theorem OAI.DukePrimeDegree.cyclic_fixedField_character line 45

Source documentation

A simple normal-closure zero gives the cyclic sign data directly in terms of the original subgroup lattice.

theorem cyclic_fixedField_character
    {N : ℕ} [NeZero N]
    (ψ : ((E ≃ₐ[IntermediateField.fixedField C] E) →* ℂˣ) →
      EvenRayCharacter (IntermediateField.fixedField C) N)
    (hid : ∀ χ, (ψ χ).idealHom = idealHom (IntermediateField.fixedField C) E χ)
    (hψ : ∀ χ, χ ≠ 1 → (ψ χ).IsNonprincipal)
    (hD : (NumberField.discr E).natAbs ∣ N)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (hsimple : zetaMultiplicity E β = 1) :
    ∃ χ : C →* ℝˣ,
      (∀ x : C, fixedFieldMultiplicity β (Subgroup.zpowers (x : E ≃ₐ[ℚ] E)) =
        if χ x = 1 then 1 else 0) ∧
…

Mentions: OAI.DukePrimeDegree.zetaMultiplicity, OAI.DukePrimeDegree.fixedFieldMultiplicity