equivalence_isCohomologous — Mathlib

English

There is an equivalence between IsCohomologous relation and equality of classes: γ1.class = γ2.class if and only if γ1 IsCohomologous γ2.

Русский

Существует эквивалентность между отношением IsCohomologous и равенством классов: γ1.class = γ2.class тогда и только тогда, когда γ1 IsCohomologous γ2.

LaTeX

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

Lean4

theorem equivalence_isCohomologous : _root_.Equivalence (IsCohomologous (G := G) (U := U))
    where
  refl γ := ⟨_, OneCohomologyRelation.refl γ.toOneCochain⟩
  symm := by
    rintro γ₁ γ₂ ⟨α, h⟩
    exact ⟨_, h.symm⟩
  trans := by
    rintro γ₁ γ₂ γ₂ ⟨α, h⟩ ⟨β, h'⟩
    exact ⟨_, h.trans h'⟩

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