English
Equality expressing the interaction of whiskering on the left with the right unitor and the associator. It equates whiskering on the left by f with a composite involving the associator and the right unitor applied to f and g.
Русский
Взаимодействие левым висениям с правым уитором и ассоциатором: равенство между висением слева и композициями через ассоциатор и правый уитор.
LaTeX
$$$ (f ◁ (ρ_g)^{hom}) = (α_f g (𝟙 c))^{-1} ≫ (ρ_{f ≫ g})^{hom} $$$
Lean4
@[reassoc, simp]
theorem whiskerLeft_rightUnitor (f : a ⟶ b) (g : b ⟶ c) : f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom := by
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ← cancel_epi (f ◁ (α_ _ _ _).inv),
pentagon_inv_assoc, triangle_assoc_comp_right, ← associator_inv_naturality_middle, ← whiskerLeft_comp_assoc,
triangle_assoc_comp_right, associator_inv_naturality_right]
