actionOfMonoidalFunctorToEndofunctor

Lean4

/-- A monoidal functor `F : C ⥤ D ⥤ D` can be thought of as a right action
of `C` on `D`. -/
@[simps!]
def actionOfMonoidalFunctorToEndofunctor (F : C ⥤ D ⥤ D) [F.Monoidal] : MonoidalRightAction C D
    where
  actionObj d c := (F.obj c).obj d
  actionHomLeft f c := (F.obj c).map f
  actionHomRight d _ _ f := (F.map f).app d
  actionAssocIso d c c' := Functor.Monoidal.μIso F c c' |>.app d |>.symm
  actionUnitIso d := Functor.Monoidal.εIso F |>.app d |>.symm
  actionAssocIso_hom_naturality {c₁ c₁' c₂ c₂' c₃ c₃'} f g
    h := by
    have e := congrArg (fun t ↦ t.app c₁) <| Functor.OplaxMonoidal.δ_natural F g h
    dsimp at e
    simp [reassoc_of% e]

Похожие утверждения