coinvariantsEquiv — Mathlib

English

There is a canonical linear isomorphism between the coinvariants ρ.Coinvariants and the quotient V / Im(ρ(g) − Id).

Русский

Существует каноническое линейное изоморфизм между коинвариантами ρ.Coinvariants и фактор-момолью V / Im(ρ(g) − Id).

LaTeX

$$$ \rho.Coinvariants \cong_{k} V / \operatorname{Im}(\rho(g) - \mathrm{id}) $$$

Lean4

/-- Given a finite cyclic group `G` generated by `g` and a `G` representation `(V, ρ)`, `V_G` is
isomorphic to `V ⧸ Im(ρ(g - 1))`. -/
noncomputable def coinvariantsEquiv (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ρ.Coinvariants ≃ₗ[k] (_ ⧸ LinearMap.range (ρ g - LinearMap.id)) :=
  Submodule.quotEquivOfEq _ _ (coinvariantsKer_eq_range ρ g hg)

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