English
Given an exact sequence M1 → M2 → M3 → 0 and a presentation pres₂ of M₂ with data, one obtains a presentation of M₃ via transporting along the exact sequence map.
Русский
При данной точной последовательности модулей M₁ → M₂ → M₃ → 0 и презентации pres₂ модуля M₂ с данными, получаем презентацию M₃ через перенос по линейному отображению на последовательности.
LaTeX
$$$\\text{ofExact} : \\text{Presentation } A M_3$ given $f,g, pres_2, hfg, hg, hg_1$$$
Lean4
/-- Given an exact sequence of `A`-modules `M₁ → M₂ → M₃ → 0`, this is the presentation
of `M₃` that is obtained from a presentation `pres₂` of `M₂`, a choice of generators
`g₁ : ι → M₁` of `M₁`, and an additional data in a `Presentation.CokernelData` structure. -/
@[simps!]
noncomputable def ofExact {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Presentation.{w₂₀, w₂₁} A M₂) {ι : Type w₁}
{g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact f g) (hg : Function.Surjective g)
(hg₁ : Submodule.span A (Set.range g₁) = ⊤) : Presentation A M₃ :=
(pres₂.cokernel data hg₁).ofLinearEquiv (hfg.linearEquivOfSurjective hg)
