Cardinality of Ore localizations #
This file contains some results on cardinality of Ore localizations.
TODO #
- Prove or disprove
OreLocalization.cardinalMk_le_lift_cardinalMk_of_commutewithCommuteassumption removed.
theorem
OreLocalization.oreDiv_one_surjective_of_finite_left
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
(X : Type v)
[MulAction R X]
[Finite ↥S]
:
Function.Surjective fun (x : X) => x /ₒ 1
theorem
AddOreLocalization.oreSub_zero_surjective_of_finite_left
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
(X : Type v)
[AddAction R X]
[Finite ↥S]
:
Function.Surjective fun (x : X) => x -ₒ 0
theorem
OreLocalization.oreDiv_one_surjective_of_finite_right
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
(X : Type v)
[MulAction R X]
[Finite X]
:
Function.Surjective fun (x : X) => x /ₒ 1
theorem
AddOreLocalization.oreSub_zero_surjective_of_finite_right
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
(X : Type v)
[AddAction R X]
[Finite X]
:
Function.Surjective fun (x : X) => x -ₒ 0
theorem
OreLocalization.numeratorHom_surjective_of_finite
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
[Finite ↥S]
:
Function.Surjective ⇑OreLocalization.numeratorHom
theorem
AddOreLocalization.numeratorHom_surjective_of_finite
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
[Finite ↥S]
:
Function.Surjective ⇑AddOreLocalization.numeratorHom
theorem
OreLocalization.cardinalMk_le_max
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
(X : Type v)
[MulAction R X]
:
theorem
AddOreLocalization.cardinalMk_le_max
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
(X : Type v)
[AddAction R X]
:
theorem
OreLocalization.cardinalMk_le
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
:
Cardinal.mk (OreLocalization S R) ≤ Cardinal.mk R
theorem
AddOreLocalization.cardinalMk_le
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
:
Cardinal.mk (AddOreLocalization S R) ≤ Cardinal.mk R
theorem
OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute
{R : Type u}
[Monoid R]
(S : Submonoid R)
[OreLocalization.OreSet S]
(X : Type v)
[MulAction R X]
(hc : ∀ (s s' : ↥S), Commute s s')
:
theorem
AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute
{R : Type u}
[AddMonoid R]
(S : AddSubmonoid R)
[AddOreLocalization.AddOreSet S]
(X : Type v)
[AddAction R X]
(hc : ∀ (s s' : ↥S), AddCommute s s')
: