ι_app_homEquiv_symm — Mathlib

English

For a colimit t and a cocone f : F ⟶ (const J).obj W, the j-th leg of f factors through t.ι via the inverse of the equivalence: t.ι.app j ≫ h.homEquiv.symm f = f.app j.

Русский

Для колимитного кокона t и кокона f : F ⟶ (const J).obj W, j-й компонент f проходит через t.ι через обратное от эквивалентности: t.ι.app j ≫ h.homEquiv.symm f = f.app j.

LaTeX

$$$t.\iota_{app\, j} \;\gg\; h.homEquiv.symm\, f = f.app\, j$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_app_homEquiv_symm (h : IsColimit t) {W : C} (f : F ⟶ (const J).obj W) (j : J) :
    t.ι.app j ≫ h.homEquiv.symm f = f.app j := by simp [homEquiv]

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