English
There is a natural equivalence between morphisms A ⟶ F.functorHom G and the internal Hom object HomObj F G A in the enriched setting.
Русский
Существует естественная эквиваленция между морфизмами A ⟶ F.functorHom G и внутренним гом-объектом HomObj F G A в обогащенной ситуации.
LaTeX
$$$\text{Equiv}\; (A \to F.functorHom G) \simeq HomObj F G A$$$
Lean4
/-- Morphisms `(𝟙_ (C ⥤ Type max v' v u) ⟶ F.functorHom G)` are in bijection with
morphisms `F ⟶ G`. -/
@[simps]
def natTransEquiv : (𝟙_ (C ⥤ Type max v' v u) ⟶ F.functorHom G) ≃ (F ⟶ G)
where
toFun
f :=
⟨fun X ↦ (f.app X (PUnit.unit)).app X (𝟙 _), by
intro X Y φ
rw [← (f.app X (PUnit.unit)).naturality φ]
congr 1
have := HomObj.congr_app (congr_fun (f.naturality φ) PUnit.unit) Y (𝟙 Y)
dsimp [functorHom, homObjFunctor] at this
aesop⟩
invFun f := { app _ _ := HomObj.ofNatTrans f }
left_inv
f := by
ext X a Y φ
have := HomObj.congr_app (congr_fun (f.naturality φ) PUnit.unit) Y (𝟙 Y)
dsimp [functorHom, homObjFunctor] at this
aesop
