finitePresentation_iff_exists_presentation

English

Two-way equivalence: a module has a finite presentation iff there exists a presentation with finite G and finite R.

Русский

Эквивалентность в обе стороны: модуль имеет конечную презентацию тогда и только тогда существует презентация с конечными G и R.

LaTeX

$$$Module.FinitePresentation\\ A M \\; \\iff \\; \\exists pres, Finite pres.G ∧ Finite pres.R$$$

Lean4

theorem finitePresentation_iff_exists_presentation :
    Module.FinitePresentation A M ↔ ∃ (pres : Presentation.{w₀, w₁} A M), Finite pres.G ∧ Finite pres.R :=
  by
  constructor
  · intro
    obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1 (finite_def.1 (inferInstanceAs (Module.Finite A M)))
    obtain ⟨R : Type w₁, _, relation, hR⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var)
          (by rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))
    exact
      ⟨{  G := G
          R := R
          relation := relation
          var := var
          linearCombination_var_relation := fun r ↦
            by
            rw [Submodule.ext_iff] at hR
            exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
          toIsPresentation := by
            rw [Relations.Solution.isPresentation_iff]
            exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩
  · rintro ⟨pres, _, _⟩
    exact pres.finitePresentation

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