hasHomology_of_iso

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.hasHomology_of_iso

English

If e: S1 ≅ S2 and S1 has Homology, then S2 has Homology.

Русский

Если e: S1 ≅ S2 и у S1 есть гомология, то у S2 также есть гомология.

LaTeX

$$$HasHomology(S_2)$$$

Lean4

theorem hasHomology_of_iso (e : S₁ ≅ S₂) [HasHomology S₁] : HasHomology S₂ :=
  HasHomology.mk' (HomologyData.ofIso e S₁.homologyData)

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

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

Разделы

Аффилиация

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