A quotient of a nonarchimedean group is nonarchimedean

NonarchimedeanGroup G asks that every neighbourhood of 1 contain an open subgroup. That property passes to G ⧸ N, and the proof is the one-line reason it should: the quotient map is open, so it carries an open subgroup at 1 to one downstairs.

This is a statement about topological groups, not about rings: nothing in it uses multiplication on a ring or the ideal structure of I. It is therefore proved at the group level and transported with @[to_additive], and the ring statement is derived from the additive one rather than reproved — the same way Mathlib derives NonarchimedeanRing (R × S) from the additive group instance on a product.

Both instances factor through one transport lemma, NonarchimedeanGroup.nonarchimedean_of_isOpenMap in TauCeti.Topology.Algebra.Nonarchimedean.Basic: the property passes along any open homomorphism continuous at the identity, which is all the quotient map is ever used for here. The group instance applies it to QuotientGroup.mk', and the ring instance applies its additive form to Ideal.Quotient.mk through QuotientRing.isOpenMap_coe — so no identification of R ⧸ I with a quotient by I.toAddSubgroup is involved. The module instance applies the additive form to Submodule.mkQ through Submodule.isOpenMap_mkQ in the same way.

The consumer is the universal property of a rational localisation (TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_completion_locTopology), which requires [NonarchimedeanRing B] on its target. Wedhorn's Example 6.38 presents a rational localisation as a quotient C ⧸ a of a ring of restricted power series, so applying that universal property to C ⧸ a needs exactly the ring instance below.

Main results

• QuotientGroup.instNonarchimedeanGroup, and its additive form QuotientAddGroup.instNonarchimedeanAddGroup: G ⧸ N is nonarchimedean when G is.
• Ideal.Quotient.instNonarchimedeanRing: R ⧸ I is nonarchimedean when R is.
• Submodule.Quotient.instNonarchimedeanAddGroup: M ⧸ N is nonarchimedean when the topological module M is.

References

• Wedhorn, Adic Spaces, Example 6.38.

instance QuotientGroup.instNonarchimedeanGroup {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] (N : Subgroup G) [N.Normal] : NonarchimedeanGroup (G ⧸ N)

A quotient of a nonarchimedean group is nonarchimedean: the quotient map is continuous and open, so this is NonarchimedeanGroup.nonarchimedean_of_isOpenMap.

instance QuotientAddGroup.instNonarchimedeanAddGroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] (N : AddSubgroup G) [N.Normal] : NonarchimedeanAddGroup (G ⧸ N)

A quotient of a nonarchimedean additive group is nonarchimedean.

instance Ideal.Quotient.instNonarchimedeanRing {R : Type u_1} [CommRing R] [TopologicalSpace R] [NonarchimedeanRing R] (I : Ideal R) : NonarchimedeanRing (R ⧸ I)

A quotient of a nonarchimedean ring by an ideal is nonarchimedean. The quotient map is continuous and open, so the additive transport lemma applies directly; the nonarchimedean field is then inherited, as for NonarchimedeanRing (R × S) in Mathlib.

instance Submodule.Quotient.instNonarchimedeanAddGroup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [NonarchimedeanAddGroup M] (N : Submodule R M) : NonarchimedeanAddGroup (M ⧸ N)

A quotient of a nonarchimedean topological module by a submodule is nonarchimedean. The quotient map is continuous and open, so the additive transport lemma applies directly.