curriedActionMopMonoidal — Mathlib

Lean4
/-- When `C` acts on the left on `D`, the functor
`curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ` is monoidal, where `D ⥤ D` has the
composition monoidal structure. -/
@[simps!]
instance curriedActionMopMonoidal : (curriedActionMop C D).Monoidal
    where
  ε := .mop <| (actionUnitNatIso C D).inv
  μ _ _ := .mop <| { app _ := αₗ _ _ _ |>.inv }
  δ _ _ := .mop <| { app _ := αₗ _ _ _ |>.hom }
  η := .mop <| (actionUnitNatIso C D).hom
  associativity c₁ c₂
    c₃ := by
    apply (mopEquiv (D ⥤ D)).fullyFaithfulInverse.map_injective
    ext d
    simpa [-associator_actionHom] using
      (IsIso.inv_eq_inv.mpr <| associator_actionHom c₁ c₂ c₃ d).symm =≫ (α_ c₁ c₂ c₃).hom ⊵ₗ d
  oplax_right_unitality
    x := by
    apply MonoidalOpposite.hom_ext
    ext t
    simpa [-rightUnitor_actionHom] using (ρ_ x).inv ⊵ₗ t ≫= rightUnitor_actionHom x t
  oplax_left_unitality
    x := by
    apply MonoidalOpposite.hom_ext
    ext t
    simpa [-leftUnitor_actionHom] using (λ_ x).inv ⊵ₗ t ≫= leftUnitor_actionHom x t
Похожие утверждения