CubicNumeratorConductor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Primitive reduction of the actual cubic numerator character preserves its cubic order, its global unit invariance, and its values on primary arguments prime to the original modulus.

lemma OAI.CubicFirstMoment.ResidueCharacterInduces.cube_eq_one line 11

theorem OAI.CubicFirstMoment.cubicNumerator_primitive_conductor line 29

Source documentation

Exact primitive character associated with any nonzero numerator.

theorem cubicNumerator_primitive_conductor (hpub : CubicSupplementaryPeriodicity)
    {v : Eisenstein} (hv : v ≠ 0) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ),
      d ≠ 0 ∧ PrimitiveResidueCharacter d ψ ∧
      d ∣ 9*v ∧ normNat d ≤ normNat (9*v) ∧ ψ^3=1 ∧
      (∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u)=1) ∧
      ResidueCharacterInduces (9*v) d (cubicNumeratorChar hpub v hv) ψ ∧
      (∀ x : Eisenstein, primary x → IsCoprime v x →
        ψ (Ideal.Quotient.mk (modulus d) x)=cubicSymbol x v) := by
…

Mentions: OAI.CubicFirstMoment.CubicSupplementaryPeriodicity, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.cubicNumeratorChar, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.primaryNoncube_primitive_conductor line 51

Source documentation

For a primary noncube the primitive character is nonprincipal and nonreal; no exceptional real character is introduced in conductor reduction.

theorem primaryNoncube_primitive_conductor (hpub : CubicSupplementaryPeriodicity)
    {v : Eisenstein} (hv : primary v) (hn : ¬∃ j : Eisenstein, j^3=v) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ),
      d ≠ 0 ∧ PrimitiveResidueCharacter d ψ ∧ ψ ≠ 1 ∧ star ψ ≠ ψ ∧
      normNat d ≤ normNat (9*v) ∧ ψ^3=1 ∧
      (∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u)=1) ∧
      (∀ x : Eisenstein, primary x → IsCoprime v x →
        ψ (Ideal.Quotient.mk (modulus d) x)=cubicSymbol x v) := by
…

Mentions: OAI.CubicFirstMoment.CubicSupplementaryPeriodicity, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.cubicSymbol