English
The weightHom map is injective, as argued by Geck’s construction; two endomorphisms with identical weight data are equal.
Русский
С помощью конструкций Geck весовое отображение инъективно: два эндоморфизма с одинаковыми весами совпадают.
LaTeX
$$Injective (weightHom P)$$
Lean4
theorem coweightHom_injective (P : RootPairing ι R M N) : Injective (coweightHom P) :=
by
intro f g hfg
ext x
· dsimp [coweightHom] at hfg
rw [MulOpposite.op_inj] at hfg
have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M) (σ₂₃ := .id R) P.flip.toPerfPair) hfg
rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h
have : f.weightMap = g.weightMap :=
by
haveI : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
refine
(Module.dualMap_dualMap_eq_iff R M).mp
(congrArg LinearMap.dualMap
((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))
exact congrFun (congrArg DFunLike.coe this) x
· dsimp [coweightHom] at hfg
simp_all only [MulOpposite.op_inj]
· dsimp [coweightHom] at hfg
rw [MulOpposite.op_inj] at hfg
set y := f.indexEquiv x with hy
have : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y) := by
exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)
rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this
rw [Equiv.symm_apply_apply] at this
rw [this, Equiv.apply_symm_apply]
