liftToFinsetColimIso_aux — Mathlib

English

A technical identity showing compatibility between Sigma.map, colimit injections, and the colimit iso in the Finset lifting construction.

Русский

Техническое тождество, показывающее совместимость между Sigma.map, инъекциями колимита и изоморфизмом колимита в конструкции подъёма на Finset.

LaTeX

$$$$ (\\Sigma.ι (F.obj ·.val)\\, j) \\, ;\\; \\mathrm{colimit.ι}(\\mathrm{liftToFinsetObj}F) \\; ;\\; (\\mathrm{colimit.isoColimitCocone}(\\mathrm{liftToFinsetColimitCocone}F))^{-1} = \\mathrm{colimit.ι}Fj. $$$$

Lean4

/-- Helper construction for `liftToFinsetColimIso`. -/
@[reassoc]
theorem liftToFinsetColimIso_aux (F : Discrete α ⥤ C) {J : Finset (Discrete α)} (j : J) :
    Sigma.ι (F.obj ·.val) j ≫
        colimit.ι (liftToFinsetObj F) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv =
      colimit.ι F j :=
  by simp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

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