English
For the RootSystem base b, the map i ↦ P.pairingIn ℤ i k (for fixed k ∈ b.support) is injective with respect to i.
Русский
Для базы b корневой системы отображение i ↦ P.pairingIn ℤ i k (при фиксированном k ∈ b.support) инъективно по i.
LaTeX
$$∀ k ∈ b.support, ∀ i ≠ j, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k$$
Lean4
/-- A characterisation of the connectedness of the Dynkin diagram for irreducible root pairings. -/
theorem induction_on_cartanMatrix [P.IsReduced] [P.IsIrreducible] (p : b.support → Prop) {i j : b.support} (hi : p i)
(hp : ∀ i j, p i → b.cartanMatrix j i ≠ 0 → p j) : p j :=
by
let q : Submodule R M := span R (P.root ∘ (↑) '' {i | p i})
have hq₀ : q ≠ ⊥ := q.ne_bot_iff.mpr ⟨P.root i, subset_span <| by simpa, P.ne_zero i⟩
have hq_mem (k : b.support) : P.root k ∈ q ↔ p k :=
by
refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩
contrapose! hk
exact b.linearIndepOn_root.linearIndependent.notMem_span_image hk
have hq_notMem (k : b.support) (hk : P.root k ∉ q) : q ≤ LinearMap.ker (P.coroot' k) :=
by
refine fun x hx ↦ LinearMap.mem_ker.mpr ?_
contrapose! hk
rw [hq_mem]
induction hx using Submodule.span_induction with
| mem x hx =>
obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by simp_all
replace hk : b.cartanMatrix k l ≠ 0 := by
rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
tauto
| zero => simp_all
| add x y hx hy hx'
hy' =>
replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
tauto
| smul a x hx hx' => simp_all
have hq : ∀ k, q ∈ invtSubmodule (P.reflection k) :=
by
rw [← b.forall_mem_support_invtSubmodule_iff]
refine fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_
rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply]
apply q.sub_mem hx
by_cases hk : P.root k ∈ q
· exact q.smul_mem _ hk
· replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
simp [hk]
simp [← hq_mem, IsIrreducible.eq_top_of_invtSubmodule_reflection q hq hq₀]
