English
There exists a canonical isomorphism between two corepresentable functors that defines the left unitor for the Day convolution construction.
Русский
Существует каноническое изоморфизм между двумя представляемыми по действию функторaми, задающий левый унитор для Day конволюции.
LaTeX
$$$ (\text{LeftUnitorCorepresentingIso}) :\; (\text{whiskeringLeft} \; (\text{prod} \; C \; C) \; C \; V).\text{obj}(\text{tensor} C) \;\cong\; \text{Coyoneda}.(\cdot) \; \text{op} \; F $$$
Lean4
/-- The isomorphism of corepresentable functors that defines the left unitor for
Day convolution. -/
@[simps!]
def leftUnitorCorepresentingIso :
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙
coyoneda.obj (.op <| Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) ≅
coyoneda.obj (.op <| F) :=
by
calc
_ ≅
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙
(whiskeringLeft _ _ _).obj (prod.leftUnitorEquivalence C).inverse ⋙
coyoneda.obj (.op <| (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
isoWhiskerLeft _
(isoWhiskerLeft _
(NatIso.ofComponents fun _ ↦
Equiv.toIso <| (prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv))
_ ≅
(whiskeringLeft _ _ _).obj
((prod.leftUnitorEquivalence C).inverse ⋙ (Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C) ⋙ tensor C) ⋙
coyoneda.obj (.op <| (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
(.refl _)
_ ≅
(whiskeringLeft _ _ _).obj (𝟭 _) ⋙
coyoneda.obj (.op <| (prod.leftUnitorEquivalence C).inverse ⋙ Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) :=
(isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents fun _ ↦ λ_ _) _)
_ ≅ _ := coyoneda.mapIso <| Iso.op <| NatIso.ofComponents fun _ ↦ (λ_ _).symm
