class_eq_iff

Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

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

English

For OneCocycle G U, γ1 IsCohomologous γ2 iff γ1.class = γ2.class.

Русский

Для OneCocycle G U, γ1 IsCohomologous γ2 эквивалентно равенству классов.

LaTeX

$$γ1.class = γ2.class ↔ γ1.IsCohomologous γ2$$

Lean4

theorem class_eq_iff (γ₁ γ₂ : OneCocycle G U) : γ₁.class = γ₂.class ↔ γ₁.IsCohomologous γ₂ :=
  (equivalence_isCohomologous _ _).quot_mk_eq_iff _ _

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

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

Разделы

Аффилиация

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