oreDiv_one_surjective_of_finite_right

English

If X is finite, the map x ↦ x /ₒ (1 : ↥S) : X → OreLocalization S X is surjective.

Русский

Если X конечен, отображение x ↦ x /ₒ 1 на локализацию Оре сюръективно.

LaTeX

$$Surjective (x \\mapsto x /_\\ o 1) : X → OreLocalization S X, [Finite X]$$

Lean4

@[to_additive]
theorem oreDiv_one_surjective_of_finite_right [Finite X] :
    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 ^ · • x)
  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]

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