English
If there is an admissible absolute value and the extension is finite, then the class group is finite.
Русский
Если существует допустимая абсолютная величина и расширение конечное, то класс-группа конечна.
LaTeX
$$Fintype (ClassGroup S) under finite extension and admissible abv$$
Lean4
/-- The **class number theorem**: the class group of an integral closure `S` of `R` in an
algebraic extension `L` is finite if there is an admissible absolute value.
See also `ClassGroup.fintypeOfAdmissibleOfFinite` where `L` is a finite
extension of `K = Frac(R)`, supplying most of the required assumptions automatically.
-/
noncomputable def fintypeOfAdmissibleOfAlgebraic [IsDedekindDomain S] [Algebra.IsAlgebraic R S] :
Fintype (ClassGroup S) :=
@Fintype.ofSurjective _ _ _
(@Fintype.ofEquiv _ { J // J ∣ Ideal.span ({algebraMap R S (∏ m ∈ finsetApprox bS adm, m)} : Set S) }
(UniqueFactorizationMonoid.fintypeSubtypeDvd _
(by
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
exact prod_finsetApprox_ne_zero bS adm))
((Equiv.refl _).subtypeEquiv fun I =>
Ideal.dvd_iff_le.trans (by rw [Equiv.refl_apply, Ideal.span_le, Set.singleton_subset_iff]; rfl)))
(ClassGroup.mkMMem bS adm) (ClassGroup.mkMMem_surjective bS adm)
