Lean4
/-- Define a left action of `Cᵒᵖ` on `Dᵒᵖ` from a left action of `C` on `D` via
the formula `(op c) ⊙ₗ (op d) = op (c ⊙ₗ d)`. -/
@[simps -isSimp]
def oppositeLeftAction [MonoidalLeftAction C D] : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
where
actionObj c d := op <| c.unop ⊙ₗ d.unop
actionHomLeft f d := (f.unop ⊵ₗ unop d).op
actionHomRight c _ _ f := (unop c ⊴ₗ f.unop).op
actionHom f g := (f.unop ⊙ₗₘ g.unop).op
actionAssocIso _ _ _ := Iso.op <| (αₗ _ _ _).symm
actionUnitIso _ := Iso.op <| (λₗ _).symm
actionHom_def
| op f, op g => by
apply Quiver.Hom.unop_inj
simpa [MonoidalLeftAction.action_exchange] using MonoidalLeftAction.actionHom_def f g
actionAssocIso_hom_naturality
| op f, op g, op h => by
apply Quiver.Hom.unop_inj
haveI := (αₗ (unop _) (unop _) (unop _)).inv ≫= MonoidalLeftAction.actionAssocIso_hom_naturality f g h
simp only [Iso.inv_hom_id_assoc] at this
simp [← this]
actionUnitIso_hom_naturality
_ := by
apply Quiver.Hom.unop_inj
simp
whiskerRight_actionHomLeft _ _
_ := by
apply Quiver.Hom.unop_inj
simp
associator_actionHom _ _ _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
leftUnitor_actionHom _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
rightUnitor_actionHom _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
