sectionsEquivHom_naturality_symm — Mathlib

English

There is a natural isomorphism between the sections functor and a coyoneda object, specifically sectionsFunctor C ≅ coyoneda.obj (op ((Functor.const C).obj X)) for a given X with Unique X, i.e., a canonical isomorphism of functors.

Русский

Существует естественное изоморфное соотношение между sectionsFunctor C и coyoneda.obj (op ((Functor.const C).obj X)) при заданном X с Unique X.

LaTeX

$$$$ \mathrm{sectionsFunctor}(C) \cong \mathrm{coyoneda.obj}(\mathrm{op}((\mathrm{Functor.const} C).obj X)) $$$$

Lean4

theorem sectionsEquivHom_naturality_symm {F G : C ⥤ Type u₂} (f : F ⟶ G) (X : Type u₂) [Unique X]
    (τ : (const C).obj X ⟶ F) :
    (G.sectionsEquivHom X).symm (τ ≫ f) = (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ) := by rfl

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