runs_forever.lean

import category_theory.limits.cones algebra.homology.homological_complex

section

open category_theory category_theory.limits homological_complex

universes u u' v v' idx

def homological_complex.cone_of_degreewise_cones
  {J : Type u} [category.{u'} J] {V : Type v} [category.{v'} V] [has_zero_morphisms V]
  {ι : Type idx} {c : complex_shape ι} 
  (F : J ⥤ homological_complex V c)
  (choices : Π (i : ι), limit_cone (F ⋙ homological_complex.eval V c i))
  : cone F := {
    X := {
      X := λ i, (choices i).cone.X,
      d := λ i j, (choices j).is_limit.lift ({
        X := (choices i).cone.X,
        π := { app := λ u, (choices i).cone.π.app u ≫ (F.obj u).d i j,
                naturality' := λ u v f, by { transitivity,
                                            apply category.id_comp,
                                            rw [category.assoc, functor.comp_map, eval_map,
                                                ← (F.map f).comm i j,
                                                ← category.assoc, ← eval_map, ← functor.comp_map,
                                                ← nat_trans.naturality, category.assoc],
                                            symmetry, apply category.id_comp } } }),
      shape' := λ i j h, (choices j).is_limit.hom_ext (by { intro u, simp,
                                                            rw (F.obj u).shape' i j h, simp }),
      d_comp_d' := λ i j k hij hjk, (choices k).is_limit.hom_ext (λ u, by simp) },
    π := {
      app := λ u, {
        f := λ i, (choices i).cone.π.app u,
        comm' := λ i j hij, eq.symm ((choices j).is_limit.fac _ u)
      },
      naturality' := by { intros u v f, ext i,
                          exact eq.trans (category.id_comp _) 
                                         (eq.trans (category.id_comp _).symm
                                                   ((choices i).cone.π.naturality f)) } } }

def homological_complex.cone_of_degreewise_cones_is_limit_cone
  {J : Type u} [category.{u'} J] {V : Type v} [category.{v'} V] [has_zero_morphisms V]
  {ι : Type idx} {c : complex_shape ι} 
  (F : J ⥤ homological_complex V c)
  (choices : Π (i : ι), limit_cone (F ⋙ homological_complex.eval V c i))
  : is_limit (homological_complex.cone_of_degreewise_cones F choices) := {
  lift := λ s, {
      f := λ i, (choices i).is_limit.lift (category_theory.functor.map_cone (eval V c i) s),
      comm' := λ i j hij, (choices j).is_limit.hom_ext
                            (by { intro, delta homological_complex.cone_of_degreewise_cones,
                                  simp }),
    },
  uniq' := λ s m h, by { ext i, dsimp [homological_complex.cone_of_degreewise_cones] at h ⊢,
                         apply (choices i).is_limit.uniq' ((eval V c i).map_cone s),
                         intro j, 
                         have := congr_arg homological_complex.hom.f (h j),
                         exact congr_arg (function.eval i) this },
  fac' := λ s u, by { ext i, apply (choices i).is_limit.fac' ((eval V c i).map_cone s) u } }

end