H1IsoOfIsTrivial_H1π_apply_apply

English

For a cocycle f in cocycles1(A) and a group element x, the isomorphism H1IsoOfIsTrivial maps H1π A f to a function whose value at x is f(x.toMul).

Русский

Для коцепиля f в cocycles1(A) и элемента группы x отображение H1IsoOfIsTrivial применимо к H1π A f так, что значение в x равно f(x.toMul).

LaTeX

$$$(H1IsoOfIsTrivial(A))\mathrm{.hom}(H1\pi(A)\,f)\,x = f\,(x^{\mathrm{toMul}})$$$

Lean4

theorem H1IsoOfIsTrivial_H1π_apply_apply (f : cocycles₁ A) (x : Additive G) :
    (H1IsoOfIsTrivial A).hom (H1π A f) x = f x.toMul := by simp

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