English
If P.pairingIn ℤ i j > 0 and i ≠ j, then α i − α j lies in the root set Φ.
Русский
Если P.pairingIn ℤ i j > 0 и i ≠ j, то α i − α j принадлежит множеству корней Φ.
LaTeX
$$α i - α j ∈ Φ$$
Lean4
theorem root_sub_root_mem_of_pairingIn_pos (h : 0 < P.pairingIn ℤ i j) (h' : i ≠ j) : α i - α j ∈ Φ :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
by_cases hli : LinearIndependent R ![α i, α j]
· -- The case where the two roots are linearly independent
suffices P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
by
rcases this with h₁ | h₁
· replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
· replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
rw [← neg_mem_range_root_iff, neg_sub]
exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩
have : P.coxeterWeightIn ℤ i j ∈ ({ 1, 2, 3 } : Set _) :=
by
have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
simp_all
simp_rw [coxeterWeightIn, Int.mul_mem_one_two_three_iff, mem_insert_iff, mem_singleton_iff, Prod.mk.injEq] at this
cutsat
· -- The case where the two roots are linearly dependent
have : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(1, 4), (2, 2), (4, 1)} : Set _) :=
by
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
replace hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4 :=
(P.coxeterWeightIn_eq_four_iff_not_linearIndependent ℤ).mpr hli
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk.injEq] at this
rcases this with hij | hij | hij
· rw [(P.pairingIn_one_four_iff ℤ i j).mp hij, two_smul, sub_add_cancel_right]
exact neg_root_mem P i
· rw [P.pairingIn_two_two_iff] at hij
contradiction
· rw [and_comm] at hij
simp [(P.pairingIn_one_four_iff ℤ j i).mp hij, two_smul]
