ι_colimitIsoColimitGrothendieck_hom

English

The colimit injections satisfy a standard isomorphism with the Grothendieck projection in the left Kan extension setup.

Русский

Инъекции колимита удовлетворяют каноническому изоморфизму с проекцией Гротендик в настройке левого канонического расширения.

LaTeX

$$$ι_colimitIsoColimitGrothendieck_hom$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitIsoColimitGrothendieck_hom (X : C) :
    colimit.ι G X ≫ (colimitIsoColimitGrothendieck L G).hom =
      colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) ⟨L.obj X, .mk (𝟙 _)⟩ :=
  by
  rw [← Iso.eq_comp_inv]
  exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

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