coboundariesToCocycles₁ — Mathlib

English

There is a natural inclusion of coboundaries into cocycles1 as a linear map.

Русский

Существует естественное включение границ в cocycles₁ как линейного отображения.

LaTeX

$$$$ coboundariesToCocycles_1 : coboundaries_1(A) \\rightarrow\\ell\\!_k cocycles_1(A). $$$$

Lean4

/-- Natural inclusion `B¹(G, A) →ₗ[k] Z¹(G, A)`. -/
abbrev coboundariesToCocycles₁ : coboundaries₁ A →ₗ[k] cocycles₁ A :=
  Submodule.inclusion (coboundaries₁_le_cocycles₁ A)

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