Lean4
/-- A monoidal functor `F : C ⥤ (D ⥤ D)ᴹᵒᵖ` can be thought of as a left action
of `C` on `D`. -/
@[simps!]
def actionOfMonoidalFunctorToEndofunctorMop (F : C ⥤ (D ⥤ D)ᴹᵒᵖ) [F.Monoidal] : MonoidalLeftAction C D
where
actionObj c d := (F.obj c).unmop.obj d
actionHomLeft f d := (F.map f).unmop.app d
actionHomRight c _ _ f := (F.obj c).unmop.map f
actionAssocIso c c' d := Functor.Monoidal.μIso F c c' |>.unmop.app d |>.symm
actionUnitIso d := Functor.Monoidal.εIso F |>.unmop.app d |>.symm
actionAssocIso_hom_naturality {c₁ c₁' c₂ c₂' c₃ c₃'} f g
h := by
have e := congrArg (fun t ↦ t.unmop.app c₃) <| Functor.OplaxMonoidal.δ_natural F f g
dsimp at e
simp [reassoc_of% e]
whiskerRight_actionHomLeft {x y} c f
d := by
have e := congrArg (fun t ↦ t.unmop.app d) <| Functor.LaxMonoidal.μ_natural_left F f c
dsimp at e
simp [e, ← NatTrans.comp_app, ← unmop_comp]
whiskerLeft_actionHomLeft c {x y} f
d := by
have e := congrArg (fun t ↦ t.unmop.app d) <| Functor.LaxMonoidal.μ_natural_right F c f
dsimp at e
simp [e, ← NatTrans.comp_app, ← unmop_comp]
associator_actionHom c₁ c₂ c₃
d := by
have e := congrArg (fun t ↦ t.unmop.app d) <| Functor.OplaxMonoidal.associativity F c₁ c₂ c₃
dsimp at e
simp only [Category.comp_id] at e
simp [e]
leftUnitor_actionHom c
d :=
by
have e :=
(F.map (λ_ c).hom).unmop.app d ≫= (congrArg (fun t ↦ t.unmop.app d) <| Functor.OplaxMonoidal.left_unitality F c)
dsimp at e
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp, ← F.map_comp_assoc, Iso.hom_inv_id,
Functor.map_id, Category.id_comp] at e
simp [e]
rightUnitor_actionHom c
d :=
by
have e :=
(F.map (ρ_ c).hom).unmop.app d ≫= (congrArg (fun t ↦ t.unmop.app d) <| Functor.OplaxMonoidal.right_unitality F c)
dsimp at e
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp, ← F.map_comp_assoc, Iso.hom_inv_id,
Functor.map_id, Category.id_comp] at e
simp [e]
