Lean4
/-- A complex of functors gives a functor to complexes. -/
@[simps obj map]
def asFunctor {T : Type*} [Category T] (C : HomologicalComplex (T ⥤ V) c) : T ⥤ HomologicalComplex V c
where
obj
t :=
{ X := fun i => (C.X i).obj t
d := fun i j => (C.d i j).app t
d_comp_d' := fun i j k _ _ => by
have := C.d_comp_d i j k
rw [NatTrans.ext_iff, funext_iff] at this
exact this t
shape := fun i j h => by
have := C.shape _ _ h
rw [NatTrans.ext_iff, funext_iff] at this
exact this t }
map
h :=
{ f := fun i => (C.X i).map h
comm' := fun _ _ _ => NatTrans.naturality _ _ }
map_id
t := by
ext i
dsimp
rw [(C.X i).map_id]
map_comp h₁
h₂ := by
ext i
dsimp
rw [Functor.map_comp]
-- TODO in fact, this is an equivalence of categories.
