Structure theorem of finitely generated torsion module up to pseudo-isomorphism

theorem PrimeSpectrum.localization_comap_range_eq_of_isDomain_of_primeHeight_eq_one {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] (s : Set (PrimeSpectrum R)) (hs : s ⊆ {p : PrimeSpectrum R | p.asIdeal.primeHeight = 1}) (hn : s.Nonempty) (hfin : s.Finite) [IsLocalization (⨅ p ∈ s, p.asIdeal.primeCompl) S] : Set.range ⇑(comap (algebraMap R S)) = s ∪ {{ asIdeal := ⊥, isPrime := ⋯ }}

theorem RingEquiv.isPrincipalIdealRing {α : Type u_1} {β : Type u_2} [Semiring α] [Semiring β] [IsPrincipalIdealRing β] (e : α ≃+* β) : IsPrincipalIdealRing α

Krull domain

class IsKrullDomain (A : Type u_1) [CommRing A] [IsDomain A] : Prop

An integral domain A is a Krull domain if it satisfies the following properties:

• Aₚ is a discrete valuation ring for every height one prime p of A.
• The intersection of all such Aₚ is equal to A.
• Any nonzero element of A is contained in only a finitely many height one primes of A.

See https://en.wikipedia.org/wiki/Krull_ring.

• isDiscreteValuationRing_localization (p : PrimeSpectrum A) : p.asIdeal.primeHeight = 1 → IsDiscreteValuationRing (Localization p.asIdeal.primeCompl)
• biInf_eq_bot : ⨅ p ∈ {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1}, Localization.subalgebra (FractionRing A) p.asIdeal.primeCompl ⋯ = ⊥
• finite (a : A) : a ≠ 0 → {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1 ∧ a ∈ p.asIdeal}.Finite

@[instance 100]

instance IsKrullDomain.isIntegrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] [IsKrullDomain A] : IsIntegrallyClosed A

@[instance 100]

instance IsIntegrallyClosed.isKrullDomain_of_isNoetherianRing (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] : IsKrullDomain A

theorem isKrullDomain_iff_isIntegrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] : IsKrullDomain A ↔ IsIntegrallyClosed A

A Noetherian ring is a Krull domain if and only if it is an integrally closed domain.

@[instance 100]

instance UniqueFactorizationMonoid.isKrullDomain (A : Type u_1) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] : IsKrullDomain A

Height one localization is PID

class HeightOneLocalizationIsPID (A : Type u_1) [CommRing A] : Prop

A typeclass asserting that for any finitely many height one primes p₁, ..., pₙ of A, let S = A \ ⋃ i, pᵢ, then S⁻¹A is a PID.

• isPrincipalIdealRing_localization (s : Set (PrimeSpectrum A)) : s ⊆ {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1} → s.Nonempty → s.Finite → IsDomain (Localization (⨅ p ∈ s, p.asIdeal.primeCompl)) ∧ IsPrincipalIdealRing (Localization (⨅ p ∈ s, p.asIdeal.primeCompl))

noncomputable def IsLocalizedModule.getNumerator {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (x : M') : M

Equations

• IsLocalizedModule.getNumerator S f x = (Classical.choose ⋯).1

theorem IsLocalizedModule.mem_of_getNumerator_image_mem {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] {R' : Type u_4} [CommSemiring R'] [Algebra R R'] [Module R' M'] [IsLocalization S R'] [Module R M] [Module R M'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N' : Submodule R' M'} {x : M'} (hx : f (getNumerator S f x) ∈ N') : x ∈ N'

If the image of getNumerator x under f is in a submodule N' of M', then x itself lies in N'.

noncomputable def IsLocalizedModule.finsetNumerator {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [DecidableEq M] (s : Finset M') : Finset M

Equations

• IsLocalizedModule.finsetNumerator S f s = Finset.image (IsLocalizedModule.getNumerator S f) s

theorem Module.finite_of_finite_isLocalized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)) : Module.Finite R M

theorem Module.finite_of_finite_localized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [AddCommMonoid M] [Module R M] (H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl M)) : Module.Finite R M

theorem Module.finite_of_finite_localized_maximal' {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [AddCommMonoid M] [Module R M] (H : ∀ (p : MaximalSpectrum R), Module.Finite (Localization p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M)) : Module.Finite R M

theorem isPrincipalIdealRing_of_isPrincipalIdealRing_localization (A : Type u_1) [CommRing A] [IsDomain A] [Finite (MaximalSpectrum A)] (hpid : ∀ (p : MaximalSpectrum A), IsPrincipalIdealRing (Localization p.asIdeal.primeCompl)) : IsPrincipalIdealRing A

If a semilocal integral domain which is not a field satisfies that it localized at all maximal ideals is a PID, then itself is a PID.

@[instance 100]

instance IsKrullDomain.heightOneLocalizationIsPID (A : Type u_1) [CommRing A] [IsDomain A] [IsKrullDomain A] : HeightOneLocalizationIsPID A

Structure theorem under the assumption that height one localization is PID

theorem LinearMap.isPseudoIsomorphism_iff_bijective_map {A : Type u_1} [CommRing A] [IsNoetherianRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] (hMT : Module.IsTorsion A M) {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A N] (hNT : Module.IsTorsion A N) (f : M →ₗ[A] N) : f.IsPseudoIsomorphism ↔ Function.Bijective ⇑((LocalizedModule.map (⨅ p ∈ (Module.support A M ∪ Module.support A N) ∩ {p : PrimeSpectrum A | p.asIdeal.primeHeight = 1}, p.asIdeal.primeCompl)) f)

Let A be a Noetherian ring and let M, N be finitely generated torsion A-modules. Let p₁, ..., pₙ be all height one primes in Supp(M) ∪ Supp(N), let S = A \ ⋃ i, pᵢ. Then an A-linear map f : M → N is a pseudo-isomorphism if and only if S⁻¹f : S⁻¹M → S⁻¹N is an isomorphism.

theorem Module.IsTorsion.isPseudoIsomorphic_pi {A : Type u} [CommRing A] [IsNoetherianRing A] [HeightOneLocalizationIsPID A] {M : Type u_1} [AddCommGroup M] [Module A M] [Module.Finite A M] (hMT : IsTorsion A M) : ∃ (ι : Type u) (x : Fintype ι) (p : ι → PrimeSpectrum A) (_ : ∀ (i : ι), (p i).asIdeal.primeHeight = 1) (e : ι → ℕ), M ∼ₚᵢₛ[A] ((i : ι) → A ⧸ (p i).asIdeal ^ e i)

Structure theorem of finitely generated torsion modules up to pseudo-isomorphism: A finitely generated torsion module over a Noetherian ring A satisfying HeightOneLocalizationIsPID is pseudo-isomorphic to a finite product of some A ⧸ pᵢ ^ eᵢ where the pᵢ ^ eᵢ are powers of height one primes of A.

theorem Module.IsTorsion.isPseudoIsomorphic_iff_nonempty_linearEquiv_localizedModule {A : Type u_1} [CommRing A] [IsNoetherianRing A] [HeightOneLocalizationIsPID A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] (hMT : IsTorsion A M) {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A N] (hNT : IsTorsion A N) : M ∼ₚᵢₛ[A] N ↔ ∀ (p : PrimeSpectrum A), p.asIdeal.primeHeight = 1 → Nonempty (LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization p.asIdeal.primeCompl] LocalizedModule p.asIdeal.primeCompl N)

Let A be a Noetherian ring satisfying HeightOneLocalizationIsPID. Then two finitely generated torsion A-modules M, N are pseudo-isomorphic if and only if their localizations at all height one primes are isomorphic.

theorem Module.IsPseudoIsomorphic.symm {A : Type u_1} [CommRing A] [IsNoetherianRing A] [HeightOneLocalizationIsPID A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] (hMT : IsTorsion A M) {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A N] (hNT : IsTorsion A N) (H : M ∼ₚᵢₛ[A] N) : N ∼ₚᵢₛ[A] M

Let A be a Noetherian ring satisfying HeightOneLocalizationIsPID. Then pseudo-isomorphic between two finitely generated torsion A-modules are symmectric.

theorem Module.isPseudoIsomorphic_comm {A : Type u_1} [CommRing A] [IsNoetherianRing A] [HeightOneLocalizationIsPID A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] (hMT : IsTorsion A M) {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A N] (hNT : IsTorsion A N) : M ∼ₚᵢₛ[A] N ↔ N ∼ₚᵢₛ[A] M

Let A be a Noetherian ring satisfying HeightOneLocalizationIsPID. Then pseudo-isomorphic between two finitely generated torsion A-modules are symmectric.