The class group of a Unique Factorization Domain is trivial

This file proves that the ideal class group of a GCD Domain is trivial. The main application is to Unique Factorization Domains, which are known to be GCD Domains.

Main result

• IsGCDMonoid.subsingleton_classGroup : the class group of a GCD domain is trivial. This includes unique factorization domains.

References

• [stacks-project]: The Stacks project, tag 0BCH

theorem IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R} (hJ : ∃ (K : Ideal R), J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) : Submodule.IsPrincipal J

instance IsGCDMonoid.subsingleton_classGroup {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] : Subsingleton (ClassGroup R)

The ideal class group of a GCD domain is trivial. This includes unique factorization domains.

@[deprecated IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal (since := "2026-07-08")]

theorem NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R} (hJ : ∃ (K : Ideal R), J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) : Submodule.IsPrincipal J

Alias of IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal.