English
The lie relation between e and f is governed by the h-e and h-f relations and yields zero in some nilpotent sense.
Русский
Связь Ли между e и f управляется отношениями h-e и h-f и приводит к нулю в некотором нильпотентном смысле.
LaTeX
$$Lie relations: [e_i, f_j] = δ_{ij} h_i with higher order constraints; in particular, for i ≠ j, [e_i, f_j] interacts trivially under crystallographic assumptions.$$
Lean4
/-- This is Lemma 2.6 from [Geck](Geck2017). -/
theorem chainBotCoeff_mul_chainTopCoeff :
(P.chainBotCoeff i m + 1) * (P.chainTopCoeff j k + 1) = (P.chainTopCoeff j l + 1) * (P.chainBotCoeff i k + 1) := by
/- Setup some typeclasses. -/
have := chainBotCoeff_mul_chainTopCoeff.isNotG2 hi hj hij h₁ h₂ h₃
letI := P.indexNeg
suffices
(P.chainBotCoeff i m + 1) * (P.chainBotCoeff j (-k) + 1) = (P.chainBotCoeff j (-l) + 1) * (P.chainBotCoeff i k + 1)
by
simpa
/- Establish basic relationships about roots and their sums / differences. -/
have him_mem : P.root i + P.root m ∈ range P.root := by rw [← h₂]; convert h₃ using 1; abel
have hik_mem : P.root k + P.root i ∈ range P.root := h₁ ▸ mem_range_self l
have hjk_mem : P.root j + P.root (-k) ∈ range P.root := by convert mem_range_self (-m) using 1;
simpa [sub_eq_add_neg] using congr(-$h₂)
have hjl_mem : P.root j + P.root (-l) ∈ range P.root := by rw [h₁, ← neg_mem_range_root_iff] at h₃;
convert h₃ using 1; simp [sub_eq_add_neg]
have h₁' : P.root (-k) - P.root i = P.root (-l) := by
simp only [root_reflectionPerm, reflection_apply_self, indexNeg_neg]; rw [← h₁]; abel
have h₂' : P.root (-k) + P.root j = P.root (-m) := by
simp only [root_reflectionPerm, reflection_apply_self, indexNeg_neg]; rw [← h₂]; abel
have h₃' : P.root (-k) + P.root j - P.root i ∈ range P.root := by
grind
/- Proceed to the main argument, following Geck's case splits. It's all just bookkeeping. -/
rcases aux_0 hik_mem with hki | ⟨hki, hik⟩
· /- Geck "Case 1" -/
exact aux_1 hi hj hij h₁ h₂ h₃ hki him_mem hjl_mem hjk_mem
rw [add_comm] at hik_mem hjk_mem
rcases aux_0 hjk_mem with hkj | ⟨hkj, hjk⟩
· /- Geck "Case 2" -/
simpa only [neg_neg] using
(aux_1 hj hi hij.symm h₂' h₁' h₃' hkj hjl_mem (by simpa only [neg_neg]) (by simpa only [neg_neg])).symm
suffices P.chainBotCoeff i m = P.chainBotCoeff j (-l) by rw [hik, hjk, this]
have aux₁ : ¬(P.chainBotCoeff i m = 1 ∧ P.chainBotCoeff j (-l) = 0) :=
aux_2 hi hj hij h₁ h₂ h₃ hki (by simpa using hkj) him_mem hjl_mem <| by rwa [add_comm]
have aux₂ : ¬(P.chainBotCoeff j (-l) = 1 ∧ P.chainBotCoeff i m = 0) := by
simpa using
aux_2 hj hi hij.symm h₂' h₁' h₃' hkj (by simpa) hjl_mem (by simpa only [neg_neg]) (by simpa only [neg_neg])
have aux₃ : P.chainBotCoeff i m = 0 ∨ P.chainBotCoeff i m = 1 :=
by
have := P.chainBotCoeff_if_one_zero him_mem
split at this <;> simp [this]
have aux₄ : P.chainBotCoeff j (-l) = 0 ∨ P.chainBotCoeff j (-l) = 1 :=
by
have := P.chainBotCoeff_if_one_zero hjl_mem
split at this <;> simp only [this, true_or, or_true]
cutsat
