PrimitiveConductor.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary conductor reduction for the finite residue characters. Minimality is measured by the positive ideal norm; the inducing character and exact deleted Euler factors are not supplied as extra assumptions.

def OAI.CubicFirstMoment.ResidueCharacterInduces line 13
Source documentation
Agreement of characters on ideals prime to the original modulus.
```
def ResidueCharacterInduces (q d : Eisenstein)
    (χ : MulChar (Residues q) ℂ) (ψ : MulChar (Residues d) ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
def OAI.CubicFirstMoment.PrimitiveResidueCharacter line 20
Source documentation
No inducing modulus has smaller norm. This is the usual primitivity criterion for a finite ray character over a principal ideal domain.
```
def PrimitiveResidueCharacter (q : Eisenstein) (χ : MulChar (Residues q) ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.refl line 24
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.trans line 27
theorem OAI.CubicFirstMoment.primitive_residue_conductor_exists line 38
Source documentation
Every finite character has an actual primitive inducing character, of modulus dividing the original one and of no larger norm.
```
theorem primitive_residue_conductor_exists {q : Eisenstein} (hq : q ≠ 0)
    (χ : MulChar (Residues q) ℂ) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ),
      d ≠ 0 ∧ ResidueCharacterInduces q d χ ψ ∧
      normNat d ≤ normNat q ∧ PrimitiveResidueCharacter d ψ := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.PrimitiveResidueCharacter
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.global_units line 54
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.restriction line 63
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.nonprincipal line 73