Finiteness conditions in commutative algebra

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

Main declarations

module.finite, algebra.finite, ring_hom.finite, alg_hom.finite all of these express that some object is finitely generated as module over some base ring.
algebra.finite_type, ring_hom.finite_type, alg_hom.finite_type all of these express that some object is finitely generated as algebra over some base ring.

source

@[class]

def module.finite (R : Type u_1) (M : Type u_4) [comm_ring R] [add_comm_group M] [module R M] :

Prop

A module over a commutative ring is finite if it is finitely generated as a module.

Equations

module.finite R M = ⊤.fg

Instances

source

@[class]

def algebra.finite_type (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

Prop

An algebra over a commutative ring is of finite_type if it is finitely generated over the base ring as algebra.

Equations

algebra.finite_type R A = ⊤.fg

Instances

module.finite.finite_type

source

theorem module.finite_def {R : Type u_1} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] :

module.finite R M ↔ ⊤.fg

source

@[instance]

def module.is_noetherian.finite (R : Type u_1) (M : Type u_4) [comm_ring R] [add_comm_group M] [module R M] [is_noetherian R M] :

module.finite R M

source

theorem module.finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [hM : module.finite R M] (f : M →ₗ[R] N) (hf : function.surjective ⇑f) :

module.finite R N

source

theorem module.finite.of_injective {R : Type u_1} {M : Type u_4} {N : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [is_noetherian R N] (f : M →ₗ[R] N) (hf : function.injective ⇑f) :

module.finite R M

source

@[instance]

def module.finite.self (R : Type u_1) [comm_ring R] :

module.finite R R

source

@[instance]

def module.finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [hM : module.finite R M] [hN : module.finite R N] :

module.finite R (M × N)

source

theorem module.finite.equiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [hM : module.finite R M] (e : M ≃ₗ[R] N) :

module.finite R N

source

theorem module.finite.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] [hRA : module.finite R A] [hAB : module.finite A B] :

module.finite R B

source

@[instance]

def module.finite.finite_type {R : Type u_1} (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] [hRA : module.finite R A] :

algebra.finite_type R A

source

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

algebra.finite_type R R

source

theorem algebra.finite_type.mv_polynomial (R : Type u_1) [comm_ring R] (ι : Type u_2) [fintype ι] :

algebra.finite_type R (mv_polynomial ι R)

source

theorem algebra.finite_type.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] (hRA : algebra.finite_type R A) (f : A →ₐ[R] B) (hf : function.surjective ⇑f) :

algebra.finite_type R B

source

theorem algebra.finite_type.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] (hRA : algebra.finite_type R A) (e : A ≃ₐ[R] B) :

algebra.finite_type R B

source

theorem algebra.finite_type.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] (hRA : algebra.finite_type R A) (hAB : algebra.finite_type A B) :

algebra.finite_type R B

source

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

Prop

A ring morphism A →+* B is finite if B is finitely generated as A-module.

Equations

f.finite = let _inst : algebra A B := f.to_algebra in module.finite A B

source

def ring_hom.finite_type {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_type if B is finitely generated as A-algebra.

Equations

f.finite_type = algebra.finite_type A B

source

theorem ring_hom.finite.id (A : Type u_1) [comm_ring A] :

(ring_hom.id A).finite

source

theorem ring_hom.finite.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective ⇑f) :

f.finite

source

theorem ring_hom.finite.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) (hf : f.finite) :

(g.comp f).finite

source

theorem ring_hom.finite.finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite) :

f.finite_type

source

theorem ring_hom.finite_type.id (A : Type u_1) [comm_ring A] :

(ring_hom.id A).finite_type

source

theorem ring_hom.finite_type.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_type) (hg : function.surjective ⇑g) :

(g.comp f).finite_type

source

theorem ring_hom.finite_type.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective ⇑f) :

f.finite_type

source

theorem ring_hom.finite_type.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_type) (hf : f.finite_type) :

(g.comp f).finite_type

source

def alg_hom.finite {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 finite if it is finite as ring morphism. In other words, if B is finitely generated as A-module.

Equations

f.finite = f.to_ring_hom.finite

source

def alg_hom.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] (f : A →ₐ[R] B) :

Prop

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

Equations

f.finite_type = f.to_ring_hom.finite_type

source

theorem alg_hom.finite.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

(alg_hom.id R A).finite

source

theorem alg_hom.finite.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) (hf : f.finite) :

(g.comp f).finite

source

theorem alg_hom.finite.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) :

f.finite

source

theorem alg_hom.finite.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] {f : A →ₐ[R] B} (hf : f.finite) :

f.finite_type

source

theorem alg_hom.finite_type.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

(alg_hom.id R A).finite_type

source

theorem alg_hom.finite_type.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_type) (hf : f.finite_type) :

(g.comp f).finite_type

source

theorem alg_hom.finite_type.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_type) (hg : function.surjective ⇑g) :

(g.comp f).finite_type

source

theorem alg_hom.finite_type.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) :

f.finite_type