English
For a ring hom f: R → T that sends S to units of T, there exists a unique ring homomorphism OreLocalization S R → T extending f.
Русский
Для кольцевого гомоморфа f: R → T, отправляющего S в элементы-единицы T, существует единственный кольцевой гомоморфизм OreLocalization S R → T, продолжающий f.
LaTeX
$$universalHom : R[S^{-1}] →+* T$$
Lean4
instance {R₀} [CommSemiring R₀] [Algebra R₀ R] : Algebra R₀ R[S⁻¹]
where
__ := inferInstanceAs (Module R₀ R[S⁻¹])
algebraMap := numeratorRingHom.comp (algebraMap R₀ R)
commutes' r
x :=
by
induction x using OreLocalization.ind with
| _ r₁ s₁
dsimp
rw [mul_div_one, oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm, Algebra.commutes,
mul_one]
smul_def' r
x := by
dsimp
rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]
