H1AddEquivOfIsTrivial_single — Mathlib

English

For a trivial A and any g ∈ G, the image of single g a corresponds to H1π A applied to cycles₁IsoOfIsTrivial inv (single g a).

Русский

Для тривиального A и любого g ∈ G отображение single g a в H1AddEquivOfIsTrivial совпадает с изображением через H1π A.

LaTeX

$$theorem H1AddEquivOfIsTrivial_single (g : G) (a : A) :\n H1AddEquivOfIsTrivial A (H1π A <| (cycles₁IsoOfIsTrivial A).inv (single g a)) =\n Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a$$

Lean4

@[simp]
theorem H1AddEquivOfIsTrivial_single (g : G) (a : A) :
    H1AddEquivOfIsTrivial A (H1π A <| (cycles₁IsoOfIsTrivial A).inv (single g a)) =
      Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a :=
  by rw [H1AddEquivOfIsTrivial_apply, H1ToTensorOfIsTrivial_H1π_single g a]

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