English
A variant form of the uniqueness statement for universalMulHom, ensuring that any homomorphism agreeing on numerator elements must be equal to the universal lift.
Русский
Вариант формы утверждения об уникальности для universalMulHom, гарантирующий, что любой гомоморфизм, совпадающий на числителях, равен универсальному подъему.
LaTeX
$$$\\text{If } φ(\\text{numeratorHom}(r)) = f(r)\\ \\forall r, \\ \\text{then } φ = \\text{universalMulHom}(f,fS,hf).$$$
Lean4
/-- The universal morphism `universalMulHom` is unique. -/
@[to_additive /-- The universal morphism `universalAddHom` is unique. -/
]
theorem universalMulHom_unique (φ : R[S⁻¹] →* T) (huniv : ∀ r : R, φ (numeratorHom r) = f r) :
φ = universalMulHom f fS hf := by
ext x;
cases x with
| _ r s
rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ← Units.val_one, ←
inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul, numeratorHom_apply,
OreLocalization.mul_cancel]
