actRight — Mathlib

Lean4
/-- Right action for the tensor product of two bimodules. -/
noncomputable def actRight : X P Q ⊗ T.X ⟶ X P Q :=
  (PreservesCoequalizer.iso (tensorRight T.X) _ _).inv ≫
    colimMap
      (parallelPairHom _ _ _ _ ((α_ _ _ _).hom ≫ (α_ _ _ _).hom ≫ (P.X ◁ S.X ◁ Q.actRight) ≫ (α_ _ _ _).inv)
        ((α_ _ _ _).hom ≫ (P.X ◁ Q.actRight))
        (by
          dsimp
          slice_lhs 1 2 => rw [associator_naturality_left]
          slice_lhs 2 3 => rw [← whisker_exchange]
          simp)
        (by
          dsimp
          simp only [comp_whiskerRight, whisker_assoc, Category.assoc, Iso.inv_hom_id_assoc]
          slice_lhs 3 4 => rw [← whiskerLeft_comp, middle_assoc, whiskerLeft_comp]
          simp))
Похожие утверждения