class

Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PresheafOfGroups.OneCocycle.class

Lean4

/-- The cohomology class of a 1-cocycle. -/
def «class» (γ : OneCocycle G U) : H1 G U :=
  Quot.mk _ γ

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

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

Разделы

Аффилиация

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