asGroupHom — Mathlib

English

A representation ρ: G → Aut_k(V) yields a group homomorphism from G into the invertible k-linear endomorphisms of V; equivalently, there is a MonoidHom from G to Units(V →ₗ[k] V).

Русский

Пусть ρ: G → Aut_k(V) — линейное представление. Тогда существует гомоморфизм групп G в множество обратимых k-линейных отображений V в V, т.е. в MonoidHom G(Units(V →ₗ[k] V)).

LaTeX

$$$ asGroupHom : G \\to_* Units (V \\to_{{\\ k}} V) $$$

Lean4

/-- When `G` is a group, a `k`-linear representation of `G` on `V` can be thought of as
a group homomorphism from `G` into the invertible `k`-linear endomorphisms of `V`.
-/
def asGroupHom : G →* Units (V →ₗ[k] V) :=
  MonoidHom.toHomUnits ρ

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