English
The setoid on X × S used for Ore localization identifies fractions r/s and r'/s' exactly when there exist u ∈ S and v ∈ R with u·r' = v·r and u·s' = v·s.
Русский
Множество эквивалентности для Ore локализации на X × S идентифицирует дроби r/s и r'/s' тогда и только тогда, когда существуют u ∈ S и v ∈ R такие, что u r' = v r и u s' = v s.
LaTeX
$$$(r,s) \sim (r',s') \iff \exists u \in S, \exists v \in R, u \cdot r' = v \cdot r \wedge u \cdot s' = v \cdot s$$$
Lean4
/-- The setoid on `R × S` used for the Ore localization. -/
@[to_additive AddOreLocalization.oreEqv /-- The setoid on `R × S` used for the Ore localization. -/
]
def oreEqv : Setoid (X × S)
where
r rs rs' := ∃ (u : S) (v : R), u • rs'.1 = v • rs.1 ∧ u * rs'.2 = v * rs.2
iseqv := by
refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
· rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩; dsimp only at *
rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
have : r₃ * v * s = s₃ * s₂ * s := by
-- Porting note: the proof used `assoc_rw`
rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩ <;> simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
· simp only [mul_smul, hru, ← Submonoid.smul_def]
· simp only [mul_assoc, hsu]
· rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨r₃, s₃⟩ ⟨u, v, hur₁, hs₁u⟩ ⟨u', v', hur₂, hs₂u⟩
rcases oreCondition v' u with ⟨r', s', h⟩; dsimp only at *
refine ⟨s' * u', r' * v, ?_, ?_⟩ <;> simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
· rw [hur₂, smul_smul, h, mul_smul, hur₁]
· rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]
