functorHomEquiv — Mathlib

English

There is a natural equivalence between morphisms from A to F.functorHom G and the internal Hom object HomObj F G A, for A a functor into Type-valued objects.

Русский

Существует естественная эквивалентность между морфизмами A ⟶ F.functorHom G и внутренним гом-объектом HomObj F G A, где A — функтор в Type.

LaTeX

$$$\text{Equiv} \\ (A \\to F.functorHom G) \\cong \\ HomObj F G A$$$

Lean4

/-- The equivalence `(A ⟶ F.functorHom G) ≃ HomObj F G A`. -/
@[simps]
def functorHomEquiv (A : C ⥤ Type max u v v') : (A ⟶ F.functorHom G) ≃ HomObj F G A
    where
  toFun
    φ :=
    { app := fun X a ↦ (φ.app X a).app X (𝟙 _)
      naturality := fun {X Y} f a => by
        rw [← (φ.app X a).naturality f (𝟙 _)]
        have := HomObj.congr_app (congr_fun (φ.naturality f) a) Y (𝟙 _)
        dsimp [functorHom, homObjFunctor] at this
        aesop }
  invFun
    x :=
    { app := fun X a ↦ { app := fun Y f => x.app Y (A.map f a) }
      naturality := fun X Y f => by
        ext
        dsimp only [types_comp_apply]
        rw [← FunctorToTypes.map_comp_apply]
        rfl }
  left_inv
    φ := by
    ext X a Y f
    exact (HomObj.congr_app (congr_fun (φ.naturality f) a) Y (𝟙 _)).trans (congr_arg ((φ.app X a).app Y) (by simp))
  right_inv x := by simp

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