English
The value of the weight β on the coroot α equals the integer expression chainLength α β minus twice the chainTopCoeff α β, interpreted in the base field: β(coroot α) = ↑(chainLength α β − 2 chainTopCoeff α β).
Русский
Значение веса β на короте α равно целочисленному выражению chainLength α β − 2 chainTopCoeff α β, приведённому в основание поля.
LaTeX
$$$\beta(\mathrm{coroot}(\alpha)) = \uparrow\big(\mathrm{chainLength}(\alpha, \beta) - 2 \cdot \mathrm{chainTopCoeff}(\alpha, \beta) : \mathbb{Z}\big)$$$
Lean4
theorem apply_coroot_eq_cast' : β (coroot α) = ↑(chainLength α β - 2 * chainTopCoeff α β : ℤ) :=
by
by_cases hα : α.IsZero
·
rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero, CharP.cast_eq_zero,
mul_zero, sub_self, Int.cast_zero]
obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero
have := chainLength_smul _ _ hx
rw [lie_eq_smul_of_mem_rootSpace hx, ← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left x_ne0, sub_eq_zero,
coe_chainTop', nsmul_eq_mul, Pi.natCast_def, Pi.add_apply, Pi.mul_apply, root_apply_coroot hα] at this
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_mul, Int.cast_ofNat, eq_sub_iff_add_eq', this, mul_comm (2 : K)]
