English
The cokernel of a linear map f: M1 → M2 with respect to a presentation pres₂ of M₂ is presented by transporting data along the section to obtain M₂ / range f.
Русский
Коконелен модуля 1-го типа от линейного отображения f: M1 → M2 с презентацией pres₂ модуля M₂ задаётся переносом данных через секцию на M₂ / range f.
LaTeX
$$$pres_2\\!:\\text{cokernel}(f,g_1) : \\text{Presentation}_A (M_2 / \\mathrm{range}(f))$$$
Lean4
/-- The presentation of the cokernel of a linear map `f : M₁ →ₗ[A] M₂` that is obtained
from a presentation `pres₂` of `M₂`, a choice of generators `g₁ : ι → M₁` of `M₁`,
and an additional data in `pres₂.CokernelData f g₁`. -/
@[simps!]
def cokernel : Presentation A (M₂ ⧸ LinearMap.range f) :=
ofIsPresentation (cokernelSolution.isPresentation pres₂ data hg₁)
