mapBifunctorHomologicalComplex — Mathlib

Lean4
/-- Given a functor `F : C₁ ⥤ C₂ ⥤ D`, this is the bifunctor which sends
`K₁ : HomologicalComplex C₁ c₁` and `K₂ : HomologicalComplex C₂ c₂` to the bicomplex
which is degree `(i₁, i₂)` consists of `(F.obj (K₁.X i₁)).obj (K₂.X i₂)`. -/
@[simps! obj_obj_X_X obj_obj_X_d obj_obj_d_f obj_map_f_f map_app_f_f]
def mapBifunctorHomologicalComplex : HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂
    where
  obj := mapBifunctorHomologicalComplexObj F c₂
  map {K₁ K₁'}
    f :=
    {
      app := fun K₂ =>
        HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X)
          (by
            intros
            dsimp
            simp only [← NatTrans.comp_app, ← F.map_comp, f.comm])
          (by simp) }
Похожие утверждения