cocycles₁IsoOfIsTrivial — Mathlib

English

If A is trivial, there is a linear isomorphism of k-modules between cocycles1(A) and Additive G →+ A, i.e., Z^1(G,A) ≅ Hom_+(G,A).

Русский

Если A тривиально, существует линейное изоморфизм между Z^1(G,A) и Additive G →+ A, то есть Z^1(G,A) ≅ Hom_+(G,A).

LaTeX

$$$$ ModuleCat.of_k(cocycles_1(A)) \\cong ModuleCat.of_k(Additive G \\rightarrow^+ A). $$$$

Lean4

/-- When `A : Rep k G` is a trivial representation of `G`, `Z¹(G, A)` is isomorphic to the
group homs `G → A`. -/
@[simps!]
def cocycles₁IsoOfIsTrivial [hA : A.IsTrivial] : ModuleCat.of k (cocycles₁ A) ≅ ModuleCat.of k (Additive G →+ A) :=
  LinearEquiv.toModuleIso
    { toFun
        f :=
        { toFun := f ∘ Additive.toMul
          map_zero' := cocycles₁_map_one f
          map_add' := cocycles₁_map_mul_of_isTrivial f }
      map_add' _ _ := rfl
      map_smul' _ _ := rfl
      invFun
        f :=
        { val := f
          property := mem_cocycles₁_of_addMonoidHom f } }

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