ι_comp_sigmaObjIso_inv — Mathlib

English

The inverse component satisfies (Sigma.ι (fun s => (f s).obj d) s) ≫ (sigmaObjIso f d).inv = (Sigma.ι f s).app d.

Русский

Обратный компонент удовлетворяет: (Sigma.ι (fun s => (f s).obj d) s) ≫ (sigmaObjIso f d).inv = (Sigma.ι f s).app d.

LaTeX

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

Lean4

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

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