ε_tensorHom_comp_μ — Mathlib

English

Repeat of the left unitality inverse coherence for F.

Русский

Повторение соответствия левого единичного инверсного факта для F.

LaTeX

$$$(\\lambda_{F X})^{-1} \\;\\circ (ε F \\triangleright F X) \\circ μ_{I,X}^F = F.map (\\lambda_X)^{-1}$$$

Lean4

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

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