unitForward_naturality₂ — Mathlib

English

In naturality two, for f: X ⟶ Y and p ∈ YonedaCollection (restrictedYonedaObj η) Y, we have: unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) = F.map f.op (unitForward η Y p).

Русский

В натуральности 2 для f: X ⟶ Y и p ∈ YonedaCollection (restrictedYonedaObj η) Y верно: unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) = F.map f.op (unitForward η Y p).

LaTeX

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

Lean4

@[simp]
theorem unitForward_naturality₂ {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X Y : C) (f : X ⟶ Y)
    (p : YonedaCollection (restrictedYonedaObj η) Y) :
    unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) = F.map f.op (unitForward η Y p) := by
  simp [unitForward]

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