English
The δ constraint for the induced oplax monoidal action map equals the δ-constraint of the underlying functor.
Русский
δ-ограничение индуцированной карты действия совпадает с δ исходной функтории.
LaTeX
$$$\delta (F.mapAction G) X Y)^{\mathrm{hom}} = \delta F X.V Y.V$$$
Lean4
/-- An oplax monoidal functor induces an oplax monoidal functor between
the categories of `G`-actions within those categories. -/
instance [F.OplaxMonoidal] : (F.mapAction G).OplaxMonoidal
where
η :=
{ hom := η F
comm := fun g => by
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
rw [map_id, Category.id_comp, Category.comp_id] }
δ X
Y :=
{ hom := δ F X.V Y.V
comm := fun g => (δ_natural F (X.ρ g) (Y.ρ g)).symm }
δ_natural_left _ _ := by ext; simp
δ_natural_right _ _ := by ext; simp
oplax_associativity _ _ _ := by ext; simp
oplax_left_unitality _ := by ext; simp
oplax_right_unitality _ := by ext; simp
