Pseudo-isomorphisms

A linear map f : M → N of modules over a commutative ring A is a pseudo-isomorphism if its kernel and cokernel are pseudo-null. The structure theory of finitely generated modules over a noetherian normal domain, and in particular of Iwasawa modules over Λ = O⟦T⟧, classifies modules up to pseudo-isomorphism: a finitely generated Λ-module admits a pseudo-isomorphism to an elementary module, and the characteristic ideal and the invariants μ and λ are invariant under pseudo-isomorphism.

Over a noetherian ring a map of finitely generated modules is a pseudo-isomorphism exactly when it becomes an isomorphism after localizing at every prime of height at most one. This local criterion drives the rest of the file: pseudo-isomorphisms compose, multiplication by an element lying in no prime of height at most one of the support is a pseudo-isomorphism, and a pseudo-isomorphism onto a finitely generated torsion module can be reversed. The last statement fails for modules that are not torsion: over ℤ_p⟦T⟧ the inclusion of the maximal ideal is a pseudo-isomorphism, while no pseudo-isomorphism goes the other way (Neukirch–Schmidt–Wingberg, Chapter V, §3, Exercise 1).

Main definitions

• TauCeti.Iwasawa.IsPseudoIsomorphism f: the kernel and the cokernel of f are pseudo-null.

Main results

• TauCeti.Iwasawa.isPseudoIsomorphism_iff_bijective_localizedModule_map: the local criterion, over a noetherian ring and for finitely generated modules.
• TauCeti.Iwasawa.IsPseudoIsomorphism.comp: over a noetherian ring, composites of pseudo-isomorphisms are pseudo-isomorphisms.
• TauCeti.Iwasawa.IsPseudoIsomorphism.prodMap: a product of pseudo-isomorphisms is a pseudo-isomorphism.
• TauCeti.Iwasawa.IsPseudoIsomorphism.restrict_torsion: over a noetherian domain, a pseudo-isomorphism restricts to a pseudo-isomorphism between the torsion submodules.
• TauCeti.Iwasawa.IsPseudoIsomorphism.finite_iff: over a noetherian ring, the source of a pseudo-isomorphism is finitely generated iff its target is.
• TauCeti.Iwasawa.isPseudoIsomorphism_lsmul: multiplication by a on a finitely generated module M is a pseudo-isomorphism if a lies in no prime of height at most one in the support of M.
• TauCeti.Iwasawa.isPseudoIsomorphism_prod_mkQ: if φ : M → N restricts to multiplication by a on a finitely generated submodule N, and a lies in no prime of height at most one in the support of N, then φ.prod N.mkQ : M → N × M ⧸ N is a pseudo-isomorphism.
• TauCeti.Iwasawa.IsPseudoIsomorphism.exists_reverse: over a noetherian ring, a pseudo-isomorphism M → N onto a finitely generated torsion module gives a pseudo-isomorphism N → M.
• TauCeti.Iwasawa.isPseudoIsomorphism_iff_bijective: over a ring of dimension at most one, such as a Dedekind domain, pseudo-isomorphisms are the isomorphisms.
• TauCeti.Iwasawa.isPseudoIsomorphism_iff_finite: over a noetherian local ring of dimension two with finite residue field, such as O⟦T⟧, a pseudo-isomorphism is a map with finite kernel and cokernel.
• TauCeti.Iwasawa.IsPseudoIsomorphism.natCard_quotSMulTop_div_natCard_torsionBy_eq: over such a ring, a pseudo-isomorphism M → N preserves the Euler quotient #(M ⧸ rM) / #M[r] of every scalar r; TauCeti.Iwasawa.IsPseudoIsomorphism.finite_torsionBy_iff and TauCeti.Iwasawa.IsPseudoIsomorphism.finite_quotSMulTop_iff say that it preserves the finiteness of M[r] and of M ⧸ rM.

The examples at the end of the file are over Λ = ℤ_p⟦T⟧. The first checks the multiplication criterion: multiplication by p on Λ ⧸ (T) ≅ ℤ_p is a pseudo-isomorphism, although it is not surjective. The second shows that the relation is not symmetric on modules that are not torsion: the inclusion of the maximal ideal 𝔪 is a pseudo-isomorphism, but no map Λ → 𝔪 is one.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (5.1.5)–(5.1.7).
• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, §13.1.

