Documentation

TauCeti.NumberTheory.ArithmeticDirichletSeries.Weight

Completely multiplicative ideal weights #

The completely multiplicative specializations of TauCeti.IdealArithmeticFunction.

A TauCeti.MultiplicativeIdealWeight K is a monoid-with-zero homomorphism Ideal (π“ž K) β†’*β‚€ β„‚ killing only finitely many height-one primes, and TauCeti.UnitaryIdealWeight K is the subtype of those whose values have modulus 1 away from that finite bad set. Using Mathlib's β†’*β‚€ vocabulary is what pins the zero-ideal law Ο‡ βŠ₯ = 0; the finiteness condition is what bounds the bad local factors of the Euler product.

Both carriers are degree one: the value at 𝔭 ^ n is forced to be Ο‡ 𝔭 ^ n. They are therefore deliberately too narrow for the ideal MΓΆbius function or for coefficient systems whose prime-power values are independent local data; those get separate carriers.

The good ideals of a weight are the ideals prime to its bad primes in the sense of Ideal.IsPrimeTo (from TauCeti.RingTheory.DedekindDomain.Ideal): nonzero and divisible by no prime of the set. Its induction principle Ideal.IsPrimeTo.induction_on factors a good ideal into good primes; this is the engine behind both TauCeti.MultiplicativeIdealWeight.apply_ne_zero_iff_isGood and TauCeti.UnitaryIdealWeight.norm_eq_one.

Main declarations #

Negative results #

Two negative results delimit the carriers. TauCeti.MultiplicativeIdealWeight.coe_ne_const_one says the everywhere-one function on all integral ideals underlies no weight, because β†’*β‚€ forces the value 0 at βŠ₯ β€” the everywhere-one function on the nonzero ideals is the trivial weight instead (TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_one). TauCeti.UnitaryIdealWeight.norm_normTwist_apply_ne_one says that a norm twist with Re z β‰  0 has modulus different from one at every ideal of absolute norm greater than one, so such twists live only in the general carrier.

References #

The general carrier of completely multiplicative ideal weights #

source
structure TauCeti.MultiplicativeIdealWeight (K : Type u_2) [Field K] [NumberField K] :
Type u_2

A multiplicative ideal weight on a number field K: a completely multiplicative complex-valued function on all integral ideals of π“ž K, packaged as a monoid-with-zero homomorphism Ideal (π“ž K) β†’*β‚€ β„‚, which kills only finitely many height-one primes.

