English
For a functor F, a family X, differentials d and a zero-sq condition, the image of a ChainComplex via F is the ChainComplex of the images, with differentials mapped by F and the square relation preserved.
Русский
При применении F к ChainComplex образуется ChainComplex из изображений X(n) с дифференциалами F(d(n)); связь d(n+1)∘d(n)=0 сохраняется.
LaTeX
$$$(F.mapHomologicalComplex (ComplexShape.down \alpha)).obj (ChainComplex.of X d sq) = ChainComplex.of (n \mapsto F(X n)) (n \mapsto F(d n)) \;\; (\text{proof: } \forall n,\ F(d(n+1)) \circ F(d(n)) = 0)$$$
Lean4
theorem map_chain_complex_of (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (X : α → W₁) (d : ∀ n, X (n + 1) ⟶ X n)
(sq : ∀ n, d (n + 1) ≫ d n = 0) :
(F.mapHomologicalComplex _).obj (ChainComplex.of X d sq) =
ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) fun n => by
rw [← F.map_comp, sq n, Functor.map_zero] :=
by
refine HomologicalComplex.ext rfl ?_
rintro i j (rfl : j + 1 = i)
simp only [CategoryTheory.Functor.mapHomologicalComplex_obj_d, of_d, eqToHom_refl, comp_id, id_comp]
