English
Two finite root systems over R with the same root data and compatible coroot ranges are equal; extensionality is provided by comparing their root data and coroot spans.
Русский
Две конечные корневые системы над R с одинаковыми данными корней и совместимыми диапазонами коротов равны; выпуклость следует из совпадения корневых данных и оболочек коретов.
LaTeX
$$$P_1.toLinearMap = P_2.toLinearMap \\;\\Rightarrow\\; P_1.root = P_2.root$ and $\\operatorname{range}P_1.coroot = \\operatorname{range}P_2.coroot$ implies $P_1 = P_2$$$
Lean4
/-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is
unique.
Formally, the point is that the hypothesis `hc` depends only on the range of the coroot mappings. -/
@[ext]
protected theorem ext [CharZero R] [NoZeroSMulDivisors R M] {P₁ P₂ : RootPairing ι R M N}
(he : P₁.toLinearMap = P₂.toLinearMap) (hr : P₁.root = P₂.root) (hc : range P₁.coroot = range P₂.coroot) :
P₁ = P₂ :=
by
have hp (hc' : P₁.coroot = P₂.coroot) : P₁.reflectionPerm = P₂.reflectionPerm :=
by
ext i j
refine P₁.root.injective ?_
conv_rhs => rw [hr]
simp only [root_reflectionPerm, reflection_apply, coroot']
simp only [hr, he, hc']
suffices P₁.coroot = P₂.coroot by obtain ⟨p₁⟩ := P₁; obtain ⟨p₂⟩ := P₂; grind
have := NoZeroSMulDivisors.int_of_charZero R M
ext i
apply P₁.injOn_dualMap_subtype_span_root_coroot (mem_range_self i) (hc ▸ mem_range_self i)
simp only [LinearMap.coe_comp, comp_apply]
apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
· exact Submodule.subset_span (mem_range_self i)
· exact P₁.coroot_root_two i
· exact P₁.mapsTo_reflection_root i
· exact hr ▸ he ▸ P₂.coroot_root_two i
· exact hr ▸ he ▸ P₂.mapsTo_reflection_root i
