Closed proper ideals survive completion

For a closed proper ideal J of a topological commutative ring A, the ideal generated by its image in the separated completion Â remains proper. No separation or completeness assumption on A is needed.

The map A → (A / J)̂ extends through Â, yielding  → (A / J)̂. This map kills the extended ideal, while closedness and properness of J ensure that the target is nonzero.

Main results

• TauCeti.map_completion_ne_top_of_isClosed: a closed proper ideal stays proper in the completion.

This supplies the completion lemma for the proper-ideal criterion in rational covers (Wedhorn's Corollary 8.32).

References

• T. Wedhorn, Adic Spaces, Corollary 8.32.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, file projects/AdicSpaces/Adic spaces/IdealLocalizationCompletion.lean, was consulted to compare completion prerequisites. The closed-ideal argument here is independent; no code is ported.

theorem TauCeti.map_completion_ne_top_of_isClosed {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {J : Ideal A} (hclosed : IsClosed ↑J) (hJ : J ≠ ⊤) : Ideal.map UniformSpace.Completion.coeRingHom J ≠ ⊤

A closed proper ideal remains proper after extension to the separated completion.

The ideal need not be prime, and the original ring need not be Hausdorff or complete.