p_opcyclesMap

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

English

If φ.f i is mono, then the induced cycles map is mono.

Русский

Если φ.f i моно, то циклическое отображение моно.

LaTeX

$$\mathrm{Mono}(\phi.f i) \Rightarrow \mathrm{Mono}(\mathrm{cyclesMap}\ \phi i)$$

Lean4

@[reassoc (attr := simp)]
theorem p_opcyclesMap : K.pOpcycles i ≫ opcyclesMap φ i = φ.f i ≫ L.pOpcycles i :=
  ShortComplex.p_opcyclesMap _

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

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

Разделы

Аффилиация

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