Cardinality of Ore localizations

This file contains some results on cardinality of Ore localizations.

TODO

• Prove or disprove OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute with Commute assumption removed.

theorem OreLocalization.oreDiv_one_surjective_of_finite_left {R : Type u} [Monoid R] (S : Submonoid R) [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) [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) [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) [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) [OreSet S] [Finite ↥S] : Function.Surjective ⇑numeratorHom

theorem AddOreLocalization.numeratorHom_surjective_of_finite {R : Type u} [AddMonoid R] (S : AddSubmonoid R) [AddOreSet S] [Finite ↥S] : Function.Surjective ⇑numeratorHom

theorem OreLocalization.cardinalMk_le_max {R : Type u} [Monoid R] (S : Submonoid R) [OreSet S] (X : Type v) [MulAction R X] : Cardinal.mk (OreLocalization S X) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk ↥S)) (Cardinal.lift.{u, v} (Cardinal.mk X))

theorem AddOreLocalization.cardinalMk_le_max {R : Type u} [AddMonoid R] (S : AddSubmonoid R) [AddOreSet S] (X : Type v) [AddAction R X] : Cardinal.mk (AddOreLocalization S X) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk ↥S)) (Cardinal.lift.{u, v} (Cardinal.mk X))

theorem OreLocalization.cardinalMk_le {R : Type u} [Monoid R] (S : Submonoid R) [OreSet S] : Cardinal.mk (OreLocalization S R) ≤ Cardinal.mk R

theorem AddOreLocalization.cardinalMk_le {R : Type u} [AddMonoid R] (S : AddSubmonoid R) [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) [OreSet S] (X : Type v) [MulAction R X] (hc : ∀ (s s' : ↥S), Commute s s') : Cardinal.mk (OreLocalization S X) ≤ Cardinal.lift.{u, v} (Cardinal.mk X)

theorem AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute {R : Type u} [AddMonoid R] (S : AddSubmonoid R) [AddOreSet S] (X : Type v) [AddAction R X] (hc : ∀ (s s' : ↥S), AddCommute s s') : Cardinal.mk (AddOreLocalization S X) ≤ Cardinal.lift.{u, v} (Cardinal.mk X)