ofSelfIso — Mathlib

English

There exists a natural isomorphism between ModuleCat.of R M and M given by the identity on objects and morphisms.

Русский

Существует естественная изоморфия между ModuleCat.of R M и M, задаваемая единичными отображениями на объекте и морфизме.

LaTeX

$$$ \mathrm{ModuleCat}.of\; R\; M \cong M $$$

Lean4

/-- Forgetting to the underlying type and then building the bundled object returns the original
module. -/
@[deprecated Iso.refl (since := "2025-05-15")]
def ofSelfIso (M : ModuleCat R) : ModuleCat.of R M ≅ M
    where
  hom := 𝟙 M
  inv := 𝟙 M

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