English
Symmetric relation: chainTopCoeff α 0 equals 1, validated through a dual argument.
Русский
Симметричная связь: chainTopCoeff α 0 равно 1, доказано двойственным методом.
LaTeX
$$$\operatorname{chainTopCoeff}(α,0) = 1$$$
Lean4
theorem chainTopCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) : chainTopCoeff α (0 : Weight K H L) = 1 :=
by
symm
apply eq_of_le_of_not_lt
· rw [Nat.one_le_iff_ne_zero]
intro e
exact
α.2 (by simpa [e, Weight.coe_zero] using genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα)
obtain ⟨x, hx, x_ne0⟩ := (chainTop α (0 : Weight K H L)).exists_ne_zero
obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα
obtain rfl := isSl2.h_eq_coroot hα he hf
have prim : isSl2.HasPrimitiveVectorWith x (chainLength α (0 : Weight K H L) : K) :=
have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
⟨x_ne0, (chainLength_smul _ _ hx).symm, by rwa [genWeightSpace_add_chainTop _ _ hα] at this⟩
obtain ⟨k, hk⟩ : ∃ k : K, k • f = (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x :=
by
have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) :=
by
convert toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2
rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul', add_assoc, smul_neg, neg_add_cancel, add_zero]
simpa using
(finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simpa using isSl2.f_ne_zero)).mp (finrank_rootSpace_eq_one _ hα.neg)
⟨_, this⟩
apply_fun (⁅f, ·⁆) at hk
simp only [lie_smul, lie_self, smul_zero, prim.lie_f_pow_toEnd_f] at hk
intro e
refine prim.pow_toEnd_f_ne_zero_of_eq_nat rfl ?_ hk.symm
have := (apply_coroot_eq_cast' α 0).symm
simp only [← @Nat.cast_two ℤ, ← Nat.cast_mul, Weight.zero_apply, Int.cast_eq_zero, sub_eq_zero, Nat.cast_inj] at this
rwa [this, Nat.succ_le, two_mul, add_lt_add_iff_left]