structure TauCeti.Iwasawa.IsPseudoIsomorphism {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : Prop

A linear map f : M → N is a pseudo-isomorphism if its kernel and its cokernel N ⧸ range f are pseudo-null.

• isPseudoNull_ker : IsPseudoNull A ↥f.ker

  The kernel of a pseudo-isomorphism is pseudo-null.

• isPseudoNull_coker : IsPseudoNull A (N ⧸ f.range)

  The cokernel of a pseudo-isomorphism is pseudo-null.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.of_bijective {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] {f : M →ₗ[A] N} (hf : Function.Bijective ⇑f) : IsPseudoIsomorphism f

A bijective linear map is a pseudo-isomorphism.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.bijective_localizedModule_map {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] {f : M →ₗ[A] N} (hf : IsPseudoIsomorphism f) (𝔭 : PrimeSpectrum A) (h𝔭 : 𝔭.asIdeal.height ≤ 1) : Function.Bijective ⇑((LocalizedModule.map 𝔭.asIdeal.primeCompl) f)

A pseudo-isomorphism becomes bijective after localizing at a prime of height at most one.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.of_bijective_localizedModule_map {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherianRing A] [Module.Finite A M] [Module.Finite A N] {f : M →ₗ[A] N} (h : ∀ (𝔭 : PrimeSpectrum A), 𝔭.asIdeal.height ≤ 1 → Function.Bijective ⇑((LocalizedModule.map 𝔭.asIdeal.primeCompl) f)) : IsPseudoIsomorphism f

Over a noetherian ring, a map of finitely generated modules that becomes bijective after localizing at every prime of height at most one is a pseudo-isomorphism.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.finite_iff {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherianRing A] {f : M →ₗ[A] N} (hf : IsPseudoIsomorphism f) : Module.Finite A M ↔ Module.Finite A N

Over a noetherian ring, the source of a pseudo-isomorphism is finitely generated iff its target is.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_iff_bijective_localizedModule_map {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherianRing A] [Module.Finite A M] [Module.Finite A N] {f : M →ₗ[A] N} : IsPseudoIsomorphism f ↔ ∀ (𝔭 : PrimeSpectrum A), 𝔭.asIdeal.height ≤ 1 → Function.Bijective ⇑((LocalizedModule.map 𝔭.asIdeal.primeCompl) f)

The local criterion: over a noetherian ring, a map of finitely generated modules is a pseudo-isomorphism iff it becomes bijective after localizing at every prime of height at most one.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.comp {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] [IsNoetherianRing A] {f : M →ₗ[A] N} {g : N →ₗ[A] P} (hg : IsPseudoIsomorphism g) (hf : IsPseudoIsomorphism f) : IsPseudoIsomorphism (g ∘ₗ f)

Over a noetherian ring, a composite of pseudo-isomorphisms is a pseudo-isomorphism.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.prodMap {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module A M'] [AddCommGroup N'] [Module A N'] {f : M →ₗ[A] N} {g : M' →ₗ[A] N'} (hf : IsPseudoIsomorphism f) (hg : IsPseudoIsomorphism g) : IsPseudoIsomorphism (f.prodMap g)

A product of two pseudo-isomorphisms is a pseudo-isomorphism.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.restrict_torsion {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsDomain A] [IsNoetherianRing A] {f : M →ₗ[A] N} (hf : IsPseudoIsomorphism f) : IsPseudoIsomorphism (f.restrict ⋯)

Over a noetherian domain, a pseudo-isomorphism restricts to a pseudo-isomorphism between the torsion submodules.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_lsmul {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] (a : A) (ha : ∀ 𝔭 ∈ Module.support A M, 𝔭.asIdeal.height ≤ 1 → a ∉ 𝔭.asIdeal) : IsPseudoIsomorphism ((LinearMap.lsmul A M) a)

The multiplication criterion: over a noetherian ring, multiplication by a on a finitely generated module M is a pseudo-isomorphism if a lies in no prime of height at most one in the support of M.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_prod_mkQ {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsNoetherianRing A] {N : Submodule A M} [Module.Finite A ↥N] {φ : M →ₗ[A] ↥N} {a : A} (hφ : φ ∘ₗ N.subtype = (LinearMap.lsmul A ↥N) a) (ha : ∀ 𝔭 ∈ Module.support A ↥N, 𝔭.asIdeal.height ≤ 1 → a ∉ 𝔭.asIdeal) : IsPseudoIsomorphism (φ.prod N.mkQ)

Let N be a finitely generated submodule of a module M over a noetherian ring, and let φ : M → N restrict to multiplication by a on N. If a lies in no prime of height at most one in the support of N, then m ↦ (φ m, m mod N) is a pseudo-isomorphism M → N × M ⧸ N.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.exists_mem_annihilator_notMem {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherianRing A] [Module.Finite A N] (hN : Module.IsTorsion A N) {f : M →ₗ[A] N} (hf : IsPseudoIsomorphism f) : ∃ γ ∈ Module.annihilator A ↥f.ker, γ ∈ Module.annihilator A (N ⧸ f.range) ∧ ∀ 𝔭 ∈ Module.support A N, 𝔭.asIdeal.height ≤ 1 → γ ∉ 𝔭.asIdeal

Prime avoidance for a pseudo-isomorphism f : M → N onto a finitely generated torsion module over a noetherian ring: some γ kills ker f and coker f and lies in no prime of height at most one in the support of N.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.exists_reverse {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsNoetherianRing A] [Module.Finite A N] (hN : Module.IsTorsion A N) {f : M →ₗ[A] N} (hf : IsPseudoIsomorphism f) : ∃ (g : N →ₗ[A] M), IsPseudoIsomorphism g

Over a noetherian ring, a pseudo-isomorphism M → N onto a finitely generated torsion module can be reversed: there is a pseudo-isomorphism N → M. Without the torsion hypothesis the statement fails: the inclusion of the maximal ideal of ℤ_p⟦T⟧ is a pseudo-isomorphism, but there is none in the other direction.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_iff_bijective {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [Ring.KrullDimLE 1 A] {f : M →ₗ[A] N} : IsPseudoIsomorphism f ↔ Function.Bijective ⇑f

Over a ring of Krull dimension at most one, such as a Dedekind domain, the pseudo-isomorphisms are the bijective linear maps.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_iff_finite {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsLocalRing A] [IsNoetherianRing A] [Finite (IsLocalRing.ResidueField A)] (hdim : ringKrullDim A = 2) {f : M →ₗ[A] N} : IsPseudoIsomorphism f ↔ Finite ↥f.ker ∧ Finite (N ⧸ f.range)

Over a noetherian local ring of dimension two with finite residue field, for example the Iwasawa algebra O⟦T⟧ of a complete discrete valuation ring O with finite residue field, a map is a pseudo-isomorphism iff its kernel and cokernel are finite.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.finite_torsionBy_iff {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsLocalRing A] [IsNoetherianRing A] [Finite (IsLocalRing.ResidueField A)] (hdim : ringKrullDim A = 2) {f : M →ₗ[A] N} (r : A) (hf : IsPseudoIsomorphism f) : Finite ↥(Submodule.torsionBy A M r) ↔ Finite ↥(Submodule.torsionBy A N r)

Over a noetherian local ring of dimension two with finite residue field, such as O⟦T⟧, a pseudo-isomorphism M → N preserves the finiteness of the r-torsion: M[r] is finite iff N[r] is.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.finite_quotSMulTop_iff {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsLocalRing A] [IsNoetherianRing A] [Finite (IsLocalRing.ResidueField A)] (hdim : ringKrullDim A = 2) {f : M →ₗ[A] N} (r : A) (hf : IsPseudoIsomorphism f) : Finite (QuotSMulTop r M) ↔ Finite (QuotSMulTop r N)

Over a noetherian local ring of dimension two with finite residue field, such as O⟦T⟧, a pseudo-isomorphism M → N preserves the finiteness of the cokernel of multiplication by r: M ⧸ rM is finite iff N ⧸ rN is.

theorem TauCeti.Iwasawa.IsPseudoIsomorphism.natCard_quotSMulTop_div_natCard_torsionBy_eq {A : Type u_1} [CommRing A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [IsLocalRing A] [IsNoetherianRing A] [Finite (IsLocalRing.ResidueField A)] (hdim : ringKrullDim A = 2) {f : M →ₗ[A] N} (r : A) (hf : IsPseudoIsomorphism f) : ↑(Nat.card (QuotSMulTop r M)) / ↑(Nat.card ↥(Submodule.torsionBy A M r)) = ↑(Nat.card (QuotSMulTop r N)) / ↑(Nat.card ↥(Submodule.torsionBy A N r))

The Euler quotient is invariant under pseudo-isomorphism. Over a noetherian local ring of dimension two with finite residue field, such as O⟦T⟧, a pseudo-isomorphism M → N satisfies #(M ⧸ rM) / #M[r] = #(N ⧸ rN) / #N[r] for every scalar r. Both sides are 0 when the torsion groups are infinite. For r = ω_n this lets the Euler quotient #(M ⧸ ω_n M) / #M[ω_n] of a finitely generated module be computed on an elementary module, while the finiteness of the coinvariants M ⧸ ω_n M and of the invariants M[ω_n] transfers by IsPseudoIsomorphism.finite_quotSMulTop_iff and IsPseudoIsomorphism.finite_torsionBy_iff; the individual orders need not agree.