Finite projective presentations

A finite projective presentation of a module is a right exact diagram P₁ → P₀ → M → 0 with both P₀ and P₁ finitely generated projective. Every finitely presented module admits such a diagram, even over a non-Noetherian ring. Keeping the diagram explicit allows constructions such as the Auslander–Bridger transpose to compare different choices of presentation.

References

• M. Auslander, M. Bridger, Stable module theory, Section 2.1.

structure TauCeti.FiniteProjectivePresentation {A : Type u} [Ring A] (M : ModuleCat A) : Type (max u (v + 1))

A right exact presentation by two finitely generated projective modules.

• P₀ : ModuleCat A

  The module of generators.

• P₁ : ModuleCat A

  The module of relations.

• finite₀ : Module.Finite A ↑self.P₀

  The generators form a finite module.

• finite₁ : Module.Finite A ↑self.P₁

  The relations form a finite module.

• projective₀ : Module.Projective A ↑self.P₀

  The generators form a projective module.

• projective₁ : Module.Projective A ↑self.P₁

  The relations form a projective module.

• p : ↑self.P₁ →ₗ[A] ↑self.P₀

  The presenting map.

• π : ↑self.P₀ →ₗ[A] ↑M

  The augmentation to the presented module.

• exact : Function.Exact ⇑self.p ⇑self.π

  The relations are exactly the kernel of the augmentation.

• surjective : Function.Surjective ⇑self.π

  The generators cover the module.

noncomputable def TauCeti.FiniteProjectivePresentation.ofFinitePresentation {A : Type u} [Ring A] {M : ModuleCat A} [Module.FinitePresentation A ↑M] [Small.{v, u} A] : FiniteProjectivePresentation M

Every finitely presented module has a finite projective presentation. The ring need only be small in the universe of the module.

Equations

• TauCeti.FiniteProjectivePresentation.ofFinitePresentation = Classical.choice ⋯