PrimitiveResidueConductorKernel.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Primitivity detects the kernel of every proper residue reduction.

lemma OAI.CubicFirstMoment.finite_monoid_idempotent_power line 11
lemma OAI.CubicFirstMoment.finite_ring_units_surjective line 28
Source documentation
A surjection of finite commutative rings is surjective on units. The proof lifts an arbitrary element and corrects its zero components using an idempotent power; no local or unramified hypothesis is imposed.
```
lemma finite_ring_units_surjective {R S : Type*} [CommRing R] [CommRing S] [Finite R]
    (f : R →+* S) (hf : Function.Surjective f) :
    Function.Surjective (Units.map f.toMonoidHom) := by
…
```
def OAI.CubicFirstMoment.residueReduction line 58
Source documentation
Reduction between actual Eisenstein residue rings.
```
def residueReduction {q d : Eisenstein} (hd : d ∣ q) : Residues q →+* Residues d :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.residueReduction_mk line 61
lemma OAI.CubicFirstMoment.residueReduction_units_surjective line 65

lemma OAI.CubicFirstMoment.residueCharacter_induces_of_kernel line 71

Source documentation

Triviality on the reduction kernel constructs a genuine lower conductor.

lemma residueCharacter_induces_of_kernel {q d : Eisenstein} (hq : q ≠ 0)
    (hd : d ∣ q) (χ : MulChar (Residues q) ℂ)
    (hker : ∀ u : (Residues q)ˣ,
      Units.map (residueReduction hd).toMonoidHom u = 1 → χ u = 1) :
    ∃ ψ : MulChar (Residues d) ℂ, ResidueCharacterInduces q d χ ψ := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.residueReduction, OAI.CubicFirstMoment.ResidueCharacterInduces

theorem OAI.CubicFirstMoment.primitiveResidue_nontrivial_kernel line 99
Source documentation
A primitive character is nontrivial on each proper reduction kernel.
```
theorem primitiveResidue_nontrivial_kernel {q d : Eisenstein} (hq : q ≠ 0)
    (hd : d ∣ q) (hsmall : normNat d < normNat q)
    (χ : MulChar (Residues q) ℂ) (hχ : PrimitiveResidueCharacter q χ) :
    ∃ u : (Residues q)ˣ, Units.map (residueReduction hd).toMonoidHom u = 1 ∧ χ u ≠ 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.residueReduction
lemma OAI.CubicFirstMoment.primitiveResidue_frequency_stabilizer line 111
Source documentation
A nonunit frequency is fixed by a unit on which a primitive character is nontrivial. The smaller modulus is the quotient by one common prime factor.
```
lemma primitiveResidue_frequency_stabilizer {q : Eisenstein} (hq : q ≠ 0)
    (χ : MulChar (Residues q) ℂ) (hχ : PrimitiveResidueCharacter q χ)
    (a : Residues q) (ha : ¬ IsUnit a) :
    ∃ u : (Residues q)ˣ, a * (u : Residues q) = a ∧ χ u ≠ 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter
theorem OAI.CubicFirstMoment.primitiveResidueFourier_nonunit line 164
Source documentation
The Fourier transform of a primitive residue character vanishes at every nonunit frequency, including those at ramified factors of the modulus.
```
theorem primitiveResidueFourier_nonunit {q : Eisenstein} (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ)
    (hχ : PrimitiveResidueCharacter q χ) (a : Residues q) (ha : ¬ IsUnit a) :
    residueCharacterFourier q hq χ a = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.residueCharacterFourier
theorem OAI.CubicFirstMoment.primitiveResidueFourier_eq line 175
Source documentation
The complete Gauss eigenrelation holds with the actual zero extension of the multiplicative character on nonunits.
```
theorem primitiveResidueFourier_eq {q : Eisenstein} (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ)
    (hχ : PrimitiveResidueCharacter q χ) (a : Residues q) :
    residueCharacterFourier q hq χ a =
      (star χ) a * gaussSum χ (residueFourierChar q hq) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.residueCharacterFourier, OAI.CubicFirstMoment.residueFourierChar

lemma OAI.CubicFirstMoment.finite_gauss_fourier_at_one line 187

Source documentation

Finite Fourier inversion at the unit element. This identity only needs the additive pairing to be perfect; the ring need not be a field.

lemma finite_gauss_fourier_at_one {R : Type*} [CommRing R] [Fintype R]
    (χ : MulChar R ℂ) (ψ : AddChar R ℂ) (hψ : ψ.IsPrimitive) :
    ∑ a : R, gaussSum χ (ψ.mulShift a) * ψ (-a) = Fintype.card R := by
…

theorem OAI.CubicFirstMoment.primitiveResidueGauss_mul_conj line 212
Source documentation
Exact square norm of the primitive residue Gauss sum, for arbitrary nonzero Eisenstein modulus, including prime powers above three.
```
theorem primitiveResidueGauss_mul_conj {q : Eisenstein} (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ)
    (hχ : PrimitiveResidueCharacter q χ) :
    gaussSum χ (residueFourierChar q hq) *
      star (gaussSum χ (residueFourierChar q hq)) = (normNat q : ℂ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.residueFourierChar, OAI.CubicFirstMoment.normNat
theorem OAI.CubicFirstMoment.primitiveResidueGauss_norm line 243
Source documentation
Positive real norm of the primitive Gauss sum.
```
theorem primitiveResidueGauss_norm {q : Eisenstein} (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ)
    (hχ : PrimitiveResidueCharacter q χ) :
    ‖gaussSum χ (residueFourierChar q hq)‖ = Real.sqrt (normNat q : ℝ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.residueFourierChar, OAI.CubicFirstMoment.normNat