English
There is an equivalence between the enriched Hom functor and the presheaf Hom afterCoyoneda construction (Coyoneda object) for a monoidal category A; this is the core equivalence functorEnrichedHomCoyonedaObjEquiv.
Русский
Существует эквивалентность между обобщённым обобщением гомоморфизмов обогащённой функции и предшествующим гомоморфизмом прешерф-черезCoyoneda-объект для моноидальной категории A.
LaTeX
$$Equiv(((functorEnrichedHom A F G).comp (coyoneda.obj (op M))).obj (op X)) ≃ ((presheafHom (F ⊗ (Functor.const _).obj M) G).obj (op X))$$
Lean4
/-- Relation between `functorEnrichedHom` and `presheafHom`. -/
noncomputable def functorEnrichedHomCoyonedaObjEquiv (M : A) (F G : Cᵒᵖ ⥤ A) [HasFunctorEnrichedHom A F G] (X : C) :
(functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X) ≃
(presheafHom (F ⊗ (Functor.const _).obj M) G).obj (op X)
where
toFun
f :=
{ app j := MonoidalClosed.uncurry (f ≫ enrichedHomπ A _ _ (Under.mk j.unop.hom.op))
naturality j j'
φ := by
dsimp
rw [tensorHom_id, ← uncurry_natural_right, ← uncurry_pre_app, Category.assoc, Category.assoc, ←
enrichedOrdinaryCategorySelf_eHomWhiskerRight, ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
congr 2
exact
(enrichedHom_condition A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (i := Under.mk j.unop.hom.op)
(j := Under.mk j'.unop.hom.op) (Under.homMk φ.unop.left.op (Quiver.Hom.unop_inj (by simp)))).symm }
invFun
g :=
end_.lift (fun j ↦ MonoidalClosed.curry (g.app (op (Over.mk j.hom.unop))))
(fun j j' φ ↦ by
dsimp
rw [enrichedOrdinaryCategorySelf_eHomWhiskerRight, enrichedOrdinaryCategorySelf_eHomWhiskerLeft, curry_pre_app,
← curry_natural_right]
congr 1
let α : Over.mk j'.hom.unop ⟶ Over.mk j.hom.unop := Over.homMk φ.right.unop (Quiver.Hom.op_inj (by simp))
simpa using (g.naturality α.op).symm)
left_inv
f := by
dsimp
ext j
dsimp
simp only [curry_uncurry, end_.lift_π]
rfl
right_inv
g := by
dsimp
ext j
dsimp
simp only [uncurry_curry, end_.lift_π]
rfl
