English
The Day convolution associator is natural in each argument; maps commute with morphisms in the three variables F, G, H.
Русский
Ассоциатор Day-конволюции естествен по каждому аргументу; отображения коммутируют с морфизмами в трёх переменных F, G, H.
LaTeX
$$$\\text{map}(\\text{map } f g) h \\; \\text{commutes with } (\\text{associator})$$$
Lean4
/-- The isomorphism of functors between
`((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -)` and
`(F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -)` that coresponsds to the associator
isomorphism for Day convolution through `corepresentableBy₂` and `corepresentableBy₂`. -/
@[simps!]
def associatorCorepresentingIso :
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙ coyoneda.obj (.op <| (F ⊠ G) ⊠ H) ≅
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C)) ⋙ coyoneda.obj (.op <| F ⊠ G ⊠ H) :=
calc
_ ≅
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((tensor C).prod (𝟭 C)) ⋙
(whiskeringLeft _ _ _).obj (prod.associativity C C C).inverse ⋙
coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) :=
isoWhiskerLeft _
(isoWhiskerLeft _
(NatIso.ofComponents fun _ ↦
Equiv.toIso <| (prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv))
_ ≅
(whiskeringLeft _ _ _).obj ((prod.associativity C C C).inverse ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C) ⋙
coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) :=
(.refl _)
_ ≅
(whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ tensor C) ⋙
coyoneda.obj (.op <| (prod.associativity C C C).inverse ⋙ (F ⊠ G) ⊠ H) :=
(isoWhiskerRight ((whiskeringLeft _ _ _).mapIso <| NatIso.ofComponents (fun _ ↦ α_ _ _ _)) _)
_ ≅ (whiskeringLeft _ _ _).obj ((𝟭 C).prod (tensor C) ⋙ tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G ⊠ H) :=
isoWhiskerLeft _ <| coyoneda.mapIso <| Iso.op <| NatIso.ofComponents (fun _ ↦ α_ _ _ _ |>.symm)
