English
If two RootSystems have Cartan matrices related by a finite index bijection, then they are equivalent as root pairings.
Русский
Если две корневые системы имеют Картановы матрицы, связанные биективным соответствием индексов, то они эквивалентны как корневые парные пары.
LaTeX
$$$\text{If } b, b_2 \text{ are RootSystems with Cartan matrices related by } e, \text{ then } P \equiv P_2^\text{root pairing}$$$
Lean4
theorem apply_mem_range_root_of_cartanMatrixEq (f : M ≃ₗ[R] M₂) (hf : ∀ i : b.support, f (P.root i) = P₂.root (e i))
(m : M) (hm : m ∈ range P.root) (he : ∀ i j, b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) :
f m ∈ range P₂.root :=
by
have (k : b.support) : (P.reflection k).trans f = f.trans (P₂.reflection (e k)) :=
by
suffices ∀ j : b.support, (P.reflection k).trans f (P.root j) = f.trans (P₂.reflection (e k)) (P.root j)
by
rw [← LinearEquiv.toLinearMap_inj]
exact b.toWeightBasis.ext fun j ↦ by simpa using this j
intro j
suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]
simpa only [cartanMatrixIn_def, algebraMap_pairingIn] using congr_arg (algebraMap ℤ R) (he j k)
obtain ⟨i, rfl⟩ := hm
apply b.induction_reflect i
· exact fun j ⟨k, hk⟩ ↦ ⟨P₂.reflectionPerm k k, by simpa⟩
· exact fun j hj ↦ ⟨e ⟨j, hj⟩, (hf _).symm⟩
· intro j k ⟨l, hl⟩ hk
replace this : f (P.reflection k (P.root j)) = (P₂.reflection (e ⟨k, hk⟩)) (f (P.root j)) := by
simpa using LinearEquiv.congr_fun (this ⟨k, hk⟩) (P.root j)
rw [root_reflectionPerm, this, ← hl, ← root_reflectionPerm]
exact mem_range_self _
