Documentation

Mathlib.RingTheory.KrullDimension.Module

Krull Dimension of Module #

In this file we define Module.supportDim R M for a R-module M as the krull dimension of its support. It is equal to the krull dimension of R / Ann M when M is finitely generated.

noncomputable def Module.supportDim (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

The krull dimension of module, defined as krullDim of its support.

Equations

Module.supportDim R M = Order.krullDim ↑(Module.support R M)

Instances For

theorem Module.supportDim_eq_bot_of_subsingleton (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Subsingleton M] :

supportDim R M = ⊥

theorem Module.supportDim_ne_bot_of_nontrivial (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Nontrivial M] :

supportDim R M ≠ ⊥

theorem Module.supportDim_eq_bot_iff_subsingleton (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

supportDim R M = ⊥ ↔ Subsingleton M

theorem Module.supportDim_ne_bot_iff_nontrivial (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

supportDim R M ≠ ⊥ ↔ Nontrivial M

theorem Module.supportDim_eq_ringKrullDim_quotient_annihilator (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] :

supportDim R M = ringKrullDim (R ⧸ annihilator R M)

theorem Module.supportDim_self_eq_ringKrullDim (R : Type u_1) [CommRing R] :

supportDim R R = ringKrullDim R

theorem Module.supportDim_le_ringKrullDim (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

supportDim R M ≤ ringKrullDim R

theorem Module.supportDim_quotient_eq_ringKrullDim {R : Type u_1} [CommRing R] (I : Ideal R) :

supportDim R (R ⧸ I) = ringKrullDim (R ⧸ I)

theorem Module.supportDim_le_of_injective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : Function.Injective ⇑f) :

supportDim R M ≤ supportDim R N

theorem Module.supportDim_le_of_surjective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : Function.Surjective ⇑f) :

supportDim R N ≤ supportDim R M

theorem Module.supportDim_eq_of_equiv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) :

supportDim R M = supportDim R N