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.cardinalMk_le
{R : Type u}
[CommSemiring R]
{L : Type u}
[CommSemiring L]
[Algebra R L]
(S : Submonoid R)
[IsLocalization S L]
:
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]
:
Alias of IsLocalization.cardinalMk_le.
A localization always has cardinality less than or equal to the base ring.
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)
:
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)
:
Alias of IsLocalization.cardinalMk.
If you do not localize at any zero-divisors, localization preserves cardinality.
@[simp]
theorem
IsFractionRing.cardinalMk
(R : Type u)
[CommRing R]
(L : Type u)
[CommRing L]
[Algebra R L]
[IsFractionRing R L]
: