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]
:
The krull dimension of module, defined as krullDim of its support.
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]
:
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)
:
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)
:
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)
: