whiskerRight_tensorUnit_comp_rightUnitor_hom

English

Analogous relation for whiskering on the right with tensor unit and the right unitor.

Русский

Аналогичное отношение для отдушки справа по отношению к тензорной единице и правому унитору.

LaTeX

$$$f \\triangleright 𝟙_D \\circ (ρ_{F X})^{hom} = (f \\otimes ε F) \\circ μ_{X, I}^{F} \\circ F.map (ρ_X)^{hom}$$$

Lean4

@[reassoc]
theorem whiskerRight_tensorUnit_comp_rightUnitor_hom {X : C} {Y : D} (f : Y ⟶ F.obj X) :
    f ▷ 𝟙_ D ≫ (ρ_ (F.obj X)).hom = (f ⊗ₘ ε F) ≫ μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom := by simp [tensorHom_def]

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