English
If every pair of elements in S commute, then #(OreLocalization S X) ≤ lift #X.
Русский
Если все пары элементов S commute, то #(OreLocalization S X) ≤ lift #X.
LaTeX
$$$ (\\forall s,s' : S, Commute s s') \\Rightarrow #(OreLocalization S X) \\le \\mathrm{lift}\n( #X ) $$$
Lean4
@[to_additive]
theorem cardinalMk_le_lift_cardinalMk_of_commute (hc : ∀ s s' : S, Commute s s') :
#(OreLocalization S X) ≤ lift.{u} #X :=
by
rcases finite_or_infinite X with _ | _
· have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
rwa [lift_umax.{v, u}, lift_id'] at this
have key (x : X) (s s' : S) (h : s • x = s' • x) (hc : Commute s s') : x /ₒ s = x /ₒ s' :=
by
rw [oreDiv_eq_iff]
refine ⟨s, s'.1, h, ?_⟩
· exact_mod_cast hc
let i (x : X × S) := x.1 /ₒ x.2
have hsurj : Surjective i := Quotient.mk''_surjective
have hi := rightInverse_surjInv hsurj
let j := (fun x : X × S ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
suffices Injective j by
have := lift_mk_le_lift_mk_of_injective this
rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this
intro y y' heq
rw [← hi y, ← hi y']
simp_rw [j, comp_apply, Prod.ext_iff] at heq
simp_rw [i]
set x := surjInv hsurj y
set x' := surjInv hsurj y'
obtain ⟨h1, h2⟩ := heq
rw [← h1] at h2 ⊢
exact key x.1 x.2 x'.2 h2 (hc _ _)
