Reflexive duals over normal domains

Over a Noetherian integrally closed domain, the dual of every finite module is reflexive. In particular its double dual is a reflexive module, even when the original module has torsion. The assertion uses the canonical evaluation map of Mathlib's Module.IsReflexive.

In codimension at most one the local rings are principal ideal domains and finite torsion-free modules are free. In higher codimension dual modules have depth at least two; the local depth criterion for bijectivity then applies to evaluation. This is the algebraic input to reflexive hulls of coherent sheaves on normal schemes.

References

• Stacks Project, Lemma 31.13.8 (Tag 0AY4), with target the structure sheaf.

theorem Ideal.bijective_localizedModule_map_dual_eval_of_height_le_one {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.IsTorsionFree R M] (p : Ideal R) [p.IsPrime] (hp : p.height ≤ 1) : Function.Bijective ⇑((LocalizedModule.map p.primeCompl) (Module.Dual.eval R M))

Evaluation on a finite torsion-free module over a Noetherian normal domain becomes bijective at every prime of height at most one.

instance TauCeti.isReflexive_dual_of_isIntegrallyClosed {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.IsReflexive R (Module.Dual R M)

Over a Noetherian integrally closed domain, the dual of any finite module is reflexive.