The class group of a Unique Factorization Domain is trivial

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

Main result

• NormalizedGCDMonoid.subsingleton_classGroup : the class group of a domain with normalizable gcd is trivial. This includes unique factorization domains.

References

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

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

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

The ideal class group of a domain with normalizable gcd is trivial. This includes unique factorization domains.