mathlib3 documentation

ring_theory.finite_presentation

Finiteness conditions in commutative algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

source
def algebra.finite_presentation (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] :
Prop

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

Equations
source
theorem algebra.finite_type.of_finite_presentation {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
algebra.finite_presentation R A → algebra.finite_type R A

A finitely presented algebra is of finite type.

source
theorem algebra.finite_presentation.of_finite_type {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] [is_noetherian_ring R] :
algebra.finite_type R A ↔ algebra.finite_presentation R A

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

source
theorem algebra.finite_presentation.equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] (hfp : algebra.finite_presentation R A) (e : A ≃ₐ[R] B) :
algebra.finite_presentation R B

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

source
@[protected]
theorem algebra.finite_presentation.mv_polynomial (R : Type u_1) [comm_ring R] (ι : Type u_2) [finite ι] :
algebra.finite_presentation R (mv_polynomial ι R)

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

source
theorem algebra.finite_presentation.self (R : Type u_1) [comm_ring R] :
algebra.finite_presentation R R

R is finitely presented as R-algebra.

source
theorem algebra.finite_presentation.polynomial (R : Type u_1) [comm_ring R] :
algebra.finite_presentation R (polynomial R)

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

source
@[protected]
theorem algebra.finite_presentation.quotient {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {I : ideal A} (h : I.fg) (hfp : algebra.finite_presentation R A) :
algebra.finite_presentation R (A ⧸ I)

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

source
theorem algebra.finite_presentation.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] {f : A →ₐ[R] B} (hf : function.surjective ⇑f) (hker : (ring_hom.ker f.to_ring_hom).fg) (hfp : algebra.finite_presentation R A) :
algebra.finite_presentation R B

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

source
theorem algebra.finite_presentation.iff {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
algebra.finite_presentation R A ↔ ∃ (n : ℕ) (I : ideal (mv_polynomial (fin n) R)) (e : (mv_polynomial (fin n) R ⧸ I) ≃ₐ[R] A), I.fg
source
theorem algebra.finite_presentation.iff_quotient_mv_polynomial' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
algebra.finite_presentation R A ↔ ∃ (ι : Type u_2) (_x : fintype ι) (f : mv_polynomial ι R →ₐ[R] A), function.surjective ⇑f ∧ (ring_hom.ker f.to_ring_hom).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.

source
theorem algebra.finite_presentation.mv_polynomial_of_finite_presentation {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (hfp : algebra.finite_presentation R A) (ι : Type u_3) [finite ι] :
algebra.finite_presentation R (mv_polynomial ι A)

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

source
theorem algebra.finite_presentation.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (hfpA : algebra.finite_presentation R A) (hfpB : algebra.finite_presentation A B) :
algebra.finite_presentation 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.

source
theorem algebra.finite_presentation.of_restrict_scalars_finite_presentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (hRB : algebra.finite_presentation R B) [hRA : algebra.finite_type R A] :
algebra.finite_presentation A B
source
theorem algebra.finite_presentation.ker_fg_of_mv_polynomial {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {n : ℕ} (f : mv_polynomial (fin n) R →ₐ[R] A) (hf : function.surjective ⇑f) (hfp : algebra.finite_presentation R A) :
(ring_hom.ker f.to_ring_hom).fg

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

source
theorem algebra.finite_presentation.ker_fg_of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] (f : A →ₐ[R] B) (hf : function.surjective ⇑f) (hRA : algebra.finite_presentation R A) (hRB : algebra.finite_presentation R B) :
(ring_hom.ker f.to_ring_hom).fg

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

source
def ring_hom.finite_presentation {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) :
Prop

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

Equations
source
theorem ring_hom.finite_type.of_finite_presentation {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite_presentation) :
f.finite_type
source
theorem ring_hom.finite_presentation.id (A : Type u_1) [comm_ring A] :
(ring_hom.id A).finite_presentation
source
theorem ring_hom.finite_presentation.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (hf : f.finite_presentation) (hg : function.surjective ⇑g) (hker : (ring_hom.ker g).fg) :
(g.comp f).finite_presentation
source
theorem ring_hom.finite_presentation.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective ⇑f) (hker : (ring_hom.ker f).fg) :
f.finite_presentation
source
theorem ring_hom.finite_presentation.of_finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_noetherian_ring A] {f : A →+* B} :
f.finite_type ↔ f.finite_presentation
source
theorem ring_hom.finite_presentation.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {g : B →+* C} {f : A →+* B} (hg : g.finite_presentation) (hf : f.finite_presentation) :
(g.comp f).finite_presentation
source
theorem ring_hom.finite_presentation.of_comp_finite_type {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) {g : B →+* C} (hg : (g.comp f).finite_presentation) (hf : f.finite_type) :
g.finite_presentation
source
def alg_hom.finite_presentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
Prop

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

Equations
source
theorem alg_hom.finite_type.of_finite_presentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] {f : A →ₐ[R] B} (hf : f.finite_presentation) :
f.finite_type
source
theorem alg_hom.finite_presentation.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :
(alg_hom.id R A).finite_presentation
source
theorem alg_hom.finite_presentation.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [algebra R A] [algebra R B] [algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite_presentation) (hf : f.finite_presentation) :
(g.comp f).finite_presentation
source
theorem alg_hom.finite_presentation.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [algebra R A] [algebra R B] [algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.finite_presentation) (hg : function.surjective ⇑g) (hker : (ring_hom.ker g.to_ring_hom).fg) :
(g.comp f).finite_presentation
source
theorem alg_hom.finite_presentation.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : function.surjective ⇑f) (hker : (ring_hom.ker f.to_ring_hom).fg) :
f.finite_presentation
source
theorem alg_hom.finite_presentation.of_finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [is_noetherian_ring A] {f : A →ₐ[R] B} :
f.finite_type ↔ f.finite_presentation
source
theorem alg_hom.finite_presentation.of_comp_finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) {g : B →ₐ[R] C} (h : (g.comp f).finite_presentation) (h' : f.finite_type) :
g.finite_presentation