Krull Dimension of Module

In this file we define Module.supportDim R M for an 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] : WithBot ℕ∞

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

Equations

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

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

theorem support_of_supportDim_eq_zero (R : Type u_1) [CommRing R] (N : Type u_3) [AddCommGroup N] [Module R N] [IsLocalRing R] (dim : Module.supportDim R N = 0) : Module.support R N = PrimeSpectrum.zeroLocus ↑(IsLocalRing.maximalIdeal R)