ofEpiOfIsIsoOfMono_g'

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_g'

English

For φ, h, and the data, the g' component of the constructed right homology data satisfies (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃.

Русский

Для φ, h и данных выполняется: (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃.

LaTeX

$$$ (\\mathrm{ofEpiOfIsIsoOfMono}\\ φ\ h).g' = h.g' \\circ φ.τ_3 $$$

Lean4

@[simp]
theorem ofEpiOfIsIsoOfMono_g' : (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃ := by simp [ofEpiOfIsIsoOfMono, opMap]

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

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

Разделы

Аффилиация

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