Principal Classes and Faithful Prime Counts

Abstract

The class map detects principality, while every integer prime count detects ideals.

Theorem 1.1 (The trivial ideal class is exactly the principal locus).

$$\begin{gathered} \forall R,K,I, \\ \mathrm{CommRing}\left(R\right)\wedge \mathrm{IsDomain}\left(R\right)\wedge \mathrm{Field}\left(K\right)\wedge \mathrm{Algebra}\left(R,K\right)\wedge \mathrm{IsFractionRing}\left(R,K\right)\Rightarrow (\mathrm{IsPrincipal}\left(\mathrm{Submodule}\left(R,K,I\right)\right)⟺\mathrm{ClassGroupMk}\left(K,I\right)=1). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/IdealClassGroups/PrincipalIdealCriterion.principal_ideal_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the orientation matching the source statement of Mathlib’s ClassGroup.mk_eq_one_iff. No Dedekind-domain assumption is added: the upstream interface requires a domain and a chosen field of fractions.

References

• Truth anchor: D5/S3/Factorization/IdealClassGroups/PrincipalIdealCriterion.principal_ideal_criterion