app_unitForward — Mathlib

English

A variant form of Naturality 2 expressing the same compatibility between forward map and morphisms.

Русский

Вариант формы Натуральности 2, выражающий ту же совместимость прямого отображения и морфизмов.

LaTeX

$$$$ unitForward\eta\ X (YonedaCollection.map_2\ (restrictedYonedaObj\eta) f\ p) = F.map f^{op} (unitForward\eta\ Y\ p) $$$$

Lean4

@[simp]
theorem app_unitForward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : Cᵒᵖ) (p : YonedaCollection (restrictedYonedaObj η) X.unop) :
    η.app X (unitForward η X.unop p) = p.yonedaEquivFst := by simpa [unitForward] using p.snd.app_val

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