of_yoneda_arrow — Mathlib

English

If hf: yoneda.map f ≫ η = s, then MakesOverArrow η s f; i.e., the underlying arrow f itself determines an over-arrow.

Русский

Если hf: yoneda.map f ≫ η = s, то MakesOverArrow η s f; то есть само ребро f определяет надстрелку.

LaTeX

$$$\\forall {Y : C} \\; {\\eta : yoneda.obj Y \\to A} \\; {X} \\; {s : yoneda.obj X \\to A} \\; {f : X ⟶ Y} \\; (hf : yoneda.map f ≫ η = s) : MakesOverArrow η s f$$$

Lean4

theorem of_yoneda_arrow {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} {f : X ⟶ Y}
    (hf : yoneda.map f ≫ η = s) : MakesOverArrow η s f := by simpa only [yonedaEquiv_yoneda_map f] using of_arrow hf

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