English
When F and G are functors into Type and A is a functor, the HomObj Equiv provides a bijection with morphisms in the tensor product.
Русский
Когда F и G — функторы в Type, а A — функтор, эквивалентность HomObj обеспечивает биекцию с морфизмами в тензоре.
LaTeX
$$$HomObj\,F\,G\,A \cong F\otimes A \to G$$$
Lean4
/-- When `F`, `G`, and `A` are all functors `C ⥤ Type w`, then `HomObj F G A` is in
bijection with `F ⊗ A ⟶ G`. -/
@[simps]
def homObjEquiv (F G A : C ⥤ Type w) : (HomObj F G A) ≃ (F ⊗ A ⟶ G)
where
toFun
a :=
⟨fun X ⟨x, y⟩ ↦ a.app X y x, fun X Y f ↦ by
ext ⟨x, y⟩
erw [congr_fun (a.naturality f y) x]
rfl⟩
invFun
a :=
⟨fun X y x ↦ a.app X (x, y), fun φ y ↦ by
ext x
erw [congr_fun (a.naturality φ) (x, y)]
rfl⟩
left_inv _ := by aesop
right_inv _ := by aesop
