English
The cokernel solution itself is a presentation, i.e. defines an isomorphism between the cokernel relations and the target module.
Русский
Коконеленное решение образует презентацию, задавая изоморфизм между коконеленными отношениями и целевым модулем.
LaTeX
$$$\\text{cokernelSolution.isPresentation}: (pres_2.\\text{cokernelSolution data}).IsPresentation$$$
Lean4
/-- The cokernel can be defined by generators and relations. -/
noncomputable def isPresentationCore : Relations.Solution.IsPresentationCore.{w} (pres₂.cokernelSolution data)
where
desc
s :=
(LinearMap.range f).liftQ
(pres₂.desc
{ var := s.var
linearCombination_var_relation := fun r ↦ s.linearCombination_var_relation (.inl r) })
(by
rw [LinearMap.range_eq_map, ← hg₁, Submodule.map_span, Submodule.span_le, Set.image_subset_iff]
rintro _ ⟨i, rfl⟩
rw [Set.mem_preimage, SetLike.mem_coe, LinearMap.mem_ker, ← data.π_lift,
Relations.Solution.IsPresentation.π_desc_apply]
exact s.linearCombination_var_relation (.inr i))
postcomp_desc s := by aesop
postcomp_injective
h := by
ext : 1
apply pres₂.toIsPresentation.postcomp_injective
ext g
exact Relations.Solution.congr_var h g
