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