id_hComp_id — Mathlib

English

For CatEnriched C and morphisms f, f' : a ⟶ b with η : f ⟶ f', the horizontal composition with the identity on b is base-compatible, i.e., HEq (hComp (𝟙 (𝟙 a)) η) η.

Русский

Для CatEnriched C и морфизмов f, f' : a ⟶ b с η : f ⟶ f', горизонтальное произведение с идентичностью на b совместимо по базовой схеме: HEq (hComp (𝟙 (𝟙 a)) η) η.

LaTeX

$$$ \\mathrm{HEq}\\left( \\mathrm{hComp}(\\mathbf{1}_{\\mathbf{1}a}, \\eta) , \\eta \\right)$$$

Lean4

@[simp]
theorem id_hComp_id {a b c : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) : hComp (𝟙 f) (𝟙 g) = 𝟙 (f ≫ g) :=
  Functor.map_id ..

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