English
There is a relation tying corootSpace α with sums a α + b χ on weights χ: membership of x in corootSpace α is equivalent to a linear relation holding for all x in corootSpace with coefficients a,b ∈ Z.
Русский
Существуют связи между corootSpace α и сумму весов a α + b χ, так что для всех x ∈ corootSpace α выполняется линейное соотношение с целыми a,b.
LaTeX
$$$\forall x \in \operatorname{corootSpace}(\alpha),\ (a \cdot \alpha + b \cdot \chi)(x) = 0$ for some integers a,b with b > 0.$$
Lean4
theorem eventually_genWeightSpace_smul_add_eq_bot : ∀ᶠ (k : ℕ) in Filter.atTop, genWeightSpace M (k • χ₁ + χ₂) = ⊥ :=
by
let f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
suffices Injective f
by
rw [← Nat.cofinite_eq_atTop, Filter.eventually_cofinite, ← finite_image_iff this.injOn]
apply (finite_genWeightSpace_ne_bot R L M).subset
simp [f]
intro k l hkl
replace hkl : (k : ℤ) • χ₁ = (l : ℤ) • χ₁ := by simpa only [f, add_left_inj, natCast_zsmul] using hkl
exact Nat.cast_inj.mp <| smul_left_injective ℤ hχ₁ hkl
