ofHom_hom — Mathlib

English

A morphism in ModuleCat is determined by its underlying linear map; applying ofHom to Hom.hom recovers the morphism.

Русский

Морфизм в ModuleCat определяется своим подлежащим линейному отображению; применение ofHom к Hom.hom восстанавливает морфизм.

LaTeX

$$$ \\mathrm{Hom.hom}(f) \\text{ identifies with } f: \\; M \\to N. $$$

Lean4

@[simp]
theorem ofHom_hom {M N : ModuleCat.{v} R} (f : M ⟶ N) : ofHom (Hom.hom f) = f :=
  rfl

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