weightHom — Mathlib

English

The function weightHom is injective as a map from End P to MonoidHom End P to weight data; equivalently, knowing the weight map of an endomorphism determines it uniquely.

Русский

Функция weightHom инъективна как отображение End P→MonoidHom; из веса эндоморфизма следует однозначно определить сам эндоморфизм.

LaTeX

$$Injective (weightHom P)$$

Lean4

/-- The weight space representation of endomorphisms -/
def weightHom (P : RootPairing ι R M N) : End P →* (Module.End R M)
    where
  toFun g := Hom.weightMap (P := P) (Q := P) g
  map_mul' g h := by ext; simp
  map_one' := by ext; simp

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