Commit 2024-11-13 17:52 1f162e90

feat(Algebra/Module): presentation of the cokernel of a linear map (#18332) If f : M₁ →ₗ[A] M₂ is a linear map between modules, pres₂ is a presentation of M₂ and g₁ : ι → M₁ is a family of generators of M₁ (which is expressed as hg₁ : Submodule.span A (Set.range g₁) = ⊤), then we provide a way to obtain a presentation of the cokernel of f. It requires an additional data data : pres₂.CokernelData f g₁, which consists of liftings of the images by f of the generators of M₁ as linear combinations of the generators of M₂. Then, we obtain a presentation pres₂.cokernel data hg₁ : Presentation A (M₂ ⧸ LinearMap.range f).