curriedActionMonoidal — Mathlib

Lean4
/-- When `C` acts on the right on `D`, the functor `curriedAction : C ⥤ (D ⥤ D)`
is monoidal, where `D ⥤ D` has the composition monoidal structure. -/
@[simps!]
instance curriedActionMonoidal [MonoidalRightAction C D] : (curriedAction C D).Monoidal
    where
  ε := (actionUnitNatIso C D).inv
  μ _ _ := { app _ := αᵣ _ _ _ |>.inv }
  δ _ _ := { app _ := αᵣ _ _ _ |>.hom }
  η := (actionUnitNatIso C D).hom
  associativity c₁ c₂
    c₃ := by
    ext d
    simpa [-actionHom_associator] using
      (IsIso.inv_eq_inv.mpr <| actionHom_associator c₁ c₂ c₃ d).symm =≫ d ⊴ᵣ (α_ c₁ c₂ c₃).hom
  oplax_right_unitality
    x := by
    ext t
    simpa [-actionHom_rightUnitor] using t ⊴ᵣ (ρ_ x).inv ≫= actionHom_rightUnitor x t
  oplax_left_unitality
    x := by
    ext t
    simpa [-actionHom_leftUnitor] using t ⊴ᵣ (λ_ x).inv ≫= actionHom_leftUnitor x t
Похожие утверждения