Localising an open subring at a topologically nilpotent element

Let A be a commutative ring with a topology and separately continuous multiplication, let B be an open subring of A, and let s : B be topologically nilpotent in A. Inverting s on both sides does not distinguish the two rings: the induced map B_s → A_s is a ring isomorphism.

The point is that B is open, so a topologically nilpotent s absorbs every element of A into B after enough multiplications. Passing to B_s makes that absorption invertible, which is exactly what surjectivity needs. Injectivity is not topological at all and is Mathlib's already.

Implementation notes

Surjectivity goes through the Mathlib criterion rather than through elements of the localisations: IsLocalization.Away.map_surjective_iff reduces it to "for every a : A, some sᵐ * a is the image of an element of B", which is exists_mul_pow_mem_of_isTopologicallyNilpotent verbatim, up to commuting the product.

Only SeparatelyContinuousMul is assumed, matching the absorption lemma: continuity of addition, a nonarchimedean neighbourhood basis and any Huber structure are all irrelevant here.

Injectivity is not proved here at all: it is Mathlib's IsLocalization.map_injective_of_injective applied to Subring.subtype_injective, which already says an injective ring map induces an injective map on the corresponding localisations. Nothing about the subring being open, or about s, enters that half.

Source

Wedhorn, Adic Spaces (arXiv:1910.05934v1), the localisation step inside the proof of Lemma 7.44(1). Only that step is formalised here — the spectral half of 7.44(1), the homeomorphism between the complements of the two closed subsets, is not proved in this file.

Main results

• TauCeti.Localization.awayMap_subtype_surjective_of_isTopologicallyNilpotent: the induced map on localisations is surjective when the subring is open and s is topologically nilpotent.
• TauCeti.Localization.awayRingEquivOfIsTopologicallyNilpotent: the resulting isomorphism B_s ≃+* A_s.

theorem TauCeti.Localization.awayMap_subtype_surjective_of_isTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousMul A] {B : Subring A} {s : ↥B} (Bs : Type u_2) (As : Type u_3) [CommSemiring Bs] [CommSemiring As] [Algebra (↥B) Bs] [IsLocalization.Away s Bs] [Algebra A As] [IsLocalization.Away (B.subtype s) As] (hB : IsOpen ↑B) (hs : IsTopologicallyNilpotent ↑s) : Function.Surjective ⇑(IsLocalization.Away.map Bs As B.subtype s)

The localisation of an open subring surjects onto the localisation of the ring. Given a : A, the topologically nilpotent s absorbs it into the open subring B after some number of multiplications, and inverting s undoes them.

noncomputable def TauCeti.Localization.awayRingEquivOfIsTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousMul A] {B : Subring A} {s : ↥B} (Bs : Type u_2) (As : Type u_3) [CommSemiring Bs] [CommSemiring As] [Algebra (↥B) Bs] [IsLocalization.Away s Bs] [Algebra A As] [IsLocalization.Away (B.subtype s) As] (hB : IsOpen ↑B) (hs : IsTopologicallyNilpotent ↑s) : Bs ≃+* As

Inverting a topologically nilpotent element does not see an open subring. For B an open subring of A and s : B topologically nilpotent in A, the induced map B_s → A_s is a ring isomorphism: injective for any subring by IsLocalization.map_injective_of_injective, surjective because s absorbs into the open B.

@[simp]

theorem TauCeti.Localization.coe_awayRingEquivOfIsTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousMul A] {B : Subring A} {s : ↥B} (Bs : Type u_2) (As : Type u_3) [CommSemiring Bs] [CommSemiring As] [Algebra (↥B) Bs] [IsLocalization.Away s Bs] [Algebra A As] [IsLocalization.Away (B.subtype s) As] (hB : IsOpen ↑B) (hs : IsTopologicallyNilpotent ↑s) : ⇑(awayRingEquivOfIsTopologicallyNilpotent Bs As hB hs) = ⇑(IsLocalization.Away.map Bs As B.subtype s)