English
There exists two integers p<0 and q>0 such that genWeightSpace SmulAdd eq_bot for χ1 and χ2 yield the bottom in both p and q.
Русский
Существуют целые p<0 и q>0, такие что genWeightSpace(помножение) для χ1, χ2 дают нижний предел в p и q.
LaTeX
$$$\exists p<0, q>0, genWeightSpace(M, p \cdot χ_1 + χ_2) = ⊥ \land genWeightSpace(M, q \cdot χ_1 + χ_2) = ⊥$$$
Lean4
/-- Given a (potential) root `α` relative to a Cartan subalgebra `H`, if we restrict to the ideal
`I = corootSpace α` of `H` (informally, `I = ⁅H(α), H(-α)⁆`), we may find an
integral linear combination between `α` and any weight `χ` of a representation.
This is Proposition 4.4 from [carter2005] and is a key step in the proof that the roots of a
semisimple Lie algebra form a root system. It shows that the restriction of `α` to `I` vanishes iff
the restriction of every root to `I` vanishes (which cannot happen in a semisimple Lie algebra). -/
theorem exists_forall_mem_corootSpace_smul_add_eq_zero [IsDomain R] [IsPrincipalIdealRing R] [CharZero R]
[NoZeroSMulDivisors R M] [IsNoetherian R M] (hα : α ≠ 0) (hχ : genWeightSpace M χ ≠ ⊥) :
∃ a b : ℤ, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0 :=
by
obtain ⟨p, hp₀, q, hq₀, hp, hq⟩ := exists₂_genWeightSpace_smul_add_eq_bot M α χ hα
let a := ∑ i ∈ Finset.Ioo p q, finrank R (genWeightSpace M (i • α + χ)) • i
let b := ∑ i ∈ Finset.Ioo p q, finrank R (genWeightSpace M (i • α + χ))
have hb : 0 < b :=
by
replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]
refine Finset.sum_pos' (fun _ _ ↦ zero_le _) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩
rw [zero_smul, zero_add]
exact finrank_pos
refine ⟨a, b, Int.natCast_pos.mpr hb, fun x hx ↦ ?_⟩
let N : ℤ → Submodule R M := fun k ↦ genWeightSpace M (k • α + χ)
have h₁ : iSupIndep fun (i : Finset.Ioo p q) ↦ N i :=
by
rw [LieSubmodule.iSupIndep_toSubmodule]
refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_
exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij
have h₂ : ∀ i, MapsTo (toEnd R H M x) ↑(N i) ↑(N i) := fun _ _ ↦ LieSubmodule.lie_mem _
have h₃ : genWeightSpaceChain M α χ p q = ⨆ i ∈ Finset.Ioo p q, N i := by
simp_rw [N, genWeightSpaceChain_def', LieSubmodule.iSup_toSubmodule]
rw [← trace_toEnd_genWeightSpaceChain_eq_zero M α χ p q hp hq hx, ← LieSubmodule.toEnd_restrict_eq_toEnd]
-- The lines below illustrate the cost of treating `LieSubmodule` as both a
-- `Submodule` and a `LieSubmodule` simultaneously.
#adaptation_note /-- 2025-06-18 (https://github.com/leanprover/lean4/issues/8804).
The `erw` causes a kernel timeout if there is no `subst`. -/
subst a b N
erw [LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃]
simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]
convert_to
_ =
∑ k ∈ Finset.Ioo p q,
(LinearMap.trace R { x // x ∈ (genWeightSpace M (k • α + χ)) })
((toEnd R { x // x ∈ H } { x // x ∈ genWeightSpace M (k • α + χ) }) x)
simp_rw [trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add, ← smul_assoc, Finset.sum_add_distrib, ←
Finset.sum_smul, natCast_zsmul]
