English
Re-statement of the universal property: for every g and h there exists a unique l with l ∘ f = g.
Русский
Повторное изложение универсального свойства: для каждого g и h существует единственный l, такой что l ∘ f = g.
LaTeX
$$$$ \exists! l : M' \to M'', \; l \circ f = g. $$$$
Lean4
/-- Universal property from localized module:
If `(M', f : M ⟶ M')` is a localized module then it satisfies the following universal property:
For every `R`-module `M''` which every `s : S`-scalar multiplication is invertible and for every
`R`-linear map `g : M ⟶ M''`, there is a unique `R`-linear map `l : M' ⟶ M''` such that
`l ∘ f = g`.
```
M -----f----> M'
| /
|g /
| / l
v /
M''
```
-/
theorem is_universal :
∀ (g : M →ₗ[R] M'') (_ : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)),
∃! l : M' →ₗ[R] M'', l.comp f = g :=
fun g h => ⟨lift S f g h, lift_comp S f g h, fun l hl => (lift_unique S f g h l hl).symm⟩
