Finiteness conditions in commutative algebra

In this file we define several notions of finiteness that are common in commutative algebra.

Main declarations

• Module.Finite, RingHom.Finite, AlgHom.Finite all of these express that some object is finitely generated as module over some base ring.
• Algebra.FiniteType, RingHom.FiniteType, AlgHom.FiniteType all of these express that some object is finitely generated as algebra over some base ring.
• Algebra.FinitePresentation, RingHom.FinitePresentation, AlgHom.FinitePresentation all of these express that some object is finitely presented as algebra over some base ring.

def Algebra.FinitePresentation (R : Type w₁) (A : Type w₂) [CommSemiring R] [Semiring A] [Algebra R A] : Prop

An algebra over a commutative semiring is Algebra.FinitePresentation if it is the quotient of a polynomial ring in n variables by a finitely generated ideal.

Equations

• Algebra.FinitePresentation R A = ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective ⇑f ∧ Ideal.FG (RingHom.ker ↑f)

theorem Algebra.FiniteType.of_finitePresentation {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] : Algebra.FinitePresentation R A → Algebra.FiniteType R A

A finitely presented algebra is of finite type.

theorem Algebra.FinitePresentation.of_finiteType {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] : Algebra.FiniteType R A ↔ Algebra.FinitePresentation R A

An algebra over a Noetherian ring is finitely generated if and only if it is finitely presented.

theorem Algebra.FinitePresentation.equiv {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (hfp : Algebra.FinitePresentation R A) (e : A ≃ₐ[R] B) : Algebra.FinitePresentation R B

If e : A ≃ₐ[R] B and A is finitely presented, then so is B.

theorem Algebra.FinitePresentation.mvPolynomial (R : Type w₁) [CommRing R] (ι : Type u_2) [Finite ι] : Algebra.FinitePresentation R (MvPolynomial ι R)

The ring of polynomials in finitely many variables is finitely presented.

theorem Algebra.FinitePresentation.self (R : Type w₁) [CommRing R] : Algebra.FinitePresentation R R

R is finitely presented as R-algebra.

theorem Algebra.FinitePresentation.polynomial (R : Type w₁) [CommRing R] : Algebra.FinitePresentation R (Polynomial R)

R[X] is finitely presented as R-algebra.

theorem Algebra.FinitePresentation.quotient {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} (h : Ideal.FG I) (hfp : Algebra.FinitePresentation R A) : Algebra.FinitePresentation R (A ⧸ I)

The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.

theorem Algebra.FinitePresentation.of_surjective {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Surjective ⇑f) (hker : Ideal.FG (RingHom.ker ↑f)) (hfp : Algebra.FinitePresentation R A) : Algebra.FinitePresentation R B

If f : A →ₐ[R] B is surjective with finitely generated kernel and A is finitely presented, then so is B.

theorem Algebra.FinitePresentation.iff {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] : Algebra.FinitePresentation R A ↔ ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), Ideal.FG I

theorem Algebra.FinitePresentation.iff_quotient_mvPolynomial' {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] : Algebra.FinitePresentation R A ↔ ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A), Function.Surjective ⇑f ∧ Ideal.FG (RingHom.ker ↑f)

An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype by a finitely generated ideal.

theorem Algebra.FinitePresentation.mvPolynomial_of_finitePresentation {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] (hfp : Algebra.FinitePresentation R A) (ι : Type v) [Finite ι] : Algebra.FinitePresentation R (MvPolynomial ι A)

If A is a finitely presented R-algebra, then MvPolynomial (Fin n) A is finitely presented as R-algebra.

theorem Algebra.FinitePresentation.trans {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hfpA : Algebra.FinitePresentation R A) (hfpB : Algebra.FinitePresentation A B) : Algebra.FinitePresentation R B

If A is an R-algebra and S is an A-algebra, both finitely presented, then S is finitely presented as R-algebra.

theorem Algebra.FinitePresentation.of_restrict_scalars_finitePresentation {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hRB : Algebra.FinitePresentation R B) [hRA : Algebra.FiniteType R A] : Algebra.FinitePresentation A B

theorem Algebra.FinitePresentation.ker_fg_of_mvPolynomial {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] {n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] A) (hf : Function.Surjective ⇑f) (hfp : Algebra.FinitePresentation R A) : Ideal.FG (RingHom.ker ↑f)

This is used to prove the strictly stronger ker_fg_of_surjective. Use it instead.

theorem Algebra.FinitePresentation.ker_fG_of_surjective {R : Type w₁} {A : Type w₂} {B : Type w₃} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) (hRA : Algebra.FinitePresentation R A) (hRB : Algebra.FinitePresentation R B) : Ideal.FG (RingHom.ker ↑f)

If f : A →ₐ[R] B is a surjection between finitely-presented R-algebras, then the kernel of f is finitely generated.

def RingHom.FinitePresentation {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) : Prop

A ring morphism A →+* B is of RingHom.FinitePresentation if B is finitely presented as A-algebra.

Equations

• RingHom.FinitePresentation f = Algebra.FinitePresentation A B

theorem RingHom.FiniteType.of_finitePresentation {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.FinitePresentation f) : RingHom.FiniteType f

theorem RingHom.FinitePresentation.id (A : Type u_1) [CommRing A] : RingHom.FinitePresentation (RingHom.id A)

theorem RingHom.FinitePresentation.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (hf : RingHom.FinitePresentation f) (hg : Function.Surjective ⇑g) (hker : Ideal.FG (RingHom.ker g)) : RingHom.FinitePresentation (RingHom.comp g f)

theorem RingHom.FinitePresentation.of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : Function.Surjective ⇑f) (hker : Ideal.FG (RingHom.ker f)) : RingHom.FinitePresentation f

theorem RingHom.FinitePresentation.of_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsNoetherianRing A] {f : A →+* B} : RingHom.FiniteType f ↔ RingHom.FinitePresentation f

theorem RingHom.FinitePresentation.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {g : B →+* C} {f : A →+* B} (hg : RingHom.FinitePresentation g) (hf : RingHom.FinitePresentation f) : RingHom.FinitePresentation (RingHom.comp g f)

theorem RingHom.FinitePresentation.of_comp_finiteType {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] (f : A →+* B) {g : B →+* C} (hg : RingHom.FinitePresentation (RingHom.comp g f)) (hf : RingHom.FiniteType f) : RingHom.FinitePresentation g

def AlgHom.FinitePresentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : Prop

An algebra morphism A →ₐ[R] B is of AlgHom.FinitePresentation if it is of finite presentation as ring morphism. In other words, if B is finitely presented as A-algebra.

Equations

• AlgHom.FinitePresentation f = RingHom.FinitePresentation ↑f

theorem AlgHom.FiniteType.of_finitePresentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {f : A →ₐ[R] B} (hf : AlgHom.FinitePresentation f) : AlgHom.FiniteType f

theorem AlgHom.FinitePresentation.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] : AlgHom.FinitePresentation (AlgHom.id R A)

theorem AlgHom.FinitePresentation.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : AlgHom.FinitePresentation g) (hf : AlgHom.FinitePresentation f) : AlgHom.FinitePresentation (AlgHom.comp g f)

theorem AlgHom.FinitePresentation.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : AlgHom.FinitePresentation f) (hg : Function.Surjective ⇑g) (hker : Ideal.FG (RingHom.ker ↑g)) : AlgHom.FinitePresentation (AlgHom.comp g f)

theorem AlgHom.FinitePresentation.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) (hker : Ideal.FG (RingHom.ker ↑f)) : AlgHom.FinitePresentation f

theorem AlgHom.FinitePresentation.of_finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [IsNoetherianRing A] {f : A →ₐ[R] B} : AlgHom.FiniteType f ↔ AlgHom.FinitePresentation f

theorem AlgHom.FinitePresentation.of_comp_finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) {g : B →ₐ[R] C} (h : AlgHom.FinitePresentation (AlgHom.comp g f)) (h' : AlgHom.FiniteType f) : AlgHom.FinitePresentation g