universalHom_unique — Mathlib

English

If φ: R[S⁻¹] →+* T is any ring hom whose values on numerator(r) coincide with f(r) for all r ∈ R, then φ is equal to the universal hom, i.e., φ = universalHom f fS hf.

Русский

Пусть φ: R[S⁻¹] →+* T — гомоморфизм колец, для которого на образах numerator(r) выполняется φ(numerator(r)) = f(r) для всех r ∈ R; тогда φ совпадает с универсальным гомоморфизмом, то есть φ = universalHom f fS hf.

LaTeX

$$∀ r, φ(numeratorHom(r)) = f(r) ⇒ φ = OreLocalization.universalHom f fS hf$$

Lean4

theorem universalHom_unique (φ : R[S⁻¹] →+* T) (huniv : ∀ r : R, φ (numeratorHom r) = f r) : φ = universalHom f fS hf :=
  RingHom.coe_monoidHom_injective <| universalMulHom_unique (RingHom.toMonoidHom f) fS hf (↑φ) huniv

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