coboundariesToCocycles₁_apply — Mathlib

English

Let A be a representation of G over k. The map from 1-coboundaries to 1-cocycles acts by taking the underlying function, i.e. for any x in coboundaries1(A), coboundariesToCocycles1 A x equals the first component of x.

Русский

Пусть A — представление группы G над кольцом k. Отображение из B^1(A) в Z^1(A) действует как проекция на функцию: для любого x ∈ coboundaries1(A) выполняется coboundariesToCocycles1 A x = x.1.

LaTeX

$$$\forall x \in \text{coboundaries}_1(A),\; \text{coboundariesToCocycles}_1(A)(x) = x.1$$$

Lean4

@[simp]
theorem coboundariesToCocycles₁_apply (x : coboundaries₁ A) : coboundariesToCocycles₁ A x = x.1 :=
  rfl

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