instHasMapBifunctorFlip

Mathlib.Algebra.Homology.BifunctorFlip

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instHasMapBifunctorFlip

English

The ιOrZero morphism aligns with the associator when the index falls away from the main simplex; otherwise it is zero.

Русский

Морфизм ιOrZero согласуется с ассоциатором, если индекс вне главного симплекса; иначе нулевой.

LaTeX

$$ιOrZero_hom compatibility$$

Lean4

instance : HasMapBifunctor K₂ K₁ F.flip c := by
  rw [hasMapBifunctor_flip_iff]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru