English
The trace form’s orthogonal of coroot α equals the weight kernel α.ker.
Русский
Ортогональное к короту α по traceForm равноker α.
LaTeX
$$(traceForm K H L).orthogonal (K ∙ coroot α) = α.ker$$
Lean4
@[simp]
theorem orthogonal_span_coroot_eq_ker (α : Weight K H L) : (traceForm K H L).orthogonal (K ∙ coroot α) = α.ker := by
if hα : α.IsZero then
have hα' : coroot α = 0 := by simpa
replace hα : α.ker = ⊤ := by ext; simp [hα]
simp [hα, hα']
else
refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
· simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat,
mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)
· have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy
rwa [traceForm_comm] at this
