e_id_comp — Mathlib

English

Identity and composition in enriched category satisfy a unit law.

Русский

Единичный элемент и композиция в обогащенной категории удовлетворяют правилу единицы.

LaTeX

$$$\rho_{(X\to Y)}^{-1} \circ _ \circ eId V Y \circ eComp V X Y Y = \mathrm{id}$$$

Lean4

@[reassoc (attr := simp)]
theorem e_id_comp (X Y : C) : (λ_ (X ⟶[V] Y)).inv ≫ eId V X ▷ _ ≫ eComp V X X Y = 𝟙 (X ⟶[V] Y) :=
  EnrichedCategory.id_comp X Y

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