boundariesOfIsBoundary₁ — Mathlib

English

The map boundariesOfIsBoundary₁ sends a 1-boundary in A to a 1-boundary in Rep.ofDistribMulAction.

Русский

Отображение boundariesOfIsBoundary₁ переводит 1-граничность из A в 1-граничность в Rep.ofDistribMulAction.

LaTeX

$$$boundariesOfIsBoundary_1 (x) (hx) : boundaries_1 (Rep.ofDistribMulAction k G A)$$$

Lean4

/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G →₀ A` satisfying the 1-boundary condition, produces a 1-boundary for the representation
on `A` induced by the `DistribMulAction`. -/
@[simps]
def boundariesOfIsBoundary₁ (x : G →₀ A) (hx : IsBoundary₁ x) : boundaries₁ (Rep.ofDistribMulAction k G A) :=
  ⟨x, hx⟩

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