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

• IsLocalization.cardinalMk_le: A localization has cardinality no larger than the base ring.
• IsLocalization.cardinalMk: If you don't localize at zero-divisors, the localization of a ring has cardinality equal to its base ring.

theorem IsLocalization.lift_cardinalMk_le {R : Type u} [CommSemiring R] {L : Type v} [CommSemiring L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] : Cardinal.lift.{u, v} (Cardinal.mk L) ≤ Cardinal.lift.{v, u} (Cardinal.mk R)

theorem IsLocalization.cardinalMk_le {R : Type u} [CommSemiring R] {L : Type u} [CommSemiring L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] : Cardinal.mk L ≤ Cardinal.mk R

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

@[deprecated IsLocalization.cardinalMk_le (since := "2024-10-30")]

theorem IsLocalization.card_le {R : Type u} [CommSemiring R] {L : Type u} [CommSemiring L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] : Cardinal.mk L ≤ Cardinal.mk R

Alias of IsLocalization.cardinalMk_le.

---

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

theorem Localization.cardinalMk {R : Type u} [CommRing R] {S : Submonoid R} (hS : S ≤ nonZeroDivisors R) : Cardinal.mk (Localization S) = Cardinal.mk R

theorem IsLocalization.lift_cardinalMk {R : Type u} [CommRing R] (L : Type v) [CommRing L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] (hS : S ≤ nonZeroDivisors R) : Cardinal.lift.{u, v} (Cardinal.mk L) = Cardinal.lift.{v, u} (Cardinal.mk R)

theorem IsLocalization.cardinalMk {R : Type u} [CommRing R] (L : Type u) [CommRing L] [Algebra R L] (S : Submonoid R) [IsLocalization S L] (hS : S ≤ nonZeroDivisors R) : Cardinal.mk L = Cardinal.mk R

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

@[deprecated IsLocalization.cardinalMk (since := "2024-10-30")]

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) : Cardinal.mk L = Cardinal.mk R

Alias of IsLocalization.cardinalMk.

---

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

@[simp]

theorem Cardinal.mk_fractionRing (R : Type u) [CommRing R] : mk (FractionRing R) = mk R

theorem FractionRing.cardinalMk (R : Type u) [CommRing R] : Cardinal.mk (FractionRing R) = Cardinal.mk R

Alias of Cardinal.mk_fractionRing.

theorem IsFractionRing.lift_cardinalMk (R : Type u) [CommRing R] (L : Type v) [CommRing L] [Algebra R L] [IsFractionRing R L] : Cardinal.lift.{u, v} (Cardinal.mk L) = Cardinal.lift.{v, u} (Cardinal.mk R)

theorem IsFractionRing.cardinalMk (R : Type u) [CommRing R] (L : Type u) [CommRing L] [Algebra R L] [IsFractionRing R L] : Cardinal.mk L = Cardinal.mk R