The quotient of a topological ring by an ideal

Two things about R ⧸ I that its algebraic theory does not record. It is T1 exactly when I is closed, and hence T0; and when f : R →+* S presents S as a topological quotient of R, the first isomorphism theorem R ⧸ ker f ≃+* S is a homeomorphism, so S carries the quotient topology and not merely a coarser one.

Mathlib proves the corresponding statement for the quotient of a topological group by a subgroup, as QuotientGroup.t1Space_iff and QuotientGroup.instT1Space. Those are stated for G ⧸ N with N : AddSubgroup G in the additive case, whereas R ⧸ I is the quotient by an Ideal. The two quotients are definitionally equal — Mathlib's own Ideal.topologicalRing_quotient builds the additive structure of R ⧸ I out of QuotientAddGroup.instIsTopologicalAddGroup — but reaching the group statement from an ideal still means presenting I as I.toAddSubgroup and transporting the closedness hypothesis along that presentation, which unification does not do on its own: with only IsClosed (I : Set R) in context, T1Space (R ⧸ I) is not synthesized. So the results below are that transport, and their proofs delegate to Mathlib rather than reproving anything.

Only separate continuity of addition is needed for the separation results, matching the hypotheses of the group statements they delegate to; no ring topology and no multiplicative continuity is used. The first isomorphism theorem below asks for even less: only that R ⧸ ker f carries the coinduced topology, which it does by construction.

The topological first isomorphism theorem

Algebraically, RingHom.quotientKerEquivOfSurjective identifies R ⧸ ker f with S for any surjective f. Topologically that says nothing: R ⧸ ker f carries the quotient topology, and a continuous surjection can land on a strictly coarser topology than the quotient one, so the bijection is continuous but need not be open. What closes the gap is exactly the hypothesis that f is a quotient map, and with it the algebraic isomorphism becomes a homeomorphism.

Over a Tate ring the quotient-map hypothesis is TauCeti.Huber.IsTateRing.isQuotientMap, an open mapping theorem.

Note that closedness of ker f comes for free once S is T1, since a kernel is the preimage of a point; it is not a further hypothesis of the theorem but a consequence for its consumers, and Ideal.Quotient.instT1Space above then hands back the separation of R ⧸ ker f.

Main results

• Ideal.Quotient.t1Space_iff: T1Space (R ⧸ I) ↔ IsClosed (I : Set R).
• Ideal.Quotient.instT1Space: the instance form, so that T0Space (R ⧸ I) is found automatically once I is known to be closed.
• Ideal.Quotient.continuous_lift: a continuous ring homomorphism annihilating I induces a continuous homomorphism on R ⧸ I, with no hypothesis on I.
• RingHom.isHomeomorph_kerLift: the map R ⧸ ker f →+* S induced by f is a homeomorphism when f is a quotient map. IsHomeomorph.homeomorph bundles that as R ⧸ ker f ≃ₜ S, and the map bundled is the ring homomorphism RingHom.kerLift, so the ring structure comes along with it and needs no transport of its own.

References

• Wedhorn, Adic Spaces, Example 6.38, where a rational localisation is presented as a quotient C ⧸ 𝔞 and its Hausdorff completion is taken.

theorem Ideal.Quotient.t1Space_iff {R : Type u_1} [TopologicalSpace R] [CommRing R] [SeparatelyContinuousAdd R] (I : Ideal R) : T1Space (R ⧸ I) ↔ IsClosed ↑I

The quotient of a topological ring by an ideal is T1 exactly when the ideal is closed. This is QuotientAddGroup.t1Space_iff read through the identification of R ⧸ I with the quotient of R by I.toAddSubgroup.

instance Ideal.Quotient.instT1Space {R : Type u_1} [TopologicalSpace R] [CommRing R] [SeparatelyContinuousAdd R] (I : Ideal R) [IsClosed ↑I] : T1Space (R ⧸ I)

The quotient of a topological ring by a closed ideal is T1, hence T0. Stated as an instance, with the closedness of I as an instance argument, so that the separation of R ⧸ I is available to instance search wherever I is known to be closed; this follows Ideal.Quotient.normedCommRing, which takes IsClosed (I : Set R) the same way.

theorem Ideal.Quotient.continuous_lift {R : Type u_1} [TopologicalSpace R] [CommRing R] (I : Ideal R) {S : Type u_2} [Semiring S] [TopologicalSpace S] {f : R →+* S} (hf : Continuous ⇑f) (hI : ∀ a ∈ I, f a = 0) : Continuous ⇑(lift I f hI)

A continuous ring homomorphism that kills I lifts to a continuous map on R ⧸ I.

No hypothesis on I is needed: closedness of I is what makes R ⧸ I separated (Ideal.Quotient.instT1Space above), which matters for maps into R ⧸ I, not for maps out of it.

theorem RingHom.isHomeomorph_kerLift {R : Type u_2} {S : Type u_3} [TopologicalSpace R] [CommRing R] [TopologicalSpace S] [Semiring S] {f : R →+* S} (hq : Topology.IsQuotientMap ⇑f) : IsHomeomorph ⇑f.kerLift

The topological first isomorphism theorem for rings. A ring homomorphism that is a quotient map presents its target as the quotient of its source by its kernel, topologically as well as algebraically.

A continuous surjection is not enough on its own. Surjectivity of f makes the lift bijective and continuity of f makes it continuous, but a continuous bijection is open only when the topology it lands in is no coarser than the one it carries; that f is a quotient map is exactly the statement that it is not coarser.

IsHomeomorph.homeomorph turns this into R ⧸ ker f ≃ₜ S. What it bundles is RingHom.kerLift, which is a ring homomorphism, so a consumer needing the isomorphism of rings has it already — RingHom.quotientKerEquivOfSurjective is that same map.