mkH1OfIsTrivial_apply — Mathlib

English

If A is trivial, there is a natural map from H1 A to (Z-linear) Abelianization G ⊗ A.

Русский

Если A тривиально, существует естественное отображение H1 A → (Abelianization G) ⊗ℤ A.

LaTeX

$$$H_1 A \\to (\\mathbb{Z}-\\text{module}) (\\operatorname{Abelianization} G) \\otimes_{\\mathbb{Z}} A$$$

Lean4

@[simp]
theorem mkH1OfIsTrivial_apply (g : G) (a : A) :
    mkH1OfIsTrivial A (Additive.ofMul (Abelianization.of g)) a = H1π A ((cycles₁IsoOfIsTrivial A).inv (single g a)) :=
  rfl

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