English
Under algebraicity and admissibility, the class group is finite.
Русский
При алгебраичности и допустимости класс-группа конечна.
LaTeX
$$$ \\text{Fintype}(\\mathrm{ClassGroup}(S)) $ under algebraic and admissible$$
Lean4
/-- The main theorem: the class group of an integral closure `S` of `R` in a
finite extension `L` of `K = Frac(R)` is finite if there is an admissible
absolute value.
See also `ClassGroup.fintypeOfAdmissibleOfAlgebraic` where `L` is an
algebraic extension of `R`, that includes some extra assumptions.
-/
noncomputable def fintypeOfAdmissibleOfFinite [IsIntegralClosure S R L] : Fintype (ClassGroup S) :=
by
letI := Classical.decEq L
letI := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
letI := IsIntegralClosure.isDedekindDomain R K L S
choose s b hb_int using FiniteDimensional.exists_is_basis_integral R K L
have : LinearIndependent R ((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) b) :=
by
apply (Basis.linearIndependent _).restrict_scalars
simp only [Algebra.smul_def, mul_one]
apply IsFractionRing.injective
obtain ⟨n, b⟩ := Submodule.basisOfPidOfLESpan this (IsIntegralClosure.range_le_span_dualBasis S b hb_int)
let f : (S ⧸ LinearMap.ker (LinearMap.restrictScalars R (Algebra.linearMap S L))) ≃ₗ[R] S :=
by
rw [LinearMap.ker_eq_bot.mpr]
· exact Submodule.quotEquivOfEqBot _ rfl
· exact IsIntegralClosure.algebraMap_injective _ R _
let bS := b.map ((LinearMap.quotKerEquivRange _).symm ≪≫ₗ f)
have : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
exact fintypeOfAdmissibleOfAlgebraic bS adm
