ConductorLocal.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local detection of the squarefree cubic conductor. A nontrivial prime character survives every inducing modulus, as witnessed by CRT.

lemma OAI.CubicFirstMoment.residue_crt_one line 13
lemma OAI.CubicFirstMoment.cubicSymbol_eq_one_of_dvd_sub line 20
lemma OAI.CubicFirstMoment.isCoprime_of_dvd_sub_one line 25
theorem OAI.CubicFirstMoment.mixed_conductor_left_prime line 32
Source documentation
Every prime in the left squarefree cubic factor divides a modulus whose character agrees with the mixed symbol on primary coprime inputs.
```
theorem mixed_conductor_left_prime {a b d p : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a)
    (hab : IsCoprime a b) (hp : primaryPrime p) (hpa : p ∣ a)
    (ψ : MulChar (Residues d) ℂ)
    (hagree : ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
      ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x) : p ∣ d := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic
lemma OAI.CubicFirstMoment.squarefree_primary_dvd_of_prime_dvd line 67
theorem OAI.CubicFirstMoment.mixed_conductor_contains line 82
Source documentation
The conductor away from three is exactly the original squarefree product: no variable prime can disappear under primitive reduction.
```
theorem mixed_conductor_contains {a b d : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (ψ : MulChar (Residues d) ℂ)
    (hagree : ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
      ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x) : a*b ∣ d := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic
lemma OAI.CubicFirstMoment.mixed_character_primary_match line 98
lemma OAI.CubicFirstMoment.residueIdealChar_primaryNormalize line 113

theorem OAI.CubicFirstMoment.primitive_ideal_mixed_match line 124

Source documentation

On all ideals prime to three, the primitive ideal coefficient agrees with the actual mixed cubic coefficient, including their common zeros.

theorem primitive_ideal_mixed_match {a b d : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (ψ : MulChar (Residues d) ℂ)
    (hu : ∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u) = 1)
    (hagree : ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
      ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x)
    (ν : EisensteinIdealExponent) (hν : primary (idealPrimaryGenerator ν)) :
    residueIdealChar d ψ ν = primaryMixedIdealChar a b ν := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealPrimaryGenerator, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.primaryMixedIdealChar