Lean4
/-- Lemma 3.5 from [Geck](Geck2017). -/
theorem lie_e_f_ne [P.IsReduced] [P.IsIrreducible] : ⁅e i, f j⁆ = 0 :=
by
letI := P.indexNeg
classical
ext (k | k) (l | l)
· aesop (erase simp indexNeg_neg) (add simp [e, f, Matrix.mul_apply, mul_ite, ite_mul])
· exact lie_e_f_ne_aux₀ k l
· have aux₁ : P.root k ≠ P.root i - P.root j := fun contra ↦ b.sub_notMem_range_root i.property j.property ⟨k, contra⟩
simp [e, f, ← sub_eq_add_neg, if_neg aux₁]
· /- Geck Case 1 (covered by the auxiliary lemmas above). -/
rcases eq_or_ne l j with rfl | h₃
· rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.zero_apply]
rcases eq_or_ne l (-i) with rfl | h₄
·
rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₂ hij, Pi.zero_apply, Matrix.zero_apply]
/- Geck Case 2.
It's all just definition unfolding and case analysis: the only real content is the external
lemma `chainBotCoeff_mul_chainTopCoeff`. -/
suffices
(∑ x,
if P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x then
((P.chainBotCoeff i x : R) + 1) * (P.chainTopCoeff j l + 1)
else 0) =
(∑ x,
if P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j then
((P.chainTopCoeff j x : R) + 1) * (P.chainBotCoeff i l + 1)
else 0)
by
have h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -i) ∧ k = -j) := by rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
have h₂ : ∀ x ∈ Finset.univ, ¬((x = j ∧ l = j) ∧ k = i) := by rintro - - ⟨⟨-, contra⟩, -⟩; contradiction
rw [← sub_eq_zero] at this
simpa [e, f, ← ite_and, Finset.sum_ite_of_false h₁, Finset.sum_ite_of_false h₂, -indexNeg_neg,
-Finset.univ_eq_attach]
by_cases h₅ : P.root l + P.root i - P.root j ∈ range P.root; swap
· have aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j) := by
rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
have aux₄ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
rintro x - ⟨hx, hx'⟩; exact h₅ ⟨k, by rw [hx', hx]; abel⟩
simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]
by_cases h₆ : P.root l + P.root i ∈ range P.root; swap
· have h₇ : P.root l - P.root j ∉ range P.root := by
rwa [b.root_sub_mem_iff_root_add_mem i j l (by aesop) i.property j.property (by aesop) (by aesop) h₅]
have aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j) := by
rintro x - ⟨hx, -⟩; exact h₆ ⟨x, by rw [hx]; abel⟩
have aux₄ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
rintro x - ⟨hx, hx'⟩; exact h₇ ⟨x, hx⟩
simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]
obtain ⟨m, hm : P.root m = P.root l - P.root j⟩ :=
b.root_sub_root_mem_of_mem_of_mem i j l (by aesop) i.property j.property h₅ h₃ h₆
obtain ⟨l', hl'⟩ := h₆
by_cases hk : P.root k = P.root l + P.root i - P.root j; swap
· grind
have aux₃ (x) (hx : x ≠ m) : ¬(P.root x = P.root l - P.root j ∧ P.root k = P.root i + P.root x) := by
grind [EmbeddingLike.apply_eq_iff_eq]
have aux₄ (x) (hx : x ≠ l') : ¬(P.root x = P.root i + P.root l ∧ P.root k = P.root x - P.root j) := by
grind [EmbeddingLike.apply_eq_iff_eq]
rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - h; rw [if_neg (aux₃ _ h)]),
Finset.sum_eq_single_of_mem l' (Finset.mem_univ _) (by rintro x - h; rw [if_neg (aux₄ _ h)]),
if_pos (⟨hm, by rw [hm, hk]; abel⟩), if_pos ⟨by rw [hl', add_comm], by rw [hl', hk]⟩]
have := chainBotCoeff_mul_chainTopCoeff i.property j.property (by aesop) hl'.symm hm.symm h₅
norm_cast
