H1IsoOfIsTrivial — Mathlib

English

If A is a trivial G-representation, then the first cohomology H1(G,A) is naturally isomorphic to the group of additive group homomorphisms from G to A.

Русский

Если A является тривиальным представлением G, то H1(G,A) естественно изоморфна группе(additive) всех односторонних гомоморфизмов от G в A.

LaTeX

$$$H^1(G,A) \\cong \\operatorname{Hom}_{\\mathrm{Add}}(G,A)$$$

Lean4

/-- When `A : Rep k G` is a trivial representation of `G`, `H¹(G, A)` is isomorphic to the
group homs `G → A`. -/
def H1IsoOfIsTrivial : H1 A ≅ ModuleCat.of k (Additive G →+ A) :=
  (HomologicalComplex.isoHomologyπ _ 0 1 (CochainComplex.prev_nat_succ 0) <| by ext;
        simp [inhomogeneousCochains.d_def, inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
          Pi.zero_apply (M := fun _ => A)]).symm ≪≫
    isoCocycles₁ A ≪≫ cocycles₁IsoOfIsTrivial A

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