English
The kernel of CorootForm is the image, under the flip map, of the dual annihilator of the root span.
Русский
Ядро CorootForm — образ двойного аннигилирующего подпространства корневого Span через отображение разворота.
LaTeX
$$\\ker P.CorootForm = (P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm$$
Lean4
theorem ker_rootForm_eq_dualAnnihilator :
LinearMap.ker P.RootForm = (P.corootSpan R).dualAnnihilator.map P.toPerfPair.symm :=
by
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
suffices finrank R (LinearMap.ker P.RootForm) = finrank R (P.corootSpan R).dualAnnihilator
by
refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm
rw [this]
apply LinearEquiv.finrank_map_eq
have aux0 := Subspace.finrank_add_finrank_dualAnnihilator_eq (P.corootSpan R)
have aux1 := Submodule.finrank_add_eq_of_isCompl P.isCompl_rootSpan_ker_rootForm
rw [← P.finrank_corootSpan_eq', P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq] at aux1
omega
