mapBifunctorShift₂Iso — Mathlib

English

The canonical isomorphism between mapBifunctorShift₁Iso and the shifted variant.

Русский

Канонический изоморфизм между mapBifunctorShift₁Iso и сдвинутым вариантом.

LaTeX

$$$ mapBifunctorShift₁Iso K_1 (K_2\llbracket y \rrbracket) F x \cong \mathrm{(shifted)} $$$

Lean4

/-- The canonical isomorphism `mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧`.
This isomorphism involves signs: on the summand `(F.obj (K₁.X p)).obj (K₂.X q)`, it is given
by the multiplication by `(p * y).negOnePow`. -/
noncomputable def mapBifunctorShift₂Iso : mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧ :=
  HomologicalComplex₂.total.mapIso (mapBifunctorHomologicalComplexShift₂Iso K₁ K₂ F y) (ComplexShape.up ℤ) ≪≫
    (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂).totalShift₂Iso y

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