H1IsoOfIsTrivial_inv_apply — Mathlib

English

For a monoid hom f: Additive G →+ A, the inverse under H1IsoOfIsTrivial equals H1π A applied to cocycles1IsoOfIsTrivial A inverse f.

Русский

Для моноидного гомоморфизма f: Additive G →+ A обратное к H1IsoOfIsTrivial действует как H1π A, применяя к f инвертированный cocycles₁IsoOfIsTrivial A.

LaTeX

$$$(H1IsoOfIsTrivial(A)).\mathrm{inv}(f) = H^1_\pi(A)( (cocycles_{1}^{\mathrm{Iso}}(A))^{\mathrm{inv}} f)$$$

Lean4

theorem H1IsoOfIsTrivial_inv_apply (f : Additive G →+ A) :
    (H1IsoOfIsTrivial A).inv f = H1π A ((cocycles₁IsoOfIsTrivial A).inv f) :=
  rfl

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