English
The automorphism obtained by reflecting at a root i is an element of Aut(P) with weight and coroot maps given by reflections.
Русский
Автоморфизм, полученный отражением по корню i, принадлежит Aut(P) и имеет соответствующие отражающие весовую и корневую карты.
LaTeX
$$$\\\\text{reflection}(P,i) \\\\in Aut(P).$$$
Lean4
/-- The automorphism of a root pairing given by a reflection. -/
def reflection (P : RootPairing ι R M N) (i : ι) : Aut P
where
weightMap := P.reflection i
coweightMap := P.coreflection i
indexEquiv := P.reflectionPerm i
weight_coweight_transpose := by ext f x; simpa [reflection_apply, coreflection_apply] using mul_comm ..
root_weightMap := by ext; simp
coroot_coweightMap := by ext; simp
bijective_weightMap := by
simp only [LinearEquiv.coe_coe]
exact LinearEquiv.bijective (P.reflection i)
bijective_coweightMap := by
simp only [LinearEquiv.coe_coe]
exact LinearEquiv.bijective (P.coreflection i)
