English
For finite root systems in characteristic zero, a linear equivalence preserving roots induces a root system equivalence.
Русский
Для конечных корневых систем в характеристике ноль линейное отображение, сохраняющее корни, индуцирует эквиверацию корневых систем.
LaTeX
$$$\\\\exists P,Q, f,e, hf:\\\\forall i,\n f(P.root i) = Q.root (e i) \\\\Rightarrow P.Equiv Q.toRootPairing.$$$
Lean4
/-- The coweight space representation of automorphisms -/
@[simps]
def coweightHom (P : RootPairing ι R M N) : Aut P →* (N ≃ₗ[R] N)ᵐᵒᵖ
where
toFun g := MulOpposite.op (coweightEquiv P P g)
map_one' := by
simp only [MulOpposite.op_eq_one_iff]
exact LinearEquiv.toLinearMap_inj.mp rfl
map_mul' := by
simp only [mul_eq_comp, coweightEquiv_comp_toLin]
exact fun x y ↦ rfl
