weightHom_injective — Mathlib

English

The weight space representation is faithful: weightHom P is injective on Aut P.

Русский

Весовое представление является верным: weightHom P инъективно на Aut P.

LaTeX

$$$\\\\text{Injective}(\\\\mathrm{weightHom}(P)).$$$

Lean4

theorem weightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.weightHom P) :=
  by
  refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_
  let h : (weightHom P g).toLinearMap = (weightHom P g').toLinearMap := hgg'
  rw [weightHom_toLinearMap, weightHom_toLinearMap] at h
  suffices h' : g.toHom = g'.toHom by exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')
  exact Hom.weightHom_injective P hgg'

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