symm — Mathlib

English

If γ1 is cohomologous to γ2 via α, then γ2 is cohomologous to γ1 via α^{-1}.

Русский

Если γ1 эквивалентно γ2 через α, то γ2 эквивалентно γ1 через α^{-1}.

LaTeX

$$OneCohomologyRelation γ₂ γ₁ α⁻¹$$

Lean4

theorem symm {γ₁ γ₂ : OneCochain G U} {α : ZeroCochain G U} (h : OneCohomologyRelation γ₁ γ₂ α) :
    OneCohomologyRelation γ₂ γ₁ α⁻¹ := fun i j T a b ↦ by
  rw [← mul_left_inj (G.map b.op (α j)), mul_assoc, ← h i j a b, mul_assoc, Cochain₀.inv_apply, map_inv,
    inv_mul_cancel_left, Cochain₀.inv_apply, map_inv, inv_mul_cancel, mul_one]

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