of_arrow — Mathlib

English

If hf: f ≫ η = s, then there is an OverArrow η s (yonedaEquiv f). In words, any arrow f from X to Y induces an OverArrow with second component given by yonedaEquiv applied to f.

Русский

Пусть hf: f ⟶ η = s. Тогда существует OverArrow η s (yonedaEquiv f).

LaTeX

$$$\\forall {F : C^{\\mathrm{op}} \\to \\mathrm{Type}_v} \\; {\\eta : F ⟶ A} \\; {X} \\; {s : yoneda.obj X \\to A} \\; {f : yoneda.obj X \\to F},\\; (hf : f ≫ η = s) \\; \\Rightarrow \\ MakesOverArrow \\ η \\ s \\ (yonedaEquiv f) $$$

Lean4

theorem of_arrow {F : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} {f : yoneda.obj X ⟶ F} (hf : f ≫ η = s) :
    MakesOverArrow η s (yonedaEquiv f) :=
  ⟨hf ▸ rfl⟩

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