isBoundary₀_of_mem_coinvariantsKer

English

If x lies in the 1-boundaries subgroup of Rep.ofDistribMulAction, then x is a 1-boundary.

Русский

Если x лежит в подгруппе 1-граничностей Rep.ofDistribMulAction, то x является 1-граничностью.

LaTeX

$$$x \in boundaries_1 (Rep.ofDistribMulAction k G A) \Rightarrow IsBoundary_1 x$$$

Lean4

theorem isBoundary₀_of_mem_coinvariantsKer (x : A)
    (hx : x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)) : IsBoundary₀ G x :=
  Submodule.span_induction (fun _ ⟨g, hg⟩ => ⟨single g.1⁻¹ g.2, by simp_all⟩) ⟨0, by simp⟩
    (fun _ _ _ _ ⟨X, hX⟩ ⟨Y, hY⟩ => ⟨X + Y, by simp_all [sum_add_index', add_sub_add_comm]⟩)
    (fun r _ _ ⟨X, hX⟩ => ⟨r • X, by simp [← hX, sum_smul_index', smul_comm, smul_sub, smul_sum]⟩) hx

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