tensorUnit_whiskerLeft_comp_leftUnitor_hom

English

Relates the left unitor after whiskering with the tensor unit to the μ-composed expression involving ε and the left unitor map.

Русский

Связь между левым унитором после отдушки по тензорной единице и композиция μ с ε и левым унитором.

LaTeX

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

Lean4

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

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