English
Sections of F.op followed by Yoneda with X correspond to natural transformations from F to the constant functor, in opposite setting.
Русский
Секции F^{op} затем yonedaobj X соответствуют естественным преобразованиям из F к константному функтору в противоположном виде.
LaTeX
$$$(F:\\, J \\to C)^{\\mathrm{op}} \\circ \\mathrm{yoneda.obj}\\; X \\quad\\text{sections} \\cong (F \\Rightarrow (\\mathrm{const}\\ J).(op\\, X))$$$
Lean4
/-- Sections of `F.op ⋙ yoneda.obj X` identify to natural
transformations `F ⟶ (const J).obj X`. -/
@[simps]
def opCompYonedaSectionsEquiv (F : J ⥤ C) (X : C) : (F.op ⋙ yoneda.obj X).sections ≃ (F ⟶ (const J).obj X)
where
toFun
s :=
{ app := fun j => s.val (op j)
naturality := fun j j' f => by
dsimp
rw [Category.comp_id]
exact (s.property f.op) }
invFun τ := ⟨fun j => τ.app j.unop, fun {j j'} f => by simp [τ.naturality f.unop]⟩
