fg_ker_iff — Mathlib

English

For a surjective linear map l: M → N, and M finitely presented, ker(l) FG iff N finitely presented.

Русский

При сюръективном линейном отображении l: M → N и M конечнопредставимом, Ker(l) FG ↔ N конечнопредставим.

LaTeX

$$$[Module.FinitePresentation R M] (l : M \to N) (hl : Function.Surjective l) : Submodule.FG (LinearMap.ker l) \iff Module.FinitePresentation R N$$$

Lean4

theorem fg_ker_iff [Module.FinitePresentation R M] (l : M →ₗ[R] N) (hl : Function.Surjective l) :
    Submodule.FG (LinearMap.ker l) ↔ Module.FinitePresentation R N :=
  ⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩

Похожие утверждения