coneOfHasLimitEval — Mathlib

Lean4

/-- A cone for a functor `F : J ⥤ HomologicalComplex C c` which is given in degree `n` by
the limit `F ⋙ eval C c n`. -/
@[simps]
noncomputable def coneOfHasLimitEval : Cone F
    where
  pt :=
    { X := fun n => limit (F ⋙ eval C c n)
      d := fun n m => limMap { app := fun j => (F.obj j).d n m }
      shape := fun {n m} h => by
        ext j
        rw [limMap_π]
        dsimp
        rw [(F.obj j).shape _ _ h, comp_zero, zero_comp] }
  π :=
    { app := fun j => { f := fun _ => limit.π _ j }
      naturality := fun i j φ => by
        ext n
        dsimp
        erw [limit.w]
        rw [id_comp] }

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