mk — Mathlib · SciLib

English

Equivalently, two representatives map to the same coinvariant iff their difference lies in the kernel of ρ.

Русский

Эквивалентно: две представления эквивалентны в коинвариантах тогда, когда их разность лежит в ядре ρ.

LaTeX

$$$mk_\rho x = mk_\rho y \iff x - y \in \mathrm{ker}(\rho)$$$

Lean4

/-- The quotient map from a representation to its coinvariants as a linear map. -/
def mk : V →ₗ[k] Coinvariants ρ :=
  Submodule.mkQ (ker ρ)

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