map_alternatingFaceMapComplex — Mathlib

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

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