id_comp — Mathlib

English

The monoidal composition with identity on the right yields the identity morphism.

Русский

Композиция с тождественным слева/справа даёт тождественный морфизм.

LaTeX

$$$$ (\rho_{\mathrm{Hom}(i j)})^{-1} \circ (\mathrm{Hom}(i j) \triangleleft \mathrm{id}_j) \circ \mathrm{comp}_{i j j} = \mathrm{Id}_{\mathrm{Hom}(i j)} $$$$

Lean4

@[simp]
theorem id_comp (i j : SimplicialThickening J) : (λ_ (Hom i j)).inv ≫ id i ▷ Hom i j ≫ comp i i j = 𝟙 (Hom i j) := by
  aesop

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