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.

class 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.

• out : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

instance Algebra.FiniteType.of_finitePresentation {R : Type w₁} {A : Type w₂} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : 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] : FiniteType R A ↔ 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] [FinitePresentation R A] (e : A ≃ₐ[R] B) : FinitePresentation R B

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

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

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

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

R is finitely presented as R-algebra.

instance Algebra.FinitePresentation.polynomial (R : Type w₁) [CommRing R] : 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 : I.FG) [FinitePresentation R A] : 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 : (RingHom.ker f.toRingHom).FG) [FinitePresentation R A] : 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] : FinitePresentation R A ↔ ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG

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

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] [FinitePresentation R A] (ι : Type v) [Finite ι] : 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] [FinitePresentation R A] [FinitePresentation A B] : 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] [FinitePresentation R B] [FiniteType R A] : 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) [FinitePresentation R A] : (RingHom.ker f.toRingHom).FG

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) [FinitePresentation R A] [FinitePresentation R B] : (RingHom.ker f.toRingHom).FG

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

• f.FinitePresentation = 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 : f.FinitePresentation) : f.FiniteType

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

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 : f.FinitePresentation) (hg : Function.Surjective ⇑g) (hker : (ker g).FG) : (g.comp f).FinitePresentation

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 : (ker f).FG) : f.FinitePresentation

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

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 : g.FinitePresentation) (hf : f.FinitePresentation) : (g.comp f).FinitePresentation

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 : (g.comp f).FinitePresentation) (hf : f.FiniteType) : g.FinitePresentation

theorem RingHom.FinitePresentation.polynomial_induction (P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop) (Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop) (polynomial : ∀ (R : Type u) [inst : CommRing R], P R (Polynomial R) Polynomial.C) (fg_ker : ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S), Function.Surjective ⇑f → (ker f).FG → Q R S f) (comp : ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)) {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.FinitePresentation) : Q R S f

Induction principle for finitely presented ring homomorphisms.

For a property to hold for all finitely presented ring homs, it suffices for it to hold for Polynomial.C : R → R[X], surjective ring homs with finitely generated kernels, and to be closed under composition.

Note that to state this conveniently for ring homs between rings of different universes, we carry around two predicates P and Q, which should be "the same" apart from universes:

• P, for ring homs (R : Type u) → (S : Type u).
• Q, for ring homs (R : Type u) → (S : Type v).

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

• f.FinitePresentation = f.FinitePresentation

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 : f.FinitePresentation) : f.FiniteType

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

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 : g.FinitePresentation) (hf : f.FinitePresentation) : (g.comp f).FinitePresentation

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 : f.FinitePresentation) (hg : Function.Surjective ⇑g) (hker : (RingHom.ker g.toRingHom).FG) : (g.comp f).FinitePresentation

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 : (RingHom.ker f.toRingHom).FG) : f.FinitePresentation

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} : f.FiniteType ↔ f.FinitePresentation

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 : (g.comp f).FinitePresentation) (h' : f.FiniteType) : g.FinitePresentation