English
There is a finite-type structure on the class group of the ring of integers of K.
Русский
Класс-группа кольца целых чисел поля K имеет структуру конечного типа.
LaTeX
$$$\\text{Fintype}(\\mathrm{ClassGroup}(\\mathcal O_K))$$$
Lean4
/-- If the measurable set `A` is norm-stable in the sense that
`normAtAllPlaces⁻¹ (normAtAllPlaces '' A) = A`, then its volume can be computed via an integral
over `normAtAllPlaces '' A`.
-/
theorem volume_eq_two_pow_mul_two_pi_pow_mul_integral [NumberField K]
(hA : normAtAllPlaces ⁻¹' (normAtAllPlaces '' A) = A) (hm : MeasurableSet A) :
volume A =
2 ^ nrRealPlaces K * .ofReal (2 * π) ^ nrComplexPlaces K *
∫⁻ x in normAtAllPlaces '' A, ∏ w : { w // IsComplex w }, ENNReal.ofReal (x w.1) :=
by
have hA₁ (x : mixedSpace K) : x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A :=
by
rw [← hA]
simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]
have hA₃ : normAtComplexPlaces ⁻¹' (normAtComplexPlaces '' (plusPart A)) = plusPart A :=
by
refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
· rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]
exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)
· have := funext_iff.mp ha₂ w
rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this
rw [← this]
exact ha₁.2 w
rw [volume_eq_two_pow_mul_volume_plusPart hA₁ hm, volume_eq_two_pi_pow_mul_integral hA₃ (measurableSet_plusPart hm), ←
mul_assoc]
refine congr_arg (_ * _ * ·) <| setLIntegral_congr ?_
rw [← volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux hA]
refine inter_ae_eq_left_of_ae_eq_univ <| ae_eq_univ.mpr <| Set.compl_iInter _ ▸ measure_iUnion_null_iff.mpr fun w ↦ ?_
rw [show {x : realSpace K | x w.1 ≠ 0}ᶜ = {x | x w.1 = 0} by ext; simp]
exact realSpace.volume_eq_zero w.1
