weightHom_injective — Mathlib

English

Similarly, the map coweightHom is injective on End P, by duality with weight maps.

Русский

Аналогично, отображение coweightHom инъективно на End P, дуальность с весовыми отображениями обеспечивает это.

LaTeX

$$Injective (coweightHom P)$$

Lean4

theorem weightHom_injective (P : RootPairing ι R M N) : Injective (weightHom P) :=
  by
  intro f g hfg
  ext x
  · exact LinearMap.congr_fun hfg x
  · refine LinearEquiv.injective P.flip.toPerfPair ?_
    simp_rw [← weight_coweight_transpose_apply]
    exact congrFun (congrArg DFunLike.coe (congrArg LinearMap.dualMap hfg)) (P.flip.toPerfPair x)
  · refine Embedding.injective P.root ?_
    simp_rw [← root_weightMap_apply]
    exact congrFun (congrArg DFunLike.coe hfg) (P.root x)

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