ker — Mathlib

English

The coinvariants of a G-representation V are the quotient V modulo the submodule generated by all elements of the form ρ(g)x − x, for g in G and x in V.

Русский

Коинварианты представления G на V есть фактор-пространство V над подмодулем, порождаемым всеми элементами вида ρ(g)x − x, где g ∈ G, x ∈ V.

LaTeX

$$$\mathrm{Coinvariants}(\rho) = V / \mathrm{ker}(\rho)^{\mathrm{span}}$$$

Lean4

/-- The submodule of a representation generated by elements of the form `ρ g x - x`. -/
def ker : Submodule k V :=
  Submodule.span k (Set.range fun (gv : G × V) => ρ gv.1 gv.2 - gv.2)

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