oreDiv_one_surjective_of_finite_left

English

If all pairs s, s' in S commute, then #(OreLocalization S X) ≤ lift #X.

Русский

Если все пары s, s' из S коммутируют, то кардинал локализации не превосходит подъём кардинала X.

LaTeX

$$If hc: ∀ s s' : S, Commute s s' then #(OreLocalization S X) ≤ lift #X$$

Lean4

@[to_additive]
theorem oreDiv_one_surjective_of_finite_left [Finite S] :
    Surjective (fun x ↦ x /ₒ (1 : ↥S) : X → OreLocalization S X) :=
  by
  refine OreLocalization.ind fun x s ↦ ?_
  obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ ·)
  wlog hlt : j < i generalizing i j
  · exact this j i hne.symm heq.symm (hne.lt_of_le (not_lt.1 hlt))
  use s ^ (i - (j + 1)) • x
  rw [oreDiv_eq_iff]
  refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
  · change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
  · simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

Похожие утверждения