universalMulHom_commutes — Mathlib

English

The universal lift is unique: if φ: R[S⁻¹] →* T satisfies φ(numeratorHom(r)) = f(r) for all r, then φ = universalMulHom f fS hf.

Русский

Универсальный подъем единственен: если φ: R[S⁻¹] →* T удовлетворяет φ(numeratorHom(r)) = f(r) для всех r, то φ = universalMulHom f fS hf.

LaTeX

$$$\\forall r,\\; φ(\\text{numeratorHom}(r)) = f(r) \\Rightarrow φ = \\text{universalMulHom}(f,fS,hf).$$$

Lean4

@[to_additive]
theorem universalMulHom_commutes {r : R} : universalMulHom f fS hf (numeratorHom r) = f r := by
  simp [numeratorHom_apply, universalMulHom_apply]

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