English
Let R be a semiring and S a multiplicative subset satisfying the Ore condition, with f : R →+* T and fS : S →* Units T such that f s = fS s for all s ∈ S. Then the universal hom from the Ore localization R[S⁻¹] to T sends the image of any r ∈ R to f(r).
Русский
Пусть R — полукольцо, S — умножимое множество, удовлетворяющее условию Ора, и заданы гомоморфизм f: R →+* T и моноидом-хомоморфизм fS: S →* Units T, такие что f s = fS s для всех s ∈ S. Тогда универсальный гомоморфин из локализации по Оре в T отправляет образ скобки r ∈ R в f(r).
LaTeX
$$$\\mathrm{universalHom}(f,f_S,hf)(\\mathrm{numeratorHom}(r)) = f(r)\\quad$ for all $r \\in R$$$
Lean4
theorem universalHom_commutes {r : R} : universalHom f fS hf (numeratorHom r) = f r := by
simp [numeratorHom_apply, universalHom_apply]
