forgetToPresheafModuleCatObjMap_apply

English

The forgetful mapping at level X sends a morphism f to the underlying map M.map f; at the level of Hom, the forgetful map coincides with applying M.map f.

Русский

Забывающее отображение на уровне X отправляет морфизм f к соответствующей карте M.map f; множественные отображения согласованы.

LaTeX

$$$ (forgetToPresheafModuleCatObjMap X hX M f).hom = M.map f $$$

Lean4

@[simp]
theorem forgetToPresheafModuleCatObjMap_apply {Y Z : Cᵒᵖ} (f : Y ⟶ Z) (m : M.obj Y) :
    (forgetToPresheafModuleCatObjMap X hX M f).hom m = M.map f m :=
  rfl

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