English
Inverse-weight map behaves dually with respect to the other invariant maps.
Русский
Обратная весовая карта образует двойственную структуру по отношению к другим инвариантным отображениям.
LaTeX
$$$ (symm P Q f).weightMap = (weightEquiv P Q f)^{-1} $$$
Lean4
/-- The inverse of a root pairing equivalence. -/
def symm {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N)
(Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) : RootPairing.Equiv Q P
where
weightMap := (weightEquiv P Q f).symm
coweightMap := (coweightEquiv P Q f).symm
indexEquiv := f.indexEquiv.symm
weight_coweight_transpose := by
ext n m
nth_rw
2 [show m = (weightEquiv P Q f) ((weightEquiv P Q f).symm m) by
exact (LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp rfl]
nth_rw
1 [show n = (coweightEquiv P Q f) ((coweightEquiv P Q f).symm n) by
exact (LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp rfl]
have := f.weight_coweight_transpose
rw [LinearMap.ext_iff₂] at this
exact Eq.symm (this ((coweightEquiv P Q f).symm n) ((weightEquiv P Q f).symm m))
root_weightMap := by
ext i
simp only [LinearEquiv.coe_coe, comp_apply]
have := f.root_weightMap
rw [funext_iff] at this
specialize this (f.indexEquiv.symm i)
simp only [comp_apply, Equiv.apply_symm_apply] at this
simp [← this]
coroot_coweightMap := by
ext i
simp only [LinearEquiv.coe_coe, comp_apply, Equiv.symm_symm]
have := f.coroot_coweightMap
rw [funext_iff] at this
specialize this (f.indexEquiv i)
simp only [comp_apply, Equiv.symm_apply_apply] at this
simp [← this]
bijective_weightMap := by
simp only [LinearEquiv.coe_coe]
exact LinearEquiv.bijective (weightEquiv P Q f).symm
bijective_coweightMap := by
simp only [LinearEquiv.coe_coe]
exact LinearEquiv.bijective (coweightEquiv P Q f).symm
