cycles₁IsoOfIsTrivial — Mathlib

English

The hom component of the isomorphism cycles1IsoOfIsTrivial acts as the identity on elements of Z1(G,A).

Русский

Гомоморфная часть изоморфизма cycles1IsoOfIsTrivial действует как тождественное отображение на элементах Z1(G,A).

LaTeX

$$(cycles1IsoOfIsTrivial A).hom x = x$$

Lean4

/-- The natural inclusion `Z₁(G, A) ⟶ C₁(G, A)` is an isomorphism when the representation
on `A` is trivial. -/
def cycles₁IsoOfIsTrivial [A.IsTrivial] : ModuleCat.of k (cycles₁ A) ≅ ModuleCat.of k (G →₀ A) :=
  (LinearEquiv.ofTop _ (cycles₁_eq_top_of_isTrivial A)).toModuleIso

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