English
For a reduced irreducible crystallographic root system, either all pairings satisfy a swap-or- double relation or all satisfy a swap-or- triple relation, uniformly for all i,j.
Русский
Для сахаристовой корневой системы, либо во всех парах индексов выполняется симметрическая связь с множителями 1 и 2, либо соотношение с множителями 1 и 3, одинаково для всех пар i,j.
LaTeX
$$$(\forall i,j,\ P.pairing i j = P.pairing j i \lor P.pairing i j = 2 \cdot P.pairing j i \lor P.pairing j i = 2 \cdot P.pairing i j) \lor (\forall i,j,\ P.pairing i j = P.pairing j i \lor P.pairing i j = 3 \cdot P.pairing j i \lor P.pairing j i = 3 \cdot P.pairing i j)$$$
Lean4
theorem forall_pairing_eq_swap_or [P.IsReduced] [P.IsIrreducible] :
(∀ i j, P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
(∀ i j, P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j) :=
by
have : Fintype ι := Fintype.ofFinite ι
have B := (P.posRootForm ℤ).toInvariantForm
by_cases h : ∀ i j, B.form (α i) (α i) = B.form (α j) (α j)
· refine Or.inl fun i j ↦ Or.inl ?_
have := B.pairing_mul_eq_pairing_mul_swap j i
rwa [h i j, mul_left_inj' (B.ne_zero j)] at this
push_neg at h
obtain ⟨i, j, hij⟩ := h
have key := B.apply_eq_or_of_apply_ne hij
set li := B.form (α i) (α i)
set lj := B.form (α j) (α j)
have : (li = 2 * lj ∨ lj = 2 * li) ∨ (li = 3 * lj ∨ lj = 3 * li) := by have := B.apply_eq_or i j; tauto
rcases this with this | this
· refine Or.inl fun k₁ k₂ ↦ ?_
have hk := B.pairing_mul_eq_pairing_mul_swap k₁ k₂
rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
· refine Or.inr fun k₁ k₂ ↦ ?_
have hk := B.pairing_mul_eq_pairing_mul_swap k₁ k₂
rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk <;>
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
