English
The orthogonal complement of the root span with respect to RootForm equals the kernel of RootForm.
Русский
Ортогональное дополнение к корневому Span относительно RootForm равно ядру RootForm.
LaTeX
$$P.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm$$
Lean4
@[simp]
theorem orthogonal_rootSpan_eq : P.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm :=
by
rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]
refine le_antisymm ?_ (by intro; simp_all)
rintro x hx y -
simp only [LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.IsOrtho] at hx ⊢
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan R) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top
simp only [LinearMap.mem_ker] at hv
simp [hx _ hu, hv]
