English
The root span and the kernel of RootForm form a complementary direct sum inside the ambient space.
Русский
Корневое пространство и ядро RootForm образуют дополнение в прямой сумме внутри окружающего пространства.
LaTeX
$$(P.rootSpan R) \\oplus Ker(P.RootForm) = M$$
Lean4
theorem isCompl_rootSpan_ker_rootForm : IsCompl (P.rootSpan R) (LinearMap.ker P.RootForm) :=
by
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
refine (Submodule.isCompl_iff_disjoint _ _ ?_).mpr P.disjoint_rootSpan_ker_rootForm
have aux : finrank R M = finrank R (P.rootSpan R) + finrank R (P.corootSpan R).dualAnnihilator := by
rw [P.toPerfPair.finrank_eq, ← P.finrank_corootSpan_eq',
Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R), Subspace.dual_finrank_eq]
rw [aux, add_le_add_iff_left]
convert Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm
exact (LinearEquiv.finrank_map_eq _ _).symm
