English
The bottom coefficient after reflecting i on i matches the top coefficient with swapped roles.
Русский
Нижний коэффициент после отражения i на i совпадает с верхним коэффициентом после перестановки ролей.
LaTeX
$$$$ P.chainBotCoeff(i, P.reflectionPerm(i,i)) = P.chainTopCoeff(i, j) $$$$
Lean4
theorem chainBotCoeff_sub_chainTopCoeff : P.chainBotCoeff i j - P.chainTopCoeff i j = P.pairingIn ℤ j i :=
by
suffices
∀ i j, LinearIndependent R ![P.root i, P.root j] → P.chainBotCoeff i j - P.chainTopCoeff i j ≤ P.pairingIn ℤ j i
by
refine le_antisymm (this i j h) ?_
specialize this (P.reflectionPerm i i) j (by simpa)
simp only [chainBotCoeff_reflectionPerm_left, chainTopCoeff_reflectionPerm_left,
pairingIn_reflectionPerm_self_right] at this
cutsat
intro i j h
have h₁ :
P.reflection i (P.root <| P.chainBotIdx i j) = P.root j + (P.chainBotCoeff i j - P.pairingIn ℤ j i) • P.root i :=
by
simp [reflection_apply_root, ← P.algebraMap_pairingIn ℤ]
module
have h₂ : P.reflection i (P.root <| P.chainBotIdx i j) ∈ range P.root :=
by
rw [← root_reflectionPerm]
exact mem_range_self _
rw [h₁, root_add_zsmul_mem_range_iff h, mem_Icc] at h₂
omega
