instAddCommGroupH

Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.instAddCommGroupH

English

Each cohomology group H^n(F) carries a natural abelian group structure.

Русский

Каждая когомология H^n(F) естественным образом имеет структуру абелевой группы.

LaTeX

$$$H(n) \in \mathrm{AddCommGrp}$$$

Lean4

noncomputable instance (n : ℕ) : AddCommGroup (F.H n) :=
  by
  dsimp only [H]
  infer_instance

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

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

Разделы

Аффилиация

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