Documentation

Mathlib.RingTheory.Localization.Cardinality

Cardinality of localizations #

In this file, we establish the cardinality of localizations. In most cases, a localization has cardinality equal to the base ring. If there are zero-divisors, however, this is no longer true - for example, ZMod 6 localized at {2, 4} is equal to ZMod 3, and if you have zero in your submonoid, then your localization is trivial (see IsLocalization.uniqueOfZeroMem).

Main statements #

A localization always has cardinality less than or equal to the base ring.

theorem IsLocalization.card {R : Type u} [CommRing R] (L : Type u) [CommRing L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] (hS : S nonZeroDivisors R) :

If you do not localize at any zero-divisors, localization preserves cardinality.