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 a notion of finiteness that is common in commutative algebra.
Main declarations #
-
submodule.fg,ideal.fgThese express that some object is finitely generated as submodule over some base ring. -
module.finite,ring_hom.finite,alg_hom.finiteall of these express that some object is finitely generated as module over some base ring.
Main results #
exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulis Nakayama's lemma, in the following form: if N is a finitely generated submodule of an ambient R-module M and I is an ideal of R such that N ⊆ IN, then there exists r ∈ 1 + I such that rN = 0.
theorem
submodule.fg_iff_add_submonoid_fg
{M : Type u_2}
[add_comm_monoid M]
(P : submodule ℕ M) :
P.fg ↔ P.to_add_submonoid.fg
theorem
submodule.fg_iff_add_subgroup_fg
{G : Type u_1}
[add_comm_group G]
(P : submodule ℤ G) :
P.fg ↔ P.to_add_subgroup.fg
theorem
submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(I : ideal R)
(N : submodule R M)
(hn : N.fg)
(hin : N ≤ I • N) :
Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV
theorem
submodule.fg_bot
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
subalgebra.fg_bot_to_submodule
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A] :
theorem
submodule.fg_of_is_unit
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
{I : submodule R A}
(hI : is_unit I) :
I.fg
theorem
submodule.fg_span
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M}
(hs : s.finite) :
(submodule.span R s).fg
theorem
submodule.fg_span_singleton
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
(submodule.span R {x}).fg
theorem
submodule.fg.map
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{P : Type u_3}
[add_comm_monoid P]
[module R P]
(f : M →ₗ[R] P)
{N : submodule R M}
(hs : N.fg) :
(submodule.map f N).fg
theorem
submodule.fg_of_fg_map_injective
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
{P : Type u_3}
[add_comm_monoid P]
[module R P]
(f : M →ₗ[R] P)
(hf : function.injective ⇑f)
{N : submodule R M}
(hfn : (submodule.map f N).fg) :
N.fg
theorem
submodule.fg_of_fg_map
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group P]
[module R P]
(f : M →ₗ[R] P)
(hf : linear_map.ker f = ⊥)
{N : submodule R M}
(hfn : (submodule.map f N).fg) :
N.fg
theorem
submodule.fg_of_fg_map_of_fg_inf_ker
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group P]
[module R P]
(f : M →ₗ[R] P)
{s : submodule R M}
(hs1 : (submodule.map f s).fg)
(hs2 : (s ⊓ linear_map.ker f).fg) :
s.fg
If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.
theorem
submodule.fg_ker_comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
[add_comm_group P]
[module R P]
(f : M →ₗ[R] N)
(g : N →ₗ[R] P)
(hf1 : (linear_map.ker f).fg)
(hf2 : (linear_map.ker g).fg)
(hsur : function.surjective ⇑f) :
(linear_map.ker (g.comp f)).fg
The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.
theorem
submodule.fg_restrict_scalars
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
[comm_semiring R]
[semiring S]
[algebra R S]
[add_comm_group M]
[module S M]
[module R M]
[is_scalar_tower R S M]
(N : submodule S M)
(hfin : N.fg)
(h : function.surjective ⇑(algebra_map R S)) :
(submodule.restrict_scalars R N).fg
theorem
submodule.fg_iff_compact
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : submodule R M) :
Finitely generated submodules are precisely compact elements in the submodule lattice.
theorem
submodule.fg.map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
(f : M →ₗ[R] N →ₗ[R] P)
{p : submodule R M}
{q : submodule R N}
(hp : p.fg)
(hq : q.fg) :
(submodule.map₂ f p q).fg
theorem
ideal.fg_ker_comp
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring A]
(f : R →+* S)
(g : S →+* A)
(hf : (ring_hom.ker f).fg)
(hg : (ring_hom.ker g).fg)
(hsur : function.surjective ⇑f) :
(ring_hom.ker (g.comp f)).fg
@[class]
structure
module.finite
(R : Type u_1)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M] :
Prop
A module over a semiring is finite if it is finitely generated as a module.
Instances of this typeclass
- module.is_noetherian.finite
- finite_dimensional.complex_to_real
- module.finite.range
- module.finite.map
- module.finite.self
- module.finite.prod
- module.finite.pi
- module.finite.base_change
- module.finite.tensor_product
- module.finite.matrix
- finite_dimensional.finite_dimensional_pi
- finite_dimensional.finite_dimensional_pi'
- finite_dimensional.finite_dimensional_submodule
- finite_dimensional.finite_dimensional_quotient
- finite_dimensional.finite_dimensional_self
- finite_dimensional.span_singleton
- finite_dimensional.span_finset
- finite_dimensional.submodule.map.finite_dimensional
- finite_dimensional_bot
- submodule.finite_dimensional_inf_left
- submodule.finite_dimensional_inf_right
- submodule.finite_dimensional_sup
- submodule.finite_dimensional_finset_sup
- submodule.finite_dimensional_supr
- finite_dimensional_finsupp
- linear_map.finite_dimensional_range
- finite_dimensional.finite_dimensional_subalgebra
- subalgebra.finite_dimensional_bot
- basis.dual_finite
- subspace.module.dual.finite_dimensional
- module.finite.linear_map
- module.finite.add_monoid_hom
- linear_map.finite_dimensional''
- complex.finite_dimensional
- quaternion_algebra.module.finite
- quaternion.module.finite
theorem
module.finite_def
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
module.finite R M ↔ ⊤.fg
theorem
module.finite.iff_add_monoid_fg
{M : Type u_1}
[add_comm_monoid M] :
module.finite ℕ M ↔ add_monoid.fg M
theorem
module.finite.iff_add_group_fg
{G : Type u_1}
[add_comm_group G] :
module.finite ℤ G ↔ add_group.fg G
theorem
module.finite.exists_fin
{R : Type u_1}
{M : Type u_4}
[semiring R]
[add_comm_monoid M]
[module R M]
[module.finite R M] :
theorem
module.finite.of_surjective
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
[hM : module.finite R M]
(f : M →ₗ[R] N)
(hf : function.surjective ⇑f) :
module.finite R N
@[protected, instance]
def
module.finite.range
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
[module.finite R M]
(f : M →ₗ[R] N) :
The range of a linear map from a finite module is finite.
@[protected, instance]
def
module.finite.map
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
(p : submodule R M)
[module.finite R ↥p]
(f : M →ₗ[R] N) :
module.finite R ↥(submodule.map f p)
Pushforwards of finite submodules are finite.
@[protected, instance]
theorem
module.finite.of_restrict_scalars_finite
(R : Type u_1)
(A : Type u_2)
(M : Type u_3)
[comm_semiring R]
[semiring A]
[add_comm_monoid M]
[module R M]
[module A M]
[algebra R A]
[is_scalar_tower R A M]
[hM : module.finite R M] :
module.finite A M
@[protected, instance]
def
module.finite.prod
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
[hM : module.finite R M]
[hN : module.finite R N] :
module.finite R (M × N)
@[protected, instance]
def
module.finite.pi
{R : Type u_1}
[semiring R]
{ι : Type u_2}
{M : ι → Type u_3}
[finite ι]
[Π (i : ι), add_comm_monoid (M i)]
[Π (i : ι), module R (M i)]
[h : ∀ (i : ι), module.finite R (M i)] :
module.finite R (Π (i : ι), M i)
theorem
module.finite.equiv
{R : Type u_1}
{M : Type u_4}
{N : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
[hM : module.finite R M]
(e : M ≃ₗ[R] N) :
module.finite R N
theorem
module.finite.trans
{R : Type u_1}
(A : Type u_2)
(M : Type u_3)
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[module A M]
[is_scalar_tower R A M]
[module.finite R A]
[module.finite A M] :
module.finite R M
@[protected, instance]
def
module.finite.base_change
(R : Type u_1)
(A : Type u_2)
(M : Type u_4)
[comm_semiring R]
[semiring A]
[algebra R A]
[add_comm_monoid M]
[module R M]
[h : module.finite R M] :
module.finite A (tensor_product R A M)
@[protected, instance]
def
module.finite.tensor_product
(R : Type u_1)
(M : Type u_4)
(N : Type u_5)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid N]
[module R N]
[hM : module.finite R M]
[hN : module.finite R N] :
module.finite R (tensor_product R M N)
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
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
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
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