mapBifunctorHomologicalComplexShift₂Iso

English

As above, the canonical isomorphism between the shifted and mapped bifunctors with signs.

Русский

Как выше, каноническое изоморфизм между сдвинутым и отображаемым бифунктором с знаками.

LaTeX

$$$ mapBifunctorHomologicalComplexShift₂Iso K_1 K_2 F y i \;: \; \text{(explicit iso)} $$$

Lean4

/-- Auxiliary definition for `mapBifunctorShift₂Iso`. -/
@[simps! hom_f_f inv_f_f]
def mapBifunctorHomologicalComplexShift₂Iso :
    ((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj (K₂⟦y⟧) ≅
      (HomologicalComplex₂.shiftFunctor₂ D y).obj (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂) :=
  HomologicalComplex.Hom.isoOfComponents (fun i₁ => HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _))
    (by
      intros
      ext
      dsimp
      simp only [id_comp, comp_id])

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