English
In a dual setting, sections of F.op composed with yoneda.obj X are naturally in bijection with morphisms F → (const J).obj (op X).
Русский
В двойственной постановке секции F^{op} ∘ yoneda.obj X эквивалентны биекция между морфизмами F → (const J).obj (op X).
LaTeX
$$$\\text{equiv}:(F^{op} \\circ \\mathrm{yoneda.obj} X)\\text{.sections} \\simeq (F \\to (\\mathrm{const}\\ J).(op\\, X))$$$
Lean4
/-- Sections of `F ⋙ yoneda.obj X` identify to natural
transformations `(const J).obj X ⟶ F`. -/
@[simps]
def compYonedaSectionsEquiv (F : J ⥤ Cᵒᵖ) (X : C) : (F ⋙ yoneda.obj X).sections ≃ ((const J).obj (op X) ⟶ F)
where
toFun
s :=
{ app := fun j => (s.val j).op
naturality := fun j j' f => by
dsimp
rw [Category.id_comp]
exact Quiver.Hom.unop_inj (s.property f).symm }
invFun τ := ⟨fun j => (τ.app j).unop, fun {j j'} f => Quiver.Hom.op_inj (by simpa using (τ.naturality f).symm)⟩