Being a β†’*β‚€ forces the value 0 at the zero ideal βŠ₯ and the value 1 at ⊀; the finiteness condition is what makes the associated Euler product have finitely many bad local factors. This carrier is degree one: its value at a prime power 𝔭 ^ n is forced to be Ο‡ 𝔭 ^ n, so it excludes the ideal MΓΆbius function and any coefficient system whose prime-power values are independent local data.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.MultiplicativeIdealWeight.instFunLikeIdealRingOfIntegersComplex {K : Type u_1} [Field K] [NumberField K] :
    FunLike (MultiplicativeIdealWeight K) (Ideal (NumberField.RingOfIntegers K)) β„‚
    Equations
    source
    instance TauCeti.MultiplicativeIdealWeight.instMonoidWithZeroHomClassIdealRingOfIntegersComplex {K : Type u_1} [Field K] [NumberField K] :
    MonoidWithZeroHomClass (MultiplicativeIdealWeight K) (Ideal (NumberField.RingOfIntegers K)) β„‚
    source
    @[simp]
    theorem TauCeti.MultiplicativeIdealWeight.coe_toMonoidWithZeroHom {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
    ⇑χ.toMonoidWithZeroHom = ⇑χ
    source
    theorem TauCeti.MultiplicativeIdealWeight.ext {K : Type u_1} [Field K] [NumberField K] {Ο‡ ψ : MultiplicativeIdealWeight K} (h : βˆ€ (I : Ideal (NumberField.RingOfIntegers K)), Ο‡ I = ψ I) :
    Ο‡ = ψ
    source
    theorem TauCeti.MultiplicativeIdealWeight.ext_iff {K : Type u_1} [Field K] [NumberField K] {Ο‡ ψ : MultiplicativeIdealWeight K} :
    Ο‡ = ψ ↔ βˆ€ (I : Ideal (NumberField.RingOfIntegers K)), Ο‡ I = ψ I
    source
    @[simp]
    theorem TauCeti.MultiplicativeIdealWeight.apply_bot {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
    Ο‡ βŠ₯ = 0

    The zero-ideal law. Every multiplicative ideal weight kills the zero ideal, so no weight is the everywhere-one function on all ideals.

    source
    @[simp]
    theorem TauCeti.MultiplicativeIdealWeight.apply_top {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
    Ο‡ ⊀ = 1
    source
    theorem TauCeti.MultiplicativeIdealWeight.ext_heightOneSpectrum {K : Type u_1} [Field K] [NumberField K] {Ο‡ ψ : MultiplicativeIdealWeight K} (h : βˆ€ (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Ο‡ 𝔭.asIdeal = ψ 𝔭.asIdeal) :
    Ο‡ = ψ

    A multiplicative ideal weight is determined by its values at the height-one primes: every nonzero ideal of π“ž K is a product of them.

    source
    def TauCeti.MultiplicativeIdealWeight.badPrimes {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
    Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

    The bad primes of an ideal weight: the height-one primes it kills. This is a derived, canonically determined accessor, not extra data.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.MultiplicativeIdealWeight.mem_badPrimes {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} :
      𝔭 ∈ Ο‡.badPrimes ↔ Ο‡ 𝔭.asIdeal = 0
      source
      theorem TauCeti.MultiplicativeIdealWeight.finite_badPrimes {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
      Ο‡.badPrimes.Finite
      source
      @[reducible, inline]
      abbrev TauCeti.MultiplicativeIdealWeight.IsGood {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
      Prop

      An ideal is good for Ο‡ when it is prime to the bad primes of Ο‡. In particular a good ideal is nonzero, even when Ο‡ has no bad primes at all.

      Equations
      Instances For
        source
        theorem TauCeti.MultiplicativeIdealWeight.apply_ne_zero_iff_isGood {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
        Ο‡ I β‰  0 ↔ Ο‡.IsGood I

        A completely multiplicative ideal weight is nonzero exactly on the good ideals. Thus the good ideals are precisely the nonvanishing locus of the weight.

        source
        theorem TauCeti.MultiplicativeIdealWeight.apply_eq_zero_iff_not_isGood {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
        Ο‡ I = 0 ↔ ¬χ.IsGood I

        Constructors and operations #

        source
        noncomputable def TauCeti.MultiplicativeIdealWeight.ofBadPrimes {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) :
        MultiplicativeIdealWeight K

        The indicator weight of a finite set S of height-one primes: the value is 1 on the ideals prime to S and 0 elsewhere. Its bad primes are exactly S, and ofBadPrimes βˆ… is the trivial weight 1.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.ofBadPrimes_apply {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) (I : Ideal (NumberField.RingOfIntegers K)) :
          (ofBadPrimes S hS) I = if I.IsPrimeTo S then 1 else 0

          Defining equation of TauCeti.MultiplicativeIdealWeight.ofBadPrimes; its body is not exposed.

          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.badPrimes_ofBadPrimes {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) :
          (ofBadPrimes S hS).badPrimes = S
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.isGood_ofBadPrimes_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) {I : Ideal (NumberField.RingOfIntegers K)} :
          (ofBadPrimes S hS).IsGood I ↔ I.IsPrimeTo S
          source
          @[instance_reducible]
          noncomputable instance TauCeti.MultiplicativeIdealWeight.instMul {K : Type u_1} [Field K] [NumberField K] :
          Mul (MultiplicativeIdealWeight K)

          The pointwise product of two multiplicative ideal weights.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.mul_apply {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
          (Ο‡ * ψ) I = Ο‡ I * ψ I
          source
          @[instance_reducible]
          noncomputable instance TauCeti.MultiplicativeIdealWeight.instOne {K : Type u_1} [Field K] [NumberField K] :
          One (MultiplicativeIdealWeight K)

          The trivial multiplicative ideal weight.

          Equations
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.one_apply {K : Type u_1} [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) :
          1 I = if I = βŠ₯ then 0 else 1

          The trivial weight is the indicator of the nonzero ideals.

          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.badPrimes_one {K : Type u_1} [Field K] [NumberField K] :
          badPrimes 1 = βˆ…
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.badPrimes_mul {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : MultiplicativeIdealWeight K) :
          (Ο‡ * ψ).badPrimes = Ο‡.badPrimes βˆͺ ψ.badPrimes
          source
          @[instance_reducible]
          noncomputable instance TauCeti.MultiplicativeIdealWeight.instCommMonoid {K : Type u_1} [Field K] [NumberField K] :
          CommMonoid (MultiplicativeIdealWeight K)

          The pointwise product of multiplicative ideal weights, with the trivial weight as unit. It is not the Dirichlet convolution of ideal arithmetic functions, which is TauCeti.IdealArithmeticFunction.convolution.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.pow_apply {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) {n : β„•} (hn : n β‰  0) (I : Ideal (NumberField.RingOfIntegers K)) :
          (Ο‡ ^ n) I = Ο‡ I ^ n

          A positive power of a weight is computed pointwise. The exponent must be nonzero: Ο‡ ^ 0 is the trivial weight, which vanishes at βŠ₯, while Ο‡ βŠ₯ ^ 0 = 1.

          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.badPrimes_pow {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) {n : β„•} (hn : n β‰  0) :
          (Ο‡ ^ n).badPrimes = Ο‡.badPrimes

          A nonzero power of a weight kills exactly the primes the weight kills, so it has the same good ideals.

          source
          @[simp]
          theorem TauCeti.MultiplicativeIdealWeight.isGood_one_iff {K : Type u_1} [Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} :
          IsGood 1 I ↔ I β‰  βŠ₯
          source
          noncomputable def TauCeti.MultiplicativeIdealWeight.restrict {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) :
          MultiplicativeIdealWeight K

          Restriction away from a finite set of primes: Ο‡ is left unchanged on the ideals prime to S and set to 0 on the others.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.MultiplicativeIdealWeight.restrict_apply {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (Ο‡ : MultiplicativeIdealWeight K) (hS : S.Finite) (I : Ideal (NumberField.RingOfIntegers K)) :
            (Ο‡.restrict S hS) I = if I.IsPrimeTo S then Ο‡ I else 0
            source
            @[simp]
            theorem TauCeti.MultiplicativeIdealWeight.badPrimes_restrict {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (Ο‡ : MultiplicativeIdealWeight K) (hS : S.Finite) :
            (Ο‡.restrict S hS).badPrimes = Ο‡.badPrimes βˆͺ S
            source
            @[simp]
            theorem TauCeti.MultiplicativeIdealWeight.restrict_empty {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (hS : βˆ….Finite) :
            Ο‡.restrict βˆ… hS = Ο‡

            Restricting away from no prime at all changes nothing.

            source
            theorem TauCeti.MultiplicativeIdealWeight.restrict_insert_apply {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (Ο‡ : MultiplicativeIdealWeight K) {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hS : S.Finite) (I : Ideal (NumberField.RingOfIntegers K)) :
            (Ο‡.restrict (insert 𝔭 S) β‹―) I = if 𝔭.asIdeal ∣ I then 0 else (Ο‡.restrict S hS) I

            Forbidding one more prime. Restricting away from insert 𝔭 S kills the ideals divisible by 𝔭 and agrees with the restriction away from S on the others.

            source
            @[simp]
            theorem TauCeti.MultiplicativeIdealWeight.one_restrict {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) :
            restrict 1 S hS = ofBadPrimes S hS

            Restricting the trivial weight away from S gives the indicator weight of ideals prime to every prime in S.

            source
            @[simp]
            theorem TauCeti.MultiplicativeIdealWeight.restrict_pow {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (Ο‡ : MultiplicativeIdealWeight K) (hS : S.Finite) {n : β„•} (hn : n β‰  0) :
            (Ο‡ ^ n).restrict S hS = Ο‡.restrict S hS ^ n

            Restriction commutes with nonzero powers. The exponent must be nonzero: (Ο‡ ^ 0).restrict S hS is the indicator weight ofBadPrimes S hS, while Ο‡.restrict S hS ^ 0 is the trivial weight.

            source
            def TauCeti.MultiplicativeIdealWeight.conj {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
            MultiplicativeIdealWeight K

            The conjugate weight I ↦ conj (Ο‡ I).

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.conj_apply {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
              Ο‡.conj I = (starRingEnd β„‚) (Ο‡ I)
              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.badPrimes_conj {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
              Ο‡.conj.badPrimes = Ο‡.badPrimes
              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.conj_conj {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
              Ο‡.conj.conj = Ο‡
              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.conj_one {K : Type u_1} [Field K] [NumberField K] :
              conj 1 = 1
              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.conj_mul {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : MultiplicativeIdealWeight K) :
              (Ο‡ * ψ).conj = Ο‡.conj * ψ.conj

              Conjugation is multiplicative for the pointwise product.

              source
              @[simp]
              theorem TauCeti.MultiplicativeIdealWeight.conj_pow {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (n : β„•) :
              (Ο‡ ^ n).conj = Ο‡.conj ^ n

              Conjugation commutes with powers; in particular the conjugate of the pointwise square is the square of the conjugate.

              source
              noncomputable def TauCeti.MultiplicativeIdealWeight.normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) :
              MultiplicativeIdealWeight K

              The norm twist I ↦ Ο‡ I * N(I) ^ (-z). For general z this leaves the unitary carrier; only the purely imaginary twists preserve it (TauCeti.UnitaryIdealWeight.normTwist).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.normTwist_apply {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
                (normTwist z Ο‡) I = Ο‡ I * ↑(Ideal.absNorm I) ^ (-z)
                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.badPrimes_normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) :
                (normTwist z Ο‡).badPrimes = Ο‡.badPrimes
                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.normTwist_zero {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                normTwist 0 Ο‡ = Ο‡
                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.normTwist_normTwist {K : Type u_1} [Field K] [NumberField K] (z w : β„‚) (Ο‡ : MultiplicativeIdealWeight K) :
                normTwist z (normTwist w Ο‡) = normTwist (z + w) Ο‡

                Successive norm twists combine by adding their parameters.

                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.normTwist_mul_normTwist {K : Type u_1} [Field K] [NumberField K] (z w : β„‚) (Ο‡ ψ : MultiplicativeIdealWeight K) :
                normTwist z Ο‡ * normTwist w ψ = normTwist (z + w) (Ο‡ * ψ)

                The pointwise product of two norm twists is the twist of the product by the sum of the parameters.

                source
                @[simp]
                theorem TauCeti.MultiplicativeIdealWeight.normTwist_pow {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) (n : β„•) :
                normTwist z Ο‡ ^ n = normTwist (↑n * z) (Ο‡ ^ n)

                The n-th power of a norm twist is the twist of the n-th power by n times the parameter. For n = 2: the pointwise square of the twist of Ο‡ by N(I) ^ (-z) is the twist of Ο‡ ^ 2 by N(I) ^ (-2z).

                Weights that are norm twists on their good locus #

                source
                def TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (u : ℝ) :
                Prop

                A weight is a norm twist on its good ideals, with parameter u, when Ο‡ I = N(I) ^ (u * I) at every ideal I prime to its bad primes. Away from the bad primes such a weight is the purely imaginary norm twist TauCeti.MultiplicativeIdealWeight.normTwist of the trivial weight, and it is the whole of that twist once the bad primes are taken into account (TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.eq_normTwist).

                These weights give degenerate examples in families of ideal weights: their L-series is a Dedekind zeta function with finitely many Euler factors deleted, read after an imaginary translation, so it has a pole and no cancellation in its ideal partial sums (TauCeti.not_hasCancellation_of_isNormTwistOnGood).

                Equations
                Instances For
                  source
                  def TauCeti.MultiplicativeIdealWeight.IsTrivialOnGood {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                  Prop

                  A weight is trivial on its good ideals when it takes the value 1 at every ideal prime to its bad primes; equivalently it is a norm twist on its good ideals with parameter 0 (TauCeti.MultiplicativeIdealWeight.isNormTwistOnGood_zero_iff).

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.MultiplicativeIdealWeight.IsTrivialOnGood.apply_eq_one {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} (h : Ο‡.IsTrivialOnGood) {I : Ideal (NumberField.RingOfIntegers K)} (hI : Ο‡.IsGood I) :
                    Ο‡ I = 1

                    A weight trivial on its good ideals takes the value 1 at each of them.

                    source
                    @[simp]
                    theorem TauCeti.MultiplicativeIdealWeight.isNormTwistOnGood_zero_iff {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                    Ο‡.IsNormTwistOnGood 0 ↔ Ο‡.IsTrivialOnGood

                    The norm twists with parameter 0 on the good ideals are the weights that are trivial there.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.isTrivialOnGood_one {K : Type u_1} [Field K] [NumberField K] :
                    IsTrivialOnGood 1

                    The trivial weight is trivial on its good ideals, which are all the nonzero ideals.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.isTrivialOnGood_ofBadPrimes {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) :
                    (ofBadPrimes S hS).IsTrivialOnGood

                    The indicator of the ideals prime to a finite set S of primes is trivial on its good ideals, which are exactly those ideals.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.eq_normTwist {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {Ο‡ : MultiplicativeIdealWeight K} {u : ℝ} (h : Ο‡.IsNormTwistOnGood u) (hSbad : Ο‡.badPrimes = S) :
                    Ο‡ = MultiplicativeIdealWeight.normTwist (-(↑u * Complex.I)) (ofBadPrimes S β‹―)

                    A norm twist on the good ideals is a norm twist of an indicator weight. A weight that is a norm twist with parameter u on its good ideals is the twist by N(I) ^ (u * I) of the indicator of the ideals prime to its bad primes. The bad set is a parameter, so that a caller holding it as a Finset need not convert.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.normTwist {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} {u : ℝ} (h : Ο‡.IsNormTwistOnGood u) (v : ℝ) :
                    (MultiplicativeIdealWeight.normTwist (-(↑v * Complex.I)) Ο‡).IsNormTwistOnGood (u + v)

                    A twist adds to the parameter. Twisting by N(I) ^ (v * I) turns a norm twist with parameter u on the good ideals into one with parameter u + v; the good ideals are unchanged.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.isNormTwistOnGood_normTwist_ofBadPrimes {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) (u : ℝ) :
                    (normTwist (-(↑u * Complex.I)) (ofBadPrimes S hS)).IsNormTwistOnGood u

                    Converse of TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.eq_normTwist. The twist by N(I) ^ (u * I) of the indicator of the ideals prime to a finite set of primes is a norm twist with parameter u on its good ideals.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.conj {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} {u : ℝ} (h : Ο‡.IsNormTwistOnGood u) :
                    Ο‡.conj.IsNormTwistOnGood (-u)

                    Conjugation negates the parameter of a norm twist on the good ideals.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.mul {K : Type u_1} [Field K] [NumberField K] {Ο‡ ψ : MultiplicativeIdealWeight K} {u v : ℝ} (hΟ‡ : Ο‡.IsNormTwistOnGood u) (hψ : ψ.IsNormTwistOnGood v) :
                    (Ο‡ * ψ).IsNormTwistOnGood (u + v)

                    The pointwise product adds the parameters of two norm twists on the good ideals. Both factors are good at every ideal good for the product, since the bad primes of a product are the union of those of its factors.

                    source
                    theorem TauCeti.MultiplicativeIdealWeight.IsNormTwistOnGood.pow {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} {u : ℝ} (h : Ο‡.IsNormTwistOnGood u) (n : β„•) :
                    (Ο‡ ^ n).IsNormTwistOnGood (↑n * u)

                    The n-th power multiplies the parameter by n for a norm twist on the good ideals. For n = 2 this identifies the pointwise square of such a weight as a norm twist with parameter 2u on its good ideals.

                    Passage to the general carrier, and the zero-ideal rejection test #

                    source
                    def TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                    IdealArithmeticFunction K

                    The ideal arithmetic function underlying an ideal weight: its restriction to the nonzero ideals.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_apply {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) (I : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
                      Ο‡.toIdealArithmeticFunction I = Ο‡ ↑I
                      source
                      theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) :
                      (normTwist z Ο‡).toIdealArithmeticFunction = fun (I : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Ο‡.toIdealArithmeticFunction I * ↑(Ideal.absNorm ↑I) ^ (-z)

                      The ideal arithmetic function underlying a norm twist multiplies by N(I) ^ (-z).

                      source
                      @[simp]
                      theorem TauCeti.MultiplicativeIdealWeight.normCoeff_normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) (n : β„•) :
                      ((normCoeff K) (normTwist z Ο‡).toIdealArithmeticFunction) n = ((normCoeff K) Ο‡.toIdealArithmeticFunction) n * ↑n ^ (-z)

                      Regrouping absorbs a norm twist. Twisting a weight by N(I) ^ (-z) twists its n-th norm coefficient by n ^ (-z).

                      source
                      theorem TauCeti.MultiplicativeIdealWeight.isMultiplicative_toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                      Ο‡.toIdealArithmeticFunction.IsMultiplicative

                      The ideal arithmetic function underlying a completely multiplicative ideal weight is multiplicative on relatively prime ideals.

                      source
                      @[simp]
                      theorem TauCeti.MultiplicativeIdealWeight.zeroExtend_toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                      Ο‡.toIdealArithmeticFunction.zeroExtend = ⇑χ

                      An ideal weight is recovered from its restriction to the nonzero ideals by extending by zero: the zero-ideal law Ο‡ βŠ₯ = 0 is exactly what makes this work.

                      source
                      theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_injective {K : Type u_1} [Field K] [NumberField K] :
                      Function.Injective toIdealArithmeticFunction
                      source
                      @[simp]
                      theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_one {K : Type u_1} [Field K] [NumberField K] :
                      toIdealArithmeticFunction 1 = 1
                      source
                      @[simp]
                      theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_mul {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : MultiplicativeIdealWeight K) :
                      (Ο‡ * ψ).toIdealArithmeticFunction = Ο‡.toIdealArithmeticFunction * ψ.toIdealArithmeticFunction
                      source
                      theorem TauCeti.MultiplicativeIdealWeight.coe_ne_const_one {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                      ⇑χ β‰  Function.const (Ideal (NumberField.RingOfIntegers K)) 1

                      Rejection test. The everywhere-one function on all integral ideals underlies no multiplicative ideal weight, since Ideal (π“ž K) β†’*β‚€ β„‚ forces the value 0 at βŠ₯. The everywhere-one function on the nonzero ideals is the trivial weight (TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_one).

                      Functoriality under an isomorphism of fields #

                      source
                      noncomputable def TauCeti.MultiplicativeIdealWeight.map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) :
                      MultiplicativeIdealWeight L

                      Transport along an isomorphism of fields. An isomorphism e : K ≃+* L carries a multiplicative ideal weight on K to one on L, by pulling ideals of π“ž L back to π“ž K along NumberField.RingOfIntegers.mapRingEquiv e.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.map_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) (I : Ideal (NumberField.RingOfIntegers L)) :
                        (map e Ο‡) I = Ο‡ (Ideal.comap (NumberField.RingOfIntegers.mapRingEquiv e) I)
                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.badPrimes_map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) :
                        (map e Ο‡).badPrimes = ⇑(IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) '' Ο‡.badPrimes

                        The bad primes transport too: they are carried along by the induced bijection of height-one spectra.

                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.toIdealArithmeticFunction_map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) :
                        (map e Ο‡).toIdealArithmeticFunction = IdealArithmeticFunction.map e Ο‡.toIdealArithmeticFunction
                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.map_id {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) :
                        map (RingEquiv.refl K) Ο‡ = Ο‡
                        source
                        theorem TauCeti.MultiplicativeIdealWeight.map_map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} {M : Type u_3} [Field L] [NumberField L] [Field M] [NumberField M] (e : K ≃+* L) (e' : L ≃+* M) (Ο‡ : MultiplicativeIdealWeight K) :
                        map e' (map e Ο‡) = map (e.trans e') Ο‡

                        Transport is functorial: transporting along e and then along e' is the same as transporting along e.trans e'.

                        Transport preserves the pointwise CommMonoid structure.

                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.map_one {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) :
                        map e 1 = 1
                        source
                        @[simp]
                        theorem TauCeti.MultiplicativeIdealWeight.map_mul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ ψ : MultiplicativeIdealWeight K) :
                        map e (Ο‡ * ψ) = map e Ο‡ * map e ψ
                        source
                        noncomputable def TauCeti.MultiplicativeIdealWeight.mapEquiv {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) :
                        MultiplicativeIdealWeight K ≃* MultiplicativeIdealWeight L

                        Transport along an isomorphism of fields, as a multiplicative equivalence of the two carriers, with inverse the transport along e.symm.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.mapEquiv_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) :
                          (mapEquiv e) Ο‡ = map e Ο‡
                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.mapEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight L) :
                          (mapEquiv e).symm Ο‡ = map e.symm Ο‡
                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.map_ofBadPrimes {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (e : K ≃+* L) (hS : S.Finite) :
                          map e (ofBadPrimes S hS) = ofBadPrimes (⇑(IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) '' S) β‹―

                          Transport carries an indicator weight to the indicator of the image prime set.

                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.map_restrict {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) (hS : S.Finite) :
                          map e (Ο‡.restrict S hS) = (map e Ο‡).restrict (⇑(IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) '' S) β‹―

                          Transport commutes with restriction after carrying the excluded prime set forward.

                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.map_conj {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : MultiplicativeIdealWeight K) :
                          map e Ο‡.conj = (map e Ο‡).conj

                          Transport commutes with complex conjugation.

                          source
                          @[simp]
                          theorem TauCeti.MultiplicativeIdealWeight.map_normTwist {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (z : β„‚) (Ο‡ : MultiplicativeIdealWeight K) :
                          map e (normTwist z Ο‡) = normTwist z (map e Ο‡)

                          Transport commutes with norm twists because absolute ideal norm is invariant under a ring equivalence.

                          The unitary subtype #

                          source
                          @[reducible, inline]
                          abbrev TauCeti.UnitaryIdealWeight (K : Type u_2) [Field K] [NumberField K] :
                          Type u_2

                          A unitary ideal weight: a multiplicative ideal weight whose values have modulus 1 away from its bad primes. Finite-order Hecke characters land here (TauCeti.UnitaryIdealWeight.ofPowEqOne), and so do the purely imaginary norm twists (TauCeti.UnitaryIdealWeight.normTwist); a norm twist with Re z β‰  0 does not (TauCeti.UnitaryIdealWeight.norm_normTwist_apply_ne_one).

                          Equations
                          Instances For
                            source
                            theorem TauCeti.UnitaryIdealWeight.norm_eq_one {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) {I : Ideal (NumberField.RingOfIntegers K)} (hI : (↑χ).IsGood I) :
                            ‖↑χ Iβ€– = 1

                            A unitary weight has modulus one on every good ideal, extending its defining condition from good primes to the entire good-ideal locus.

                            source
                            theorem TauCeti.UnitaryIdealWeight.norm_le_one {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (I : Ideal (NumberField.RingOfIntegers K)) :
                            ‖↑χ Iβ€– ≀ 1

                            A unitary weight is bounded by one on every ideal. The bound is unconditional: it carries no goodness hypothesis, so a comparison indexed by all of (Ideal (π“ž K))⁰ can apply it termwise. norm_eq_one is sharper where it applies, but obliges the caller to split that index type first; this is the form a convergence estimate wants.

                            source
                            theorem TauCeti.MultiplicativeIdealWeight.IsTrivialOnGood.norm_apply_le_one {K : Type u_1} [Field K] [NumberField K] {Ο‡ : MultiplicativeIdealWeight K} (h : Ο‡.IsTrivialOnGood) {I : Ideal (NumberField.RingOfIntegers K)} :
                            β€–Ο‡ Iβ€– ≀ 1

                            A weight trivial on its good ideals is unitary, so it is bounded by one on every ideal (TauCeti.UnitaryIdealWeight.norm_le_one).

                            source
                            @[instance_reducible]
                            noncomputable instance TauCeti.UnitaryIdealWeight.instOne {K : Type u_1} [Field K] [NumberField K] :
                            One (UnitaryIdealWeight K)

                            The trivial weight is unitary.

                            Equations
                            source
                            @[simp]
                            theorem TauCeti.UnitaryIdealWeight.val_one {K : Type u_1} [Field K] [NumberField K] :
                            ↑1 = 1
                            source
                            @[instance_reducible]
                            noncomputable instance TauCeti.UnitaryIdealWeight.instMul {K : Type u_1} [Field K] [NumberField K] :
                            Mul (UnitaryIdealWeight K)

                            The pointwise product of unitary weights is unitary.

                            Equations
                            source
                            @[simp]
                            theorem TauCeti.UnitaryIdealWeight.val_mul {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : UnitaryIdealWeight K) :
                            ↑(Ο‡ * ψ) = ↑χ * β†‘Οˆ
                            source
                            @[instance_reducible]
                            noncomputable instance TauCeti.UnitaryIdealWeight.instCommMonoid {K : Type u_1} [Field K] [NumberField K] :
                            CommMonoid (UnitaryIdealWeight K)

                            Pointwise multiplication makes the unitary weights a commutative monoid.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            source
                            @[simp]
                            theorem TauCeti.UnitaryIdealWeight.val_pow {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (n : β„•) :
                            ↑(Ο‡ ^ n) = ↑χ ^ n
                            source
                            def TauCeti.UnitaryIdealWeight.ofPowEqOne {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) {n : β„•} (hn : n β‰  0) (h : βˆ€ 𝔭 βˆ‰ Ο‡.badPrimes, Ο‡ 𝔭.asIdeal ^ n = 1) :
                            UnitaryIdealWeight K

                            Finite-order weights are unitary. If a positive power of Ο‡ takes the value 1 at every good prime β€” as for a finite-order Hecke character β€” then Ο‡ is unitary.

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem TauCeti.UnitaryIdealWeight.val_ofPowEqOne {K : Type u_1} [Field K] [NumberField K] (Ο‡ : MultiplicativeIdealWeight K) {n : β„•} (hn : n β‰  0) (h : βˆ€ 𝔭 βˆ‰ Ο‡.badPrimes, Ο‡ 𝔭.asIdeal ^ n = 1) :
                              ↑(ofPowEqOne Ο‡ hn h) = Ο‡
                              source
                              noncomputable def TauCeti.UnitaryIdealWeight.normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (hz : z.re = 0) (Ο‡ : UnitaryIdealWeight K) :
                              UnitaryIdealWeight K

                              Imaginary norm twists preserve unitarity. For Re z = 0 the factor N(I) ^ (-z) has modulus 1, so the twisted weight is again unitary.

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem TauCeti.UnitaryIdealWeight.val_normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (hz : z.re = 0) (Ο‡ : UnitaryIdealWeight K) :
                                ↑(normTwist z hz Ο‡) = MultiplicativeIdealWeight.normTwist z ↑χ
                                source
                                @[simp]
                                theorem TauCeti.UnitaryIdealWeight.normTwist_zero {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                normTwist 0 normTwist_zero._proof_1 Ο‡ = Ο‡

                                The zero norm twist acts trivially on unitary weights.

                                source
                                @[simp]
                                theorem TauCeti.UnitaryIdealWeight.normTwist_normTwist {K : Type u_1} [Field K] [NumberField K] (z w : β„‚) (hz : z.re = 0) (hw : w.re = 0) (Ο‡ : UnitaryIdealWeight K) :
                                normTwist z hz (normTwist w hw Ο‡) = normTwist (z + w) β‹― Ο‡

                                Successive imaginary norm twists of a unitary weight combine by adding their parameters.

                                source
                                @[simp]
                                theorem TauCeti.UnitaryIdealWeight.normTwist_mul_normTwist {K : Type u_1} [Field K] [NumberField K] (z w : β„‚) (hz : z.re = 0) (hw : w.re = 0) (Ο‡ ψ : UnitaryIdealWeight K) :
                                normTwist z hz Ο‡ * normTwist w hw ψ = normTwist (z + w) β‹― (Ο‡ * ψ)

                                The pointwise product of two imaginary norm twists of unitary weights is the twist of the product by the sum of the parameters.

                                source
                                @[simp]
                                theorem TauCeti.UnitaryIdealWeight.normTwist_pow {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (hz : z.re = 0) (Ο‡ : UnitaryIdealWeight K) (n : β„•) :
                                normTwist z hz Ο‡ ^ n = normTwist (↑n * z) β‹― (Ο‡ ^ n)

                                The n-th power of an imaginary norm twist of a unitary weight is the twist of the n-th power by n times the parameter.

                                source
                                theorem TauCeti.UnitaryIdealWeight.norm_normTwist {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (z : β„‚) {I : Ideal (NumberField.RingOfIntegers K)} (hI : (↑χ).IsGood I) :
                                β€–(MultiplicativeIdealWeight.normTwist z ↑χ) Iβ€– = ↑(Ideal.absNorm I) ^ (-z.re)

                                The modulus of an arbitrary norm twist. At a good ideal, twisting a unitary weight by z gives modulus N(I) ^ (-Re z); only the purely imaginary twists therefore stay unitary.

                                source
                                theorem TauCeti.UnitaryIdealWeight.norm_normTwist_apply_ne_one {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) {z : β„‚} (hz : z.re β‰  0) {I : Ideal (NumberField.RingOfIntegers K)} (hN : 1 < Ideal.absNorm I) :
                                β€–(MultiplicativeIdealWeight.normTwist z ↑χ) Iβ€– β‰  1

                                Rejection test. A norm twist with Re z β‰  0 leaves the unitary carrier: at every ideal of absolute norm greater than one its modulus differs from 1, being N(I) ^ (-Re z) at a good ideal and 0 elsewhere. Such twists therefore live only in TauCeti.MultiplicativeIdealWeight.

                                source
                                def TauCeti.UnitaryIdealWeight.conj {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                UnitaryIdealWeight K

                                The conjugate of a unitary weight is unitary.

                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem TauCeti.UnitaryIdealWeight.val_conj {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                  ↑χ.conj = (↑χ).conj
                                  source
                                  @[simp]
                                  theorem TauCeti.UnitaryIdealWeight.conj_one {K : Type u_1} [Field K] [NumberField K] :
                                  conj 1 = 1
                                  source
                                  @[simp]
                                  theorem TauCeti.UnitaryIdealWeight.conj_mul {K : Type u_1} [Field K] [NumberField K] (Ο‡ ψ : UnitaryIdealWeight K) :
                                  (Ο‡ * ψ).conj = Ο‡.conj * ψ.conj

                                  Conjugation of unitary weights is multiplicative for the pointwise product.

                                  source
                                  @[simp]
                                  theorem TauCeti.UnitaryIdealWeight.conj_pow {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (n : β„•) :
                                  (Ο‡ ^ n).conj = Ο‡.conj ^ n

                                  Conjugation of unitary weights commutes with powers, in particular with the pointwise square.

                                  source
                                  noncomputable def TauCeti.UnitaryIdealWeight.restrict {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) :
                                  UnitaryIdealWeight K

                                  Restricting a unitary weight away from a finite set of primes keeps it unitary: the restricted weight is unchanged at the primes that are good for it.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem TauCeti.UnitaryIdealWeight.val_restrict {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) :
                                    ↑(Ο‡.restrict S hS) = (↑χ).restrict S hS
                                    source
                                    @[simp]
                                    theorem TauCeti.UnitaryIdealWeight.restrict_empty {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (hS : βˆ….Finite) :
                                    Ο‡.restrict βˆ… hS = Ο‡

                                    Restricting a unitary weight away from no prime at all changes nothing.

                                    source
                                    @[simp]
                                    theorem TauCeti.UnitaryIdealWeight.restrict_pow {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) {n : β„•} (hn : n β‰  0) :
                                    (Ο‡ ^ n).restrict S hS = Ο‡.restrict S hS ^ n

                                    Restriction of unitary weights commutes with nonzero powers, in particular with the pointwise square. As for TauCeti.MultiplicativeIdealWeight.restrict_pow, the exponent 0 is excluded.

                                    source
                                    noncomputable def TauCeti.UnitaryIdealWeight.map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight K) :
                                    UnitaryIdealWeight L

                                    Transport along an isomorphism of fields preserves unitarity: the transported weight has the same values as Ο‡, read off at the corresponding primes.

                                    Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem TauCeti.UnitaryIdealWeight.val_map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight K) :
                                      ↑(map e Ο‡) = MultiplicativeIdealWeight.map e ↑χ
                                      source
                                      @[simp]
                                      theorem TauCeti.UnitaryIdealWeight.map_id {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                      map (RingEquiv.refl K) Ο‡ = Ο‡
                                      source
                                      theorem TauCeti.UnitaryIdealWeight.map_map {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} {M : Type u_3} [Field L] [NumberField L] [Field M] [NumberField M] (e : K ≃+* L) (e' : L ≃+* M) (Ο‡ : UnitaryIdealWeight K) :
                                      map e' (map e Ο‡) = map (e.trans e') Ο‡

                                      Transport is functorial on the unitary carrier as well.

                                      Transport preserves the pointwise CommMonoid structure of the unitary carrier too.

                                      source
                                      @[simp]
                                      theorem TauCeti.UnitaryIdealWeight.map_one {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) :
                                      map e 1 = 1
                                      source
                                      @[simp]
                                      theorem TauCeti.UnitaryIdealWeight.map_mul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ ψ : UnitaryIdealWeight K) :
                                      map e (Ο‡ * ψ) = map e Ο‡ * map e ψ
                                      source
                                      noncomputable def TauCeti.UnitaryIdealWeight.mapEquiv {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) :
                                      UnitaryIdealWeight K ≃* UnitaryIdealWeight L

                                      Transport along an isomorphism of fields, as a multiplicative equivalence of the unitary carriers.

                                      Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem TauCeti.UnitaryIdealWeight.mapEquiv_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight K) :
                                        (mapEquiv e) Ο‡ = map e Ο‡
                                        source
                                        @[simp]
                                        theorem TauCeti.UnitaryIdealWeight.mapEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight L) :
                                        (mapEquiv e).symm Ο‡ = map e.symm Ο‡
                                        source
                                        @[simp]
                                        theorem TauCeti.UnitaryIdealWeight.map_restrict {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight K) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Finite) :
                                        map e (Ο‡.restrict S hS) = (map e Ο‡).restrict (⇑(IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) '' S) β‹―

                                        Transport commutes with restriction on unitary weights after carrying the excluded prime set forward.

                                        source
                                        @[simp]
                                        theorem TauCeti.UnitaryIdealWeight.map_conj {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (Ο‡ : UnitaryIdealWeight K) :
                                        map e Ο‡.conj = (map e Ο‡).conj

                                        Transport commutes with complex conjugation on unitary weights.

                                        source
                                        @[simp]
                                        theorem TauCeti.UnitaryIdealWeight.map_normTwist {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (z : β„‚) (hz : z.re = 0) (Ο‡ : UnitaryIdealWeight K) :
                                        map e (normTwist z hz Ο‡) = normTwist z hz (map e Ο‡)

                                        Transport commutes with purely imaginary norm twists on unitary weights.

                                        source
                                        def TauCeti.UnitaryIdealWeight.toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                        IdealArithmeticFunction K

                                        The ideal arithmetic function underlying a unitary weight: the restriction of the underlying multiplicative weight to the nonzero ideals.

                                        Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem TauCeti.UnitaryIdealWeight.toIdealArithmeticFunction_apply {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) (I : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
                                          Ο‡.toIdealArithmeticFunction I = ↑χ ↑I
                                          source
                                          theorem TauCeti.UnitaryIdealWeight.toIdealArithmeticFunction_eq_val {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                          Ο‡.toIdealArithmeticFunction = (↑χ).toIdealArithmeticFunction

                                          The ideal arithmetic function of a unitary weight agrees with that of its underlying multiplicative weight.

                                          source
                                          @[simp]
                                          theorem TauCeti.UnitaryIdealWeight.normCoeff_normTwist {K : Type u_1} [Field K] [NumberField K] (z : β„‚) (hz : z.re = 0) (Ο‡ : UnitaryIdealWeight K) (n : β„•) :
                                          ((normCoeff K) (normTwist z hz Ο‡).toIdealArithmeticFunction) n = ((normCoeff K) Ο‡.toIdealArithmeticFunction) n * ↑n ^ (-z)

                                          Regrouping absorbs an imaginary norm twist. For z.re = 0, twisting a unitary weight by N(I) ^ (-z) multiplies its n-th norm coefficient by n ^ (-z).

                                          source
                                          theorem TauCeti.UnitaryIdealWeight.isMultiplicative_toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                          Ο‡.toIdealArithmeticFunction.IsMultiplicative

                                          The ideal arithmetic function underlying a unitary ideal weight is multiplicative on relatively prime ideals.

                                          source
                                          @[simp]
                                          theorem TauCeti.UnitaryIdealWeight.zeroExtend_toIdealArithmeticFunction {K : Type u_1} [Field K] [NumberField K] (Ο‡ : UnitaryIdealWeight K) :
                                          Ο‡.toIdealArithmeticFunction.zeroExtend = ⇑↑χ

                                          A unitary weight is recovered from its underlying ideal arithmetic function by extending by zero, just as in TauCeti.MultiplicativeIdealWeight.zeroExtend_toIdealArithmeticFunction.

                                          source
                                          @[simp]
                                          theorem TauCeti.UnitaryIdealWeight.toIdealArithmeticFunction_one {K : Type u_1} [Field K] [NumberField K] :
                                          toIdealArithmeticFunction 1 = 1

                                          The trivial unitary weight restricts to the constant-one ideal arithmetic function.

                                          source
                                          theorem TauCeti.UnitaryIdealWeight.toIdealArithmeticFunction_injective {K : Type u_1} [Field K] [NumberField K] :
                                          Function.Injective toIdealArithmeticFunction

                                          A unitary weight is determined by its ideal arithmetic function.