ι_comp_sigmaObjIso_hom — Mathlib

English

For a discrete index α and f: α → D ⥤ C, (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s => (f s).obj d) s.

Русский

Для дискретного индекса α и f: α → D ⥤ C, выполняется равенство (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s => (f s).obj d) s.

LaTeX

$$$(\\Sigma.ι f s).\\mathrm{app} d \\;\\circ\\; (\\sigmaObjIso f d).\\mathrm{hom} = \\Sigma.\\mathrm{ι} (\\lambda s, (f s).\\mathrm{obj}\\; d)\\, s.$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_sigmaObjIso_hom (f : α → D ⥤ C) (d : D) (s : α) :
    (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s => (f s).obj d) s := by simp [sigmaObjIso]

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