left_unitality_hom — Mathlib

English

Relates δ with the unit η and the unit tensor transformation on the left via a tensor product.

Русский

Связь δ с η и единичной трансформацией по тензорному блоку слева через тензорное произведение.

LaTeX

$$$δ F (I) X \\circ (η F \\otimes f) = F.map (λ_X)^{hom} \\circ (λ_{F X})^{-1} \\circ f$$$

Lean4

@[reassoc (attr := simp)]
theorem left_unitality_hom (X : C) : δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom := by
  rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc, ← F.map_comp, Iso.hom_inv_id, F.map_id,
    id_comp]

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