H1π_comp_map

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

URI: https://scilib.ai/kg/mathlib#groupCohomology.H1π_comp_map

← MathLib Explorer

English

Exactness is expressed by Im(f) = Ker(g).

Русский

Точность выражается равенством Im(f) = Ker(g).

LaTeX

$$$\operatorname{Im}(f) = \ker(g)$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem H1π_comp_map : H1π A ≫ map f φ 1 = mapCocycles₁ f φ ≫ H1π B := by
  simp [H1π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₁_hom_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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