uliftYonedaEquiv_naturality — Mathlib

English

For X,Y in C^op and F a functor, the naturality of uliftYonedaEquiv in f and g holds: uliftYonedaEquiv.map_naturality.

Русский

Для X,Y в C^op и F — функтор, сохраниется естественность uliftYonedaEquiv в аргументах f и g.

LaTeX

$$$uliftYonedaEquiv.map_naturality$$$

Lean4

theorem uliftYonedaEquiv_naturality {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type max w v₁} (f : uliftYoneda.{w}.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.map g (uliftYonedaEquiv.{w} f) = uliftYonedaEquiv.{w} (uliftYoneda.map g.unop ≫ f) := by
  simp [uliftYonedaEquiv, uliftYoneda, ← FunctorToTypes.naturality _ _ f g (ULift.up (𝟙 _))]

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