ofHom_hom — Mathlib

English

For topological modules X,Y and a morphism f : X ⟶ Y, the ofHom construction recovers the original morphism from its underlying map: ofHom f.hom = f.

Русский

Для X,Y и морфизма f : X ⟶ Y конструктор ofHom восстанавливает исходный морфизм по его основанной карте: ofHom f.hom = f.

LaTeX

$$$ \operatorname{ofHom}(f.\\hom) = f $$$

Lean4

@[simp]
theorem ofHom_hom {X Y : TopModuleCat R} (f : X.Hom Y) : ofHom f.hom = f :=
  rfl

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