hComp_id — Mathlib

English

For CatEnriched C and η : f ⟶ f', the horizontal composition with the identity on b is equal to the base morphisms: hComp η (𝟙 (𝟙 b)) = eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f').symm.

Русский

Для CatEnriched C и η : f ⟶ f' горизонтальное произведение с единицей на b равно базовой морфизме: hComp η (𝟙 (𝟙 b)) = eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f').symm.

LaTeX

$$$ hComp(\\eta, \\mathbf{1}_{\\mathbf{1} b}) = eqToHom(\\mathrm{comp\_id}\,f) \\;≫\\; \\eta \\;≫\\; eqToHom(\\mathrm{comp\_id}\,f')^{-1} $$$

Lean4

theorem hComp_id {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') :
    hComp η (𝟙 (𝟙 b)) = eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f').symm := by simp [← heq_eq_eq, hComp_id_heq]

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