homEquiv_symm_π_app — Mathlib

English

For a limit t and morphism f: W ⟶ t.pt, the symmetry of the hom-equivalence satisfies h.homEquiv.symm f ≫ t.π.app j = f.app j for all j.

Русский

Для предела t и морфизма f: W ⟶ t.pt, тож симметрия гом-эквивалентности удовлетворяет h.homEquiv.symm f ≫ t.π.app j = f.app j для всех j.

LaTeX

$$$ h.homEquiv.symm f \\circ t.\\pi_{j} = f_{j} $$$

Lean4

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

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