English
For s ∈ ℝ, the cardinality of principal ideals with norm ≤ s, times torsion order, equals the cardinality of integerSet elements with norm ≤ s.
Русский
Для s ∈ ℝ кардинал числа главных идеалов с нормой ≤ s, умноженный на порядок тorsion, равен кардиналу элементов integerSet с нормой ≤ s.
LaTeX
$$$\\operatorname{card\\_principal\\_norm\\_le}(K, s) \\cdot \\operatorname{torsionOrder}(K) = \\operatorname{card}\\{a:\\; a\\in \\text{integerSet}(K) : \\operatorname{mixedEmbedding.norm}(a) \\le s\\}$$$
Lean4
/-- For `s : ℝ`, the number of principal nonzero ideals in `𝓞 K` divisible par `J` of norm `≤ s`
multiplied by the order of the torsion of `K` is equal to the number of elements in `idealSet K J`
of norm `≤ s`. -/
theorem card_isPrincipal_dvd_norm_le (s : ℝ) :
Nat.card
{ I : (Ideal (𝓞 K))⁰ //
(J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) ≤ s } *
torsionOrder K =
Nat.card { a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ s } :=
by
obtain hs | hs := le_or_gt 0 s
· simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]
rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
refine
Nat.card_congr <|
@Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _ (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩)
(fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_
simp_rw [Subtype.mk.injEq]
calc
_ ≃ { I : { I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _ } // absNorm I.1.1 = i } × torsion K :=
Equiv.prodSubtypeFstEquivSubtypeProd
_ ≃ { I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i } × torsion K :=
(Equiv.prodCongrLeft fun _ ↦
(Equiv.subtypeSubtypeEquivSubtypeInter (p := fun I : (Ideal (𝓞 K))⁰ ↦
J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊) (q := fun I ↦ absNorm I.1 = i)))
_ ≃ { I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i } × torsion K :=
(Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by aesop)
_ ≃ { a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i } := (idealSetEquivNorm K J i).symm
_ ≃ { a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i } :=
by
simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
rfl
_ ≃
{ b : { a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊ } //
intNorm (idealSetEquiv K J b).1 = i } :=
(Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm
·
simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)),
lt_iff_not_ge.mp (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty, zero_mul]
