piObjIso_hom_comp_π — Mathlib

English

For a discrete index α, and a functor f: α → D ⥤ C, the component of piObjIso composed with Pi.π equals the app projection: (piObjIso f d).hom ≫ Pi.π f s).app d = Pi.π f s).app d.

Русский

Для дискретного индекса α и функтору f: α → D ⥤ C, компоненту piObjIso при композиции с Pi.π даёт нужный компонент: (piObjIso f d).hom ≫ Pi.π f s).app d = Pi.π f s).app d.

LaTeX

$$$\\big(\\piObjIso\, f\, d\\big).\\mathrm{hom} \\; \\circ \\; \\mathrm{Pi}.\\mathrm{π}\\big(f\, s\\big).\\mathrm{app} \\; d = \\mathrm{Pi}.\\mathrm{π}\\big(f\\, s\\big).\\mathrm{app} \\; d.$$$

Lean4

@[reassoc (attr := simp)]
theorem piObjIso_hom_comp_π (f : α → D ⥤ C) (d : D) (s : α) :
    (piObjIso f d).hom ≫ Pi.π (fun s => (f s).obj d) s = (Pi.π f s).app d := by simp [piObjIso]

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