ι_colimitIsoColimitGrothendieck_inv

English

Equality of injections for Grothendieck construction with colimit iso when comparing G and CostructuredArrow projections.

Русский

Равенство инъекций для конструирования Гротендик через колимит и проекции Costructured Arrow.

LaTeX

$$$ι_colimitIsoColimitGrothendieck_inv$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitIsoColimitGrothendieck_inv (X : Grothendieck (CostructuredArrow.functor L)) :
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (colimitIsoColimitGrothendieck L G).inv =
      colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber) :=
  by simp [colimitIsoColimitGrothendieck]

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