The reflexive hull up to pseudo-isomorphism

Let A be a noetherian integrally closed domain and M a finitely generated torsion-free A-module. The canonical map M → M** into the reflexive hull is a pseudo-isomorphism: at a prime 𝔭 of height at most one, the ring A_𝔭 is a field or a discrete valuation ring, so M_𝔭 is free and hence reflexive, and taking double duals commutes with localization for finitely presented modules.

Over a regular local ring of dimension at most two, such as the Iwasawa algebra Λ = O⟦T⟧, reflexive modules are free (TauCeti.IsRegularLocalRing.free_of_isReflexive), so every finitely generated torsion-free module is pseudo-isomorphic to a free module of finite rank. Together with the splitting off of the torsion submodule (TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_torsion_mkQ), this reduces the structure theorem for finitely generated modules over such rings to the torsion case.

Main results

• TauCeti.Iwasawa.isPseudoIsomorphism_dual_eval: over a noetherian integrally closed domain, M → M** is a pseudo-isomorphism for every finitely generated torsion-free module M.
• TauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_of_isTorsionFree: over a regular local ring of dimension at most two, a finitely generated torsion-free module admits a pseudo-isomorphism to Aⁿ for some n.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, Chapter V, §1, where these facts enter the proof of the structure theorem (5.1.10).
• N. Bourbaki, Commutative Algebra, Chapter VII, §4.

theorem TauCeti.Iwasawa.isPseudoIsomorphism_dual_eval {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] [Module.Finite A M] [Module.IsTorsionFree A M] : IsPseudoIsomorphism (Module.Dual.eval A M)

The reflexive hull. Over a noetherian integrally closed domain, the canonical map M → M** of a finitely generated torsion-free module into its double dual is a pseudo-isomorphism.

theorem TauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_of_isTorsionFree {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) [Module.Finite A M] [Module.IsTorsionFree A M] : ∃ (n : ℕ) (f : M →ₗ[A] Fin n → A), IsPseudoIsomorphism f

Over a regular local ring of dimension at most two, a finitely generated torsion-free module M admits a pseudo-isomorphism M → Aⁿ for some n: its reflexive hull is free.