instHasMapProdObjGradedObjectFunctorMapBifunctorXπ

English

There exists a canonical map associated to the π-index in the bifunctor construction, arising from applying a bifunctor to a pair of chain complexes and then projecting to the π-component; this map is well-defined and respects zero morphisms.

Русский

Существует каноническое отображение, связанное с π-индексом в построении бифунктора, получаемом при применении бифунктора к паре комплексов и проекции на π-компоненту; отображение корректно определено и сохраняет нули Морфизмов.

LaTeX

$$$\\text{There exists a canonical morphism }\\Pi: (K_1 \\text{ X } X) \\otimes (K_2 \\text{ X } X) \\to K_3 \\text{ X } X \\quad\\text{(in the totalized bifunctor context with } \\pi).$$$

Lean4

instance : (((GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (ComplexShape.π c₁ c₂ c₁₂) :=
  inferInstanceAs (HasMapBifunctor K₁ K₂ F₁₂ c₁₂)

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