import Definitions.Def_RatIdele_Normalizer import Mathlib.NumberTheory.Padics.RingHoms import Mathlib.NumberTheory.DirichletCharacter.Bounds set_option autoImplicit false noncomputable section open NumberField IsDedekindDomain IsDedekindDomain.HeightOneSpectrum WithZero open Rat.HeightOneSpectrum NumberField.AdelicLevel namespace RatIdele local notation "π”Έβ„š" => AdeleRing (π“ž β„š) β„š local notation "π”Έβ„šf" => FiniteAdeleRing (π“ž β„š) β„š section Residue def unitPadicAt (p : β„•) [hp : Fact p.Prime] (x : (π”Έβ„š)Λ£) : β„€_[p] := (PadicInt.adicCompletionIntegersEquiv (π“ž β„š) ⟨p, hp.out⟩).symm.toAlgEquiv.toRingEquiv (unitIntAt ((primesEquiv (R := π“ž β„š)).symm ⟨p, hp.out⟩) x) theorem unitPadicAt_mul (p : β„•) [Fact p.Prime] (x y : (π”Έβ„š)Λ£) : unitPadicAt p (x * y) = unitPadicAt p x * unitPadicAt p y := by unfold unitPadicAt rw [unitIntAt_mul, map_mul] theorem unitPadicAt_one (p : β„•) [Fact p.Prime] : unitPadicAt p 1 = 1 := by unfold unitPadicAt rw [unitIntAt_one, map_one] theorem natCast_mul_unitPadicAt_eq_one (p : β„•) [hp : Fact p.Prime] {x : (π”Έβ„š)Λ£} {n : β„•} (h : ((n : β„•) : ((primesEquiv (R := π“ž β„š)).symm ⟨p, hp.out⟩).adicCompletion β„š) * unitAt ((primesEquiv (R := π“ž β„š)).symm ⟨p, hp.out⟩) x = 1) : ((n : β„•) : β„€_[p]) * unitPadicAt p x = 1 := by unfold unitPadicAt rw [← map_natCast (PadicInt.adicCompletionIntegersEquiv (π“ž β„š) ⟨p, hp.out⟩).symm.toAlgEquiv.toRingEquiv n, ← map_mul, natCast_mul_unitIntAt_eq_one h, map_one] theorem unitPadicAt_eq_neg_one (p : β„•) [hp : Fact p.Prime] {x : (π”Έβ„š)Λ£} (h : unitAt ((primesEquiv (R := π“ž β„š)).symm ⟨p, hp.out⟩) x = -1) : unitPadicAt p x = -1 := by unfold unitPadicAt rw [show unitIntAt ((primesEquiv (R := π“ž β„š)).symm ⟨p, hp.out⟩) x = -1 from Subtype.ext (by rw [coe_unitIntAt, h, NegMemClass.coe_neg, OneMemClass.coe_one]), map_neg, map_one] theorem fact_prime_of_mem_primeFactors {N : β„•} (p : N.primeFactors) : Fact (p : β„•).Prime := ⟨Nat.prime_of_mem_primeFactors p.2⟩ attribute [local instance] fact_prime_of_mem_primeFactors variable (N : β„•) def unitResidues (x : (π”Έβ„š)Λ£) : (p : N.primeFactors) β†’ ZMod ((p : β„•) ^ N.factorization p) := fun p => PadicInt.toZModPow (N.factorization p) (unitPadicAt p x) theorem unitResidues_mul (x y : (π”Έβ„š)Λ£) : unitResidues N (x * y) = unitResidues N x * unitResidues N y := by funext p show PadicInt.toZModPow (N.factorization p) (unitPadicAt p (x * y)) = PadicInt.toZModPow (N.factorization p) (unitPadicAt p x) * PadicInt.toZModPow (N.factorization p) (unitPadicAt p y) rw [unitPadicAt_mul, map_mul] theorem unitResidues_one : unitResidues N 1 = 1 := by funext p show PadicInt.toZModPow (N.factorization p) (unitPadicAt p 1) = 1 rw [unitPadicAt_one, map_one] variable [NeZero N] def unitResidue : (π”Έβ„š)Λ£ β†’* ZMod N where toFun x := (ZMod.equivPi N (NeZero.ne N)).symm (unitResidues N x) map_one' := by rw [unitResidues_one, map_one] map_mul' x y := by rw [unitResidues_mul, map_mul] theorem unitResidue_apply (x : (π”Έβ„š)Λ£) : unitResidue N x = (ZMod.equivPi N (NeZero.ne N)).symm (unitResidues N x) := rfl theorem equivPi_unitResidue (x : (π”Έβ„š)Λ£) : ZMod.equivPi N (NeZero.ne N) (unitResidue N x) = unitResidues N x := by rw [unitResidue_apply, RingEquiv.apply_symm_apply] theorem natCast_mul_unitResidue_eq_one {x : (π”Έβ„š)Λ£} {n : β„•} (h : βˆ€ w : HeightOneSpectrum (π“ž β„š), natGenerator w ∣ N β†’ ((n : β„•) : w.adicCompletion β„š) * unitAt w x = 1) : (n : ZMod N) * unitResidue N x = 1 := by apply (ZMod.equivPi N (NeZero.ne N)).injective rw [map_mul, map_natCast, equivPi_unitResidue, map_one] funext p rw [Pi.mul_apply, Pi.natCast_apply, Pi.one_apply] show ((n : β„•) : ZMod ((p : β„•) ^ N.factorization p)) * PadicInt.toZModPow (N.factorization p) (unitPadicAt p x) = 1 rw [← map_natCast (PadicInt.toZModPow (p := (p : β„•)) (N.factorization p)) n, ← map_mul, natCast_mul_unitPadicAt_eq_one (p : β„•) (h _ ?_), map_one] rw [natGenerator_primesEquiv_symm] exact Nat.dvd_of_mem_primeFactors p.2 theorem unitResidue_eq_one {x : (π”Έβ„š)Λ£} (h : βˆ€ w : HeightOneSpectrum (π“ž β„š), natGenerator w ∣ N β†’ unitAt w x = 1) : unitResidue N x = 1 := by have := natCast_mul_unitResidue_eq_one N (n := 1) (x := x) fun w hw => by rw [Nat.cast_one, one_mul, h w hw] rwa [Nat.cast_one, one_mul] at this theorem unitResidue_eq_neg_one {x : (π”Έβ„š)Λ£} (h : βˆ€ w : HeightOneSpectrum (π“ž β„š), natGenerator w ∣ N β†’ unitAt w x = -1) : unitResidue N x = -1 := by apply (ZMod.equivPi N (NeZero.ne N)).injective rw [equivPi_unitResidue, map_neg, map_one] funext p rw [Pi.neg_apply, Pi.one_apply] show PadicInt.toZModPow (N.factorization p) (unitPadicAt p x) = -1 rw [unitPadicAt_eq_neg_one (p : β„•) (h _ ?_), map_neg, map_one] rw [natGenerator_primesEquiv_symm] exact Nat.dvd_of_mem_primeFactors p.2 theorem unitResidue_principal (q : β„šΛ£) : unitResidue N (Units.map (algebraMap β„š π”Έβ„š : β„š β†’* π”Έβ„š) q) = 1 := unitResidue_eq_one N fun w _ => unitAt_principal w q end Residue end RatIdele namespace DirichletCharacter open RatIdele local notation "π”Έβ„š" => AdeleRing (π“ž β„š) β„š local notation "π”Έβ„šf" => FiniteAdeleRing (π“ž β„š) β„š variable {N : β„•} [NeZero N] (Ο‡ : DirichletCharacter β„‚ N) def dirichletIdeleChar : (π”Έβ„š)Λ£ β†’* β„‚Λ£ := (Ο‡.toUnitHom.comp (unitResidue N).toHomUnits)⁻¹ theorem coe_dirichletIdeleChar_apply (x : (π”Έβ„š)Λ£) : ((dirichletIdeleChar Ο‡ x : β„‚Λ£) : β„‚) = (Ο‡ (unitResidue N x))⁻¹ := by rw [dirichletIdeleChar, MonoidHom.inv_apply, Units.val_inv_eq_inv_val, MonoidHom.comp_apply, MulChar.coe_toUnitHom, MonoidHom.coe_toHomUnits] theorem dirichletIdeleChar_eq_one_of_unitResidue_eq_one {x : (π”Έβ„š)Λ£} (h : unitResidue N x = 1) : dirichletIdeleChar Ο‡ x = 1 := by refine Units.ext ?_ rw [coe_dirichletIdeleChar_apply, h, map_one, inv_one, Units.val_one] theorem dirichletIdeleChar_principal (q : β„šΛ£) : dirichletIdeleChar Ο‡ (Units.map (algebraMap β„š π”Έβ„š : β„š β†’* π”Έβ„š) q) = 1 := dirichletIdeleChar_eq_one_of_unitResidue_eq_one Ο‡ (unitResidue_principal N q) theorem norm_coe_dirichletIdeleChar_apply (x : (π”Έβ„š)Λ£) : β€–((dirichletIdeleChar Ο‡ x : β„‚Λ£) : β„‚)β€– = 1 := by rw [coe_dirichletIdeleChar_apply, norm_inv, ← MonoidHom.coe_toHomUnits (unitResidue N) x, Ο‡.unit_norm_eq_one, inv_one] theorem dirichletIdeleChar_finIncl_localUnit_of_valued_one {v : HeightOneSpectrum (π“ž β„š)} (hv : Β¬ natGenerator v ∣ N) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = 1) : dirichletIdeleChar Ο‡ (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) = 1 := by refine dirichletIdeleChar_eq_one_of_unitResidue_eq_one Ο‡ (unitResidue_eq_one N fun w hw => ?_) have hwv : w β‰  v := fun h => hv (h β–Έ hw) unfold unitAt rw [ρ_finIncl_localUnit_of_valued_one v t ht, map_one, inv_one, mul_one, Units.coe_map, finIncl_apply_snd, localUnit_apply_of_ne (π“ž β„š) β„š v t hwv] theorem coe_dirichletIdeleChar_finIncl_localUnit_of_valued_exp_neg_one {v : HeightOneSpectrum (π“ž β„š)} (hv : Β¬ natGenerator v ∣ N) (t : (v.adicCompletion β„š)Λ£) (ht : Valued.v (t : v.adicCompletion β„š) = exp (-1 : β„€)) : ((dirichletIdeleChar Ο‡ (Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t)) : β„‚Λ£) : β„‚) = Ο‡ (natGenerator v) := by set x := Units.map (finIncl (π“ž β„š) β„š) (localUnit (π“ž β„š) β„š v t) with hx have hres : ((natGenerator v : β„•) : ZMod N) * unitResidue N x = 1 := by refine natCast_mul_unitResidue_eq_one N fun w hw => ?_ have hwv : w β‰  v := fun h => hv (h β–Έ hw) unfold unitAt rw [ρ_finIncl_localUnit v t ht, hx, Units.coe_map, finIncl_apply_snd, localUnit_apply_of_ne (π“ž β„š) β„š v t hwv, one_mul, map_natCast, mul_inv_cancelβ‚€ (natCast_adicCompletion_ne_zero w (prime_natGenerator v).ne_zero)] have hΟ‡ : Ο‡ (natGenerator v) * Ο‡ (unitResidue N x) = 1 := by rw [← map_mul, hres, map_one] rw [coe_dirichletIdeleChar_apply] exact (eq_inv_of_mul_eq_one_left hΟ‡).symm theorem dirichletIdeleChar_eq_one_of_snd_eq_one_of_pos {x : (π”Έβ„š)Λ£} (hx : βˆ€ w : HeightOneSpectrum (π“ž β„š), (x : π”Έβ„š).2 w = 1) (hpos : 0 < archCoord x) : dirichletIdeleChar Ο‡ x = 1 := by refine dirichletIdeleChar_eq_one_of_unitResidue_eq_one Ο‡ (unitResidue_eq_one N fun w _ => ?_) unfold unitAt rw [ρ_eq_archSign_of_snd_eq_one hx, archSign, if_pos hpos, hx w, map_one, inv_one, mul_one] theorem coe_dirichletIdeleChar_of_snd_eq_one_of_neg {x : (π”Έβ„š)Λ£} (hx : βˆ€ w : HeightOneSpectrum (π“ž β„š), (x : π”Έβ„š).2 w = 1) (hneg : archCoord x < 0) : ((dirichletIdeleChar Ο‡ x : β„‚Λ£) : β„‚) = Ο‡ (-1) := by have hres : unitResidue N x = -1 := by refine unitResidue_eq_neg_one N fun w _ => ?_ unfold unitAt rw [ρ_eq_archSign_of_snd_eq_one hx, archSign, if_neg (not_lt.mpr hneg.le), hx w, map_neg, map_one, inv_neg, inv_one, one_mul] have hΟ‡ : Ο‡ (-1) * Ο‡ (-1) = 1 := by rw [← map_mul, neg_one_mul, neg_neg, map_one] rw [coe_dirichletIdeleChar_apply, hres] exact (eq_inv_of_mul_eq_one_left hΟ‡).symm end DirichletCharacter end