coinvariantsKer_eq_range — Mathlib

English

For a finite cyclic group G generated by g and a representation ρ, the kernel of the coinvariants map equals the range of ρ(g) − Id.

Русский

Для конечной циклической группы G, порожденной g, и представления ρ, ядро карты коинвариант равно образу ρ(g) − Id.

LaTeX

$$$ \operatorname{ker}(\rho_{\mathrm{coinvariants}}) = \operatorname{range}(\rho(g) - \mathrm{id}) $$$

Lean4

theorem coinvariantsKer_eq_range (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    Coinvariants.ker ρ = LinearMap.range (ρ g - LinearMap.id) :=
  by
  refine le_antisymm (Submodule.span_le.2 ?_) ?_
  · rintro a ⟨⟨γ, α⟩, rfl⟩
    rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
    induction i with
    | zero => exact ⟨0, by simp⟩
    | succ n _ =>
      use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
      simpa using ρ.apply_sub_id_partialSum_eq _ _ _
  · rintro x ⟨y, rfl⟩
    simpa using Coinvariants.sub_mem_ker g y

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