iso — Mathlib

English

There is a canonical isomorphism between LocalizedModule(S,M) and M' given by the universal property.

Русский

Существует канонический изоморфизм между LocalizedModule(S,M) и M' благодаря универсальному свойству.

LaTeX

$$$$ \mathrm{iso}_S f : \mathrm{LocalizedModule}(S,M) \cong_\!R M'. $$$$

Lean4

/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, then `M'` is isomorphic to
`LocalizedModule S M` as an `R`-module.
-/
noncomputable def iso : LocalizedModule S M ≃ₗ[R] M' :=
  { fromLocalizedModule S f, Equiv.ofBijective (fromLocalizedModule S f) <| fromLocalizedModule.bij _ _ with }

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