actLeft — Mathlib

Lean4
/-- Left action for the tensor product of two bimodules. -/
noncomputable def actLeft : R.X ⊗ X P Q ⟶ X P Q :=
  (PreservesCoequalizer.iso (tensorLeft R.X) _ _).inv ≫
    colimMap
      (parallelPairHom _ _ _ _ ((α_ _ _ _).inv ≫ ((α_ _ _ _).inv ▷ _) ≫ (P.actLeft ▷ S.X ▷ Q.X))
        ((α_ _ _ _).inv ≫ (P.actLeft ▷ Q.X))
        (by
          dsimp
          simp only [Category.assoc]
          slice_lhs 1 2 => rw [associator_inv_naturality_middle]
          slice_rhs 3 4 => rw [← comp_whiskerRight, middle_assoc, comp_whiskerRight]
          simp)
        (by
          dsimp
          slice_lhs 1 1 => rw [whiskerLeft_comp]
          slice_lhs 2 3 => rw [associator_inv_naturality_right]
          slice_lhs 3 4 => rw [whisker_exchange]
          simp))
Похожие утверждения