unitHomEquiv_apply_coe — Mathlib

English

The evaluation of a unit morphism at an object X is given by applying the component of f to 1.

Русский

Оценка единичного морфа на объекте X задаётся применением компоненты отображения к 1.

LaTeX

$$$(M.\mathrm{unitHomEquiv} f).\mathrm{val} X = f.\mathrm{val}.app X (1) $$$

Lean4

@[simp]
theorem unitHomEquiv_apply_coe (M : SheafOfModules R) (f : unit R ⟶ M) (X : Cᵒᵖ) :
    (M.unitHomEquiv f).val X = f.val.app X (1 : R.val.obj X) :=
  rfl

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