π_tensor_id_actRight — Mathlib

English

The action of the unit on the right is compatible with actRight, giving equality between coequalized forms and the left unitor.

Русский

Действие единицы справа совместимо с actRight, дают равенство между образами коглеи и правым единичным унитором.

LaTeX

$$$(\_ ◁ η) ≫ actRight P Q = (\rho_\_).hom$$$

Lean4

theorem π_tensor_id_actRight :
    (coequalizer.π _ _ ▷ T.X) ≫ actRight P Q = (α_ _ _ _).hom ≫ (P.X ◁ Q.actRight) ≫ coequalizer.π _ _ :=
  by
  erw [map_π_preserves_coequalizer_inv_colimMap (tensorRight _)]
  simp only [Category.assoc]

Похожие утверждения