piObjIso_inv_comp_π — Mathlib

English

The inverse of piObjIso composed with Pi.π equals the projection from the product: (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s => (f s).obj d) s.

Русский

Обратный к piObjIso после композиции с Pi.π даёт плоскую проекцию: (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s => (f s).obj d) s.

LaTeX

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

Lean4

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

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