isColimitCoconeOfLEOfCocone — Mathlib

English

There is a natural map from the arrow map data of the extended cocone to the arrow data of the original functor F, coherent with the maps in the directed system.

Русский

Существует естественное отображение из данных отображения стрелки расширённого кокона к данным стрелок оригинального функторa F, согласованное с отображениями в направленной системе.

LaTeX

$$$\\mathrm{arrowMap}(\\mathrm{ofCocone} \\ c) = \\mathrm{ArrowMk}(F.map) \\circ \\text{coherence}$$$

Lean4

/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/
def isColimitCoconeOfLEOfCocone (hc : IsColimit c) : IsColimit (coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
  (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1
    (IsColimit.ofIsoColimit hc
      (Cocones.ext (ofCoconeObjIsoPt c).symm
        (fun ⟨i, hi⟩ ↦ by
          dsimp
          rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc])))

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