Finitely presented algebras and finitely presented modules

In this file we establish relations between finitely presented as an algebra and finitely presented as a module.

Main results:

• Algebra.FinitePresentation.of_finitePresentation: If S is finitely presented as a module over R, then it is finitely presented as an algebra over R.
• Module.FinitePresentation.of_finite_of_finitePresentation: If S is finite as a module over R and finitely presented as an algebra over R, then it is finitely presented as a module over R.

References

• Grothendieck, EGA IV₁ 1.4.7

theorem Module.Finite.exists_free_surjective (R : Type u) (S : Type u_1) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] : ∃ (S' : Type u) (x : CommRing S') (x_1 : Algebra R S') (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S') (f : S' →ₐ[R] S), Function.Surjective ⇑f

EGA IV₁, 1.4.7.1

instance Algebra.FinitePresentation.of_finitePresentation (R : Type u) (S : Type u_1) [CommRing R] [CommRing S] [Algebra R S] [Module.FinitePresentation R S] : FinitePresentation R S

If S is finitely presented as a module over R, it is finitely presented as an algebra over R.

theorem Module.FinitePresentation.of_finite_of_finitePresentation (R : Type u) (S : Type u_1) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Algebra.FinitePresentation R S] : FinitePresentation R S

If S is finite as a module over R and finitely presented as an algebra over R, then it is finitely presented as a module over R.

theorem Module.FinitePresentation.iff_finitePresentation_of_finite (R : Type u) (S : Type u_1) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] : FinitePresentation R S ↔ Algebra.FinitePresentation R S

If S is a finite R-algebra, finitely presented as a module and as an algebra is equivalent.