dayConvolutionInternalHomDiagramFunctor

Lean4
/-- Given `F : C ⥤ V`, this is the functor
`G ↦ c c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c))`.
The internal hom functor for Day convolution `[F, -]` is naturally isomorphic
to the functor `G ↦ c ↦ end_ (c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c)))`, hence
this definition. -/
@[simps!]
def dayConvolutionInternalHomDiagramFunctor (F : C ⥤ V) : (C ⥤ V) ⥤ C ⥤ Cᵒᵖ ⥤ C ⥤ V
    where
  obj
    G :=
    { obj c := Functor.whiskeringLeft₂ _ |>.obj F.op |>.obj (tensorRight c ⋙ G) |>.obj MonoidalClosed.internalHom
      map {c c'}
        f :=
        Functor.whiskeringLeft₂ _ |>.obj F.op |>.map (Functor.whiskerRight (curriedTensor C |>.flip.map f) G) |>.app
          MonoidalClosed.internalHom }
  map {G G'}
    η :=
    { app c := Functor.whiskeringLeft₂ _ |>.obj F.op |>.map (Functor.whiskerLeft _ η) |>.app MonoidalClosed.internalHom
      naturality {c c'}
        f := by
        ext j k
        dsimp
        simpa [-NatTrans.naturality] using congr_arg (ihom <| F.obj <| unop j).map (η.naturality <| k ◁ f) }
Похожие утверждения