English
A solution is a presentation precisely when the submodule generated by the image of the generators is the whole module and the kernel of the projection equals the submodule generated by the relations.
Русский
Презентацией является решение тогда и только тогда, когда порожденная образами генераторов подмодуль равен всему модулю, и ядро отображения совпадает с подмодулем, порожденным отношениями.
LaTeX
$$$\\text{solution.IsPresentation} \\iff \\left( \\operatorname{span}_A(\\operatorname{range}\\text{solution.var}) = \\top \\right) \\land \\left( \\ker \\text{solution.π} = \\operatorname{span}_A(\\operatorname{range} \\text{relations.relation}) \\right).$$$
Lean4
theorem isPresentation_iff :
solution.IsPresentation ↔
Submodule.span A (Set.range solution.var) = ⊤ ∧
LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation) :=
by
rw [← injective_fromQuotient_iff_ker_π_eq_span, ← surjective_π_iff_span_eq_top, ←
surjective_fromQuotient_iff_surjective_π, ]
exact ⟨fun h ↦ ⟨h.bijective.2, h.bijective.1⟩, fun h ↦ ⟨⟨h.2, h.1⟩⟩⟩
