Ideals of prime-power norm as weighted multiplicity vectors

theorem NairTenenbaum.ideal_prime_power_product_count {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (e : Ideal (NumberField.RingOfIntegers K) → ℕ) (Q : Ideal (NumberField.RingOfIntegers K)) : Multiset.count Q (UniqueFactorizationMonoid.normalizedFactors (∏ P ∈ S, P ^ e P)) = if Q ∈ S then e Q else 0

noncomputable def NairTenenbaum.idealOfMultiplicities {K : Type u_1} [Field K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (e : ↥S → ℕ) : Ideal (NumberField.RingOfIntegers K)

The ideal obtained by multiplying prime ideals with specified multiplicities.

Equations

• NairTenenbaum.idealOfMultiplicities S e = ∏ P : ↥S, ↑P ^ e P

theorem NairTenenbaum.idealOfMultiplicities_count {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (e : ↥S → ℕ) (P : ↥S) : Multiset.count (↑P) (UniqueFactorizationMonoid.normalizedFactors (idealOfMultiplicities S e)) = e P

theorem NairTenenbaum.idealOfMultiplicities_factor_counts {K : Type u_1} [Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} (hI : I ≠ ⊥) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hs : (UniqueFactorizationMonoid.normalizedFactors I).toFinset ⊆ S) : (idealOfMultiplicities S fun (P : ↥S) => Multiset.count (↑P) (UniqueFactorizationMonoid.normalizedFactors I)) = I

theorem NairTenenbaum.idealOfMultiplicities_norm {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (e : ↥(primeIdealSupport K p) → ℕ) : Ideal.absNorm (idealOfMultiplicities (primeIdealSupport K p) e) = p ^ ∑ P : ↥(primeIdealSupport K p), (↑P).inertiaDeg ℤ * e P

noncomputable def NairTenenbaum.idealNormPrimePowerEquiv {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = p ^ k } ≃ { e : ↥(primeIdealSupport K p) → ℕ // ∑ P : ↥(primeIdealSupport K p), (↑P).inertiaDeg ℤ * e P = k }

Prime-power-norm ideals identified with weighted prime-ideal multiplicities.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.idealNormCount_prime_pow_eq_card_vectors {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : idealNormCount K (p ^ k) = Nat.card { e : ↥(primeIdealSupport K p) → ℕ // ∑ P : ↥(primeIdealSupport K p), (↑P).inertiaDeg ℤ * e P = k }