actRight_one' — Mathlib

English

Equality expressing the unit interaction on the right with actRight, via the left unitor.

Русский

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

LaTeX

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

Lean4

theorem actRight_one' : (_ ◁ η) ≫ actRight P Q = (ρ_ _).hom :=
  by
  refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
  dsimp [X]
  slice_lhs 1 2 => rw [← whisker_exchange]
  slice_lhs 2 3 => rw [π_tensor_id_actRight]
  slice_lhs 1 2 => rw [associator_naturality_right]
  slice_lhs 2 3 => rw [← whiskerLeft_comp, actRight_one]
  simp

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