instHasMapBifunctorObjIntShiftFunctor_1

English

The instance provides a total HasMapBifunctor structure for shifting by an integer in the CochainComplex context.

Русский

Инстанс обеспечивает общую структуру HasMapBifunctor для сдвига на целое число в контексте коцепанского комплекса.

LaTeX

$$$ \text{HasMapBifunctor } K_1 (K_2\llbracket y \rrbracket) F $$$

Lean4

instance : HasMapBifunctor K₁ (K₂⟦y⟧) F :=
  HomologicalComplex₂.hasTotal_of_iso (mapBifunctorHomologicalComplexShift₂Iso K₁ K₂ F y).symm _

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