tensorHom_ε_comp_μ — Mathlib

English

A compatibility relation between the unit ε, a tensored morphism, and the multiplication μ.

Русский

Совместимость между единицей ε, тензоризованным морфизмом и умножением μ.

LaTeX

$$$(ε F \\otimes f) \\;\\circ μ_{\\mathbb{1},X}^F = 𝟙_D \\triangleleft f \\;\\circ (λ_{F X})^{-1} \\circ F.map (λ_X)^{-1}$$$

Lean4

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

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