hComp_id — Mathlib

English

A more detailed left-unit law for hComp in CatEnrichedOrdinary: hComp η (𝟙 (𝟙 b)) equals eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f')^{-1}.

Русский

Уравнение левого единичного закона для hComp в CatEnrichedOrdinary: hComp η (𝟙 (𝟙 b)) = eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f').symm.

LaTeX

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

Lean4

theorem hComp_id {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') :
    hComp η (𝟙 (𝟙 b)) = eqToHom (comp_id f) ≫ η ≫ eqToHom (comp_id f').symm :=
  by
  ext
  simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
  rw [homEquiv_id]
  simp [CatEnriched.hComp_id_heq]

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