finitePresentation_of_ker — Mathlib

English

If N has a finite presentation and l: M → N is surjective, then M has a finite presentation.

Русский

Если N имеет конечное представление и l: M → N сюръективна, то M имеет конечное представление.

LaTeX

$$$[Module.FinitePresentation R N](l : M \to N) (hl : Function.Surjective l) : Module.FinitePresentation R M$$$

Lean4

theorem finitePresentation_of_ker [Module.FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective l)
    [Module.FinitePresentation R (LinearMap.ker l)] : Module.FinitePresentation R M :=
  by
  obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG :=
    by
    apply Submodule.fg_of_fg_map_of_fg_inf_ker l
    · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.fg_top
    · rw [top_inf_eq, ← Submodule.fg_top]; exact Module.Finite.fg_top
  refine ⟨s, hs, ?_⟩
  let π := Finsupp.linearCombination R ((↑) : s → M)
  have H : Function.Surjective π :=
    LinearMap.range_eq_top.mp (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
  have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) :=
    by
    constructor
    rw [Submodule.fg_top]; exact Module.FinitePresentation.fg_ker _ (hl.comp H)
  let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)
  have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl
  have hf : Function.Surjective f := by
    rw [← LinearMap.range_eq_top]
    apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
    rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e, LinearMap.range_comp,
      Submodule.range_subtype, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective H]
  change (LinearMap.ker π).FG
  have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) := Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))
  rw [← inf_eq_right.mpr this, ← Submodule.range_subtype (LinearMap.ker _), ← Submodule.map_comap_eq, ←
    LinearMap.ker_comp, e, LinearMap.ker_comp f,
    LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype (LinearMap.ker l)), Submodule.comap_bot]
  exact (Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)

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