compCoyonedaSectionsEquiv — Mathlib

English

A related formulation expressing the same evaluation of sections via the equivalence.

Русский

Альтернативная формулировка той же оценки секций через эквивалентность.

LaTeX

$$$\\text{(same as above)}$$$

Lean4

/-- Sections of `F ⋙ coyoneda.obj (op X)` identify to natural
transformations `(const J).obj X ⟶ F`. -/
@[simps]
def compCoyonedaSectionsEquiv (F : J ⥤ C) (X : C) : (F ⋙ coyoneda.obj (op X)).sections ≃ ((const J).obj X ⟶ F)
    where
  toFun
    s :=
    { app := fun j => s.val j
      naturality := fun j j' f => by
        dsimp
        rw [Category.id_comp]
        exact (s.property f).symm }
  invFun τ := ⟨τ.app, fun {j j'} f => by simpa using (τ.naturality f).symm⟩

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