map_id — Mathlib

English

Let ρ be a G-representation on V. The map induced on coinvariants by the identity linear map on V is the identity map on the coinvariants.

Русский

Пусть ρ — G-представление пространства V. Отображение, индуцируемое тождественным линейным отображением на V, на когонвариантах есть тождественное отображение на когонвариантах.

LaTeX

$$$\\mathrm{map}_{\\rho,\\rho}(\\mathrm{id}_V) = \\mathrm{id}_{\\mathrm{Coinvariants}(\\rho)}$$$

Lean4

@[simp]
theorem map_id (ρ : Representation k G V) : map ρ ρ LinearMap.id (by simp) = LinearMap.id := by ext; rfl

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