Pseudo-null modules, pseudo-isomorphisms, and pseudo-isomorphic modules

Pseudo-null modules

class Module.IsPseudoNull (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] : Prop

A finitely generated module M over a Noetherian ring A is called pseudo-null, if every prime ideals in the support of M are of height ≥ 2. Equivalently, if M localized at p equals zero for all prime ideals p of height ≤ 1.

• two_le_primeHeight (p : PrimeSpectrum A) : p ∈ support A M → 2 ≤ p.asIdeal.primeHeight

theorem Module.isPseudoNull_iff (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] : IsPseudoNull A M ↔ ∀ p ∈ support A M, 2 ≤ p.asIdeal.primeHeight

theorem Module.isPseudoNull_iff_primeHeight_le_one_imp_subsingleton (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] : IsPseudoNull A M ↔ ∀ (p : PrimeSpectrum A), p.asIdeal.primeHeight ≤ 1 → Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

theorem Module.IsPseudoNull.subsingleton_of_primeHeight_le_one (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [IsPseudoNull A M] {p : PrimeSpectrum A} (hp : p.asIdeal.primeHeight ≤ 1) : Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

theorem LinearEquiv.isPseudoNull_iff {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M ≃ₗ[A] N) : Module.IsPseudoNull A M ↔ Module.IsPseudoNull A N

theorem LinearEquiv.isPseudoNull {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M ≃ₗ[A] N) [Module.IsPseudoNull A M] : Module.IsPseudoNull A N

instance Module.isPseudoNull_of_subsingleton (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [Subsingleton M] : IsPseudoNull A M

theorem Module.isPseudoNull_iff_subsingleton_of_krullDimLE_one (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [Ring.KrullDimLE 1 A] : IsPseudoNull A M ↔ Subsingleton M

A module over a ring with Krull dimension ≤ 1 is pseudo-null if and only it is zero.

theorem IsNoetherianRing.exists_nilradical_pow_eq_bot (A : Type u) [CommRing A] [IsNoetherianRing A] : ∃ (n : ℕ), nilradical A ^ n = ⊥

theorem IsNoetherianRing.exists_pow_le_of_zeroLocus_eq_singleton (A : Type u) [CommRing A] [IsNoetherianRing A] {I : Ideal A} {p : PrimeSpectrum A} (h : PrimeSpectrum.zeroLocus ↑I = {p}) : ∃ (n : ℕ), p.asIdeal ^ n ≤ I

theorem Module.support_subset_maximalIdeal_iff_exists_pow_le_annihilator (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [IsNoetherianRing A] [IsLocalRing A] [Module.Finite A M] : support A M ⊆ {{ asIdeal := IsLocalRing.maximalIdeal A, isPrime := ⋯ }} ↔ ∃ (n : ℕ), IsLocalRing.maximalIdeal A ^ n ≤ annihilator A M

theorem Module.isPseudoNull_iff_support_subset_maximalIdeal_of_ringKrullDim_eq_two (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (hd : ringKrullDim A = 2) [IsLocalRing A] : IsPseudoNull A M ↔ support A M ⊆ {{ asIdeal := IsLocalRing.maximalIdeal A, isPrime := ⋯ }}

theorem Module.isPseudoNull_iff_finite_of_ringKrullDim_eq_two (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (hd : ringKrullDim A = 2) [IsNoetherianRing A] [IsLocalRing A] [Finite (IsLocalRing.ResidueField A)] [Module.Finite A M] : IsPseudoNull A M ↔ Finite M

Let A be a Noetherian local ring of Krull dimension 2 with finite residue field, M be a finitely generated A-module. Then M is pseudo-null if and only if the cardinality of M is finite.

theorem Module.isPseudoNull_of_injective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (h : Function.Injective ⇑f) [IsPseudoNull A N] : IsPseudoNull A M

Pseudo-null modules are preserved by taking submodules.

theorem Module.isPseudoNull_of_surjective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (h : Function.Surjective ⇑f) [IsPseudoNull A M] : IsPseudoNull A N

Pseudo-null modules are preserved by taking quotient modules.

theorem Module.isPseudoNull_of_exact {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type x} [AddCommGroup P] [Module A P] (f : M →ₗ[A] N) (g : N →ₗ[A] P) (h : Function.Exact ⇑f ⇑g) [IsPseudoNull A M] [IsPseudoNull A P] : IsPseudoNull A N

If M, P are pseudo-null, M → N → P is exact at N, then N is also pseudo-null.

Pseudo-isomorphisms

structure LinearMap.IsPseudoIsomorphism {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : Prop

A linear map between two finitely generated modules over a Noetherian ring is called a pseudo-isomorphism if its kernel and cokernel are pseudo-null.

• isPseudoNull_ker : Module.IsPseudoNull A ↥(ker f)
• isPseudoNull_coker : Module.IsPseudoNull A (N ⧸ range f)

theorem LinearMap.isPseudoIsomorphism_iff {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : f.IsPseudoIsomorphism ↔ Module.IsPseudoNull A ↥(ker f) ∧ Module.IsPseudoNull A (N ⧸ range f)

theorem LinearMap.isPseudoIsomorphism_iff_primeHeight_le_one_imp_bijective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : f.IsPseudoIsomorphism ↔ ∀ (p : PrimeSpectrum A), p.asIdeal.primeHeight ≤ 1 → Function.Bijective ⇑((LocalizedModule.map p.asIdeal.primeCompl) f)

theorem LinearMap.IsPseudoIsomorphism.bijective_of_primeHeight_le_one {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {f : M →ₗ[A] N} (H : f.IsPseudoIsomorphism) {p : PrimeSpectrum A} (hp : p.asIdeal.primeHeight ≤ 1) : Function.Bijective ⇑((LocalizedModule.map p.asIdeal.primeCompl) f)

theorem LinearMap.isPseudoIsomorphism_iff_of_injective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (h : Function.Injective ⇑f) : f.IsPseudoIsomorphism ↔ Module.IsPseudoNull A (N ⧸ range f)

theorem LinearMap.isPseudoIsomorphism_iff_of_surjective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (h : Function.Surjective ⇑f) : f.IsPseudoIsomorphism ↔ Module.IsPseudoNull A ↥(ker f)

theorem LinearMap.isPseudoIsomorphism_of_bijective {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (h : Function.Bijective ⇑f) : f.IsPseudoIsomorphism

theorem LinearEquiv.isPseudoIsomorphism {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M ≃ₗ[A] N) : (↑f).IsPseudoIsomorphism

theorem LinearMap.isPseudoIsomorphism_id {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] : id.IsPseudoIsomorphism

theorem LinearMap.isPseudoIsomorphism_zero_iff {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] : IsPseudoIsomorphism 0 ↔ Module.IsPseudoNull A M ∧ Module.IsPseudoNull A N

theorem LinearMap.isPseudoIsomorphism_of_isPseudoNull {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) [Module.IsPseudoNull A M] [Module.IsPseudoNull A N] : f.IsPseudoIsomorphism

theorem LinearMap.isPseudoIsomorphism_iff_of_isPseudoNull_left {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) [Module.IsPseudoNull A M] : f.IsPseudoIsomorphism ↔ Module.IsPseudoNull A N

If M is pseudo-null, then M → N is a pseudo-isomorphism if and only if N is pseudo-null.

theorem LinearMap.isPseudoIsomorphism_iff_of_isPseudoNull_right {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) [Module.IsPseudoNull A N] : f.IsPseudoIsomorphism ↔ Module.IsPseudoNull A M

If N is pseudo-null, then M → N is a pseudo-isomorphism if and only if M is pseudo-null.

theorem LinearMap.IsPseudoIsomorphism.comp {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type x} [AddCommGroup P] [Module A P] {f : M →ₗ[A] N} {g : N →ₗ[A] P} (hg : g.IsPseudoIsomorphism) (hf : f.IsPseudoIsomorphism) : (g ∘ₗ f).IsPseudoIsomorphism

Composition of two pseudo-isomorphisms is a pseudo-isomorphism.

Pseudo-isomorphic modules

structure Module.IsPseudoIsomorphic (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (N : Type w) [AddCommGroup N] [Module A N] : Prop

Two finitely generated modules M, N over a Noetherian ring A is called pseudo-isomorphic, if there exists a linear map f : M →ₗ[A] N which is a pseudo-isomorphism.

WARNING: pseudo-isomorphic is not symmetric in general.

• exists_isPseudoIsomorphism : ∃ (f : M →ₗ[A] N), f.IsPseudoIsomorphism

theorem Module.isPseudoIsomorphic_iff (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (N : Type w) [AddCommGroup N] [Module A N] : M ∼ₚᵢₛ[A] N ↔ ∃ (f : M →ₗ[A] N), f.IsPseudoIsomorphism

def Module.«term_∼ₚᵢₛ[_]_» : Lean.TrailingParserDescr

Two finitely generated modules M, N over a Noetherian ring A is called pseudo-isomorphic, if there exists a linear map f : M →ₗ[A] N which is a pseudo-isomorphism.

WARNING: pseudo-isomorphic is not symmetric in general.

Equations

• One or more equations did not get rendered due to their size.

theorem Module.IsPseudoIsomorphic.refl (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] : M ∼ₚᵢₛ[A] M

Pseudo-isomorphic is reflexive.

theorem Module.isPseudoIsomorphic_iff_of_isPseudoNull_left (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (N : Type w) [AddCommGroup N] [Module A N] [IsPseudoNull A M] : M ∼ₚᵢₛ[A] N ↔ IsPseudoNull A N

theorem Module.isPseudoIsomorphic_iff_of_isPseudoNull_right (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] (N : Type w) [AddCommGroup N] [Module A N] [IsPseudoNull A N] : M ∼ₚᵢₛ[A] N ↔ IsPseudoNull A M

theorem Module.IsPseudoIsomorphic.trans {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] {P : Type x} [AddCommGroup P] [Module A P] (h1 : M ∼ₚᵢₛ[A] N) (h2 : N ∼ₚᵢₛ[A] P) : M ∼ₚᵢₛ[A] P

Pseudo-isomorphic is transitive.