English
If two finite root systems P and Q over a characteristic-zero ring are given along with a linear equivalence f: M ≃ M₂ and an index bijection e: ι ≃ ι₂ preserving roots, then there exists an isomorphism of root systems between P and Q expressed via the root-pairing structure.
Русский
Если две конечные корневые системы P и Q заданы вместе с линейным тождеством f: M ≃ M₂ и биекция индексов e: ι ≃ ι₂, сохраняющими корни, то существует изоморфизм корневых систем между P и Q, совместимый с их структурой парирования корней.
LaTeX
$$$\\\\exists f : M \\\\cong_R M_2, \\\\exists e : ι \\\\simeq ι_2 \\\\text{ such that } \\\\forall i, f(P.root i) = Q.root(e i) \\\\Rightarrow P \\\\Equiv Q.toRootPairing.$$$
Lean4
/-- For finite roots systems in characteristic zero, a linear equivalence preserving roots, also
preserves coroots, and is thus an equivalence of root systems. -/
def mk' [CharZero R] [NoZeroSMulDivisors R M₂] [Finite ι₂] (P : RootSystem ι R M N) (Q : RootSystem ι₂ R M₂ N₂)
(f : M ≃ₗ[R] M₂) (e : ι ≃ ι₂) (hf : ∀ i, f (P.root i) = Q.root (e i)) : P.Equiv Q.toRootPairing
where
weightMap := f
coweightMap := Q.flip.toPerfPair.trans (f.dualMap.trans P.flip.toPerfPair.symm)
indexEquiv := e
weight_coweight_transpose := by ext; simp [RootSystem.flip]
root_weightMap := by ext; simp [hf]
coroot_coweightMap :=
by
let g : N ≃ₗ[R] N₂ := P.flip.toPerfPair.trans <| f.symm.dualMap.trans Q.flip.toPerfPair.symm
suffices Q = P.map e f g by
ext i
rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]
conv_lhs => rw [this]
rfl
ext m n
· simp [RootSystem.map, RootPairing.map, RootSystem.flip, g]
· simp [hf, RootSystem.map, RootPairing.map]
bijective_weightMap := LinearEquiv.bijective _
bijective_coweightMap := LinearEquiv.bijective _
