English
The alternatingFaceMapComplex.map is a natural transformation respecting degree-wise components.
Русский
Map из AlternatingFaceMapComplex.map является естественным преобразованием, сохраняющим компоненты по степеням.
LaTeX
$$$\mathrm{map} f$ is a natural transformation with components $(\mathrm{map} f)_n = f_{\langle n \rangle}$$$
Lean4
theorem map_alternatingFaceMapComplex {D : Type*} [Category D] [Preadditive D] (F : C ⥤ D) [F.Additive] :
alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex _ =
(SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D :=
by
apply CategoryTheory.Functor.ext
· intro X Y f
ext n
simp only [Functor.comp_map, HomologicalComplex.comp_f, alternatingFaceMapComplex_map_f,
Functor.mapHomologicalComplex_map_f, HomologicalComplex.eqToHom_f, eqToHom_refl, comp_id, id_comp,
SimplicialObject.whiskering_obj_map_app]
· intro X
apply HomologicalComplex.ext
· rintro i j (rfl : j + 1 = i)
dsimp only [Functor.comp_obj]
simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d, eqToHom_refl, id_comp, comp_id,
AlternatingFaceMapComplex.objD, Functor.map_sum, Functor.map_zsmul]
rfl
· ext n
rfl