Transporting a nonarchimedean topology to a quotient or a subobject

NonarchimedeanGroup G asks that every neighbourhood of 1 contain an open subgroup. That property passes to the target of any open homomorphism that is continuous at 1: the image of an open subgroup inside f ⁻¹' U is an open subgroup inside U.

Mathlib has the embedding case, NonarchimedeanGroup.nonarchimedean_of_emb. Injectivity plays no part in the argument, so the statement below drops it and keeps only openness; the embedding case is recovered from it.

The transport is given in two steps, because the two halves have different hypotheses. exists_openSubgroup_subset_of_isOpenMap is the argument itself, and needs nothing of H beyond a group structure and a topology. nonarchimedean_of_isOpenMap packages it as the bundled class, which additionally requires [IsTopologicalGroup H] — not for the argument, but because NonarchimedeanGroup extends IsTopologicalGroup, so the parent structure is part of the conclusion. Consumers wanting the instance use the second; consumers wanting the property under minimal hypotheses use the first.

The file also records the subobject direction, which is the opposite transport and needs no openness at all: a subgroup or subring carries the subspace topology, and an open subgroup of the ambient group meets it in an open subgroup. Mathlib has neither of these two instances, and its NonarchimedeanGroup.nonarchimedean_of_emb does not give them, since it asks the inclusion to be an open embedding, which a subgroup's need not be.

Main results

• NonarchimedeanGroup.exists_openSubgroup_subset_of_isOpenMap, and its additive form NonarchimedeanAddGroup.exists_openAddSubgroup_subset_of_isOpenMap.
• Subgroup.instNonarchimedeanGroup and Subring.instNonarchimedeanRing: a subgroup of a nonarchimedean group, and a subring of a nonarchimedean ring, are nonarchimedean in the subspace topology. These are what put a nonarchimedean structure on the ring of definition of a rational localisation.
• NonarchimedeanGroup.nonarchimedean_of_isOpenMap, and its additive form NonarchimedeanAddGroup.nonarchimedean_of_isOpenMap.

theorem NonarchimedeanGroup.exists_openSubgroup_subset_of_isOpenMap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : ContinuousAt (⇑f) 1) (hopen : IsOpenMap ⇑f) {U : Set H} (hU : U ∈ nhds 1) : ∃ (V : OpenSubgroup H), ↑V ⊆ U

The nonarchimedean property transports along an open homomorphism. If f : G →* H is open and continuous at 1 and G is nonarchimedean, then every neighbourhood of 1 in H contains an open subgroup.

This is the whole of the transport argument, and it asks nothing of H beyond a group structure and a topology. The bundled form is nonarchimedean_of_isOpenMap, which needs [IsTopologicalGroup H] in addition — see the module docstring.

theorem NonarchimedeanAddGroup.exists_openAddSubgroup_subset_of_isOpenMap {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] [AddGroup H] [TopologicalSpace H] (f : G →+ H) (hf : ContinuousAt (⇑f) 0) (hopen : IsOpenMap ⇑f) {U : Set H} (hU : U ∈ nhds 0) : ∃ (V : OpenAddSubgroup H), ↑V ⊆ U

The nonarchimedean property transports along an open homomorphism. If f : G →+ H is open and continuous at 0 and G is nonarchimedean, then every neighbourhood of 0 in H contains an open additive subgroup.

theorem NonarchimedeanGroup.nonarchimedean_of_isOpenMap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : ContinuousAt (⇑f) 1) (hopen : IsOpenMap ⇑f) : NonarchimedeanGroup H

Transport along an open homomorphism. If f : G →* H is open and continuous at 1, and G is nonarchimedean, then so is H. This generalizes Mathlib's nonarchimedean_of_emb, which is the case of an open embedding; injectivity is not used.

[IsTopologicalGroup H] is required by the conclusion rather than by the argument: NonarchimedeanGroup extends IsTopologicalGroup, so continuous_mul and continuous_inv are fields of the structure being built. For the transport without it, use exists_openSubgroup_subset_of_isOpenMap.

theorem NonarchimedeanAddGroup.nonarchimedean_of_isOpenMap {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H) (hf : ContinuousAt (⇑f) 0) (hopen : IsOpenMap ⇑f) : NonarchimedeanAddGroup H

Transport along an open homomorphism. If f : G →+ H is open and continuous at 0, and G is nonarchimedean, then so is H.

instance Subgroup.instNonarchimedeanGroup {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] (H : Subgroup G) : NonarchimedeanGroup ↥H

A subgroup of a nonarchimedean group is nonarchimedean in the subspace topology: the traces of the ambient open subgroups are open subgroups of it, and they remain a basis.

instance AddSubgroup.instNonarchimedeanAddGroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] (H : AddSubgroup G) : NonarchimedeanAddGroup ↥H

A subgroup of a nonarchimedean additive group is nonarchimedean in the subspace topology: the traces of the ambient open subgroups are open subgroups of it, and they remain a basis.

instance Subring.instNonarchimedeanRing {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (S : Subring R) : NonarchimedeanRing ↥S

A subring of a nonarchimedean ring is nonarchimedean in the subspace topology.

Nothing is proved here that AddSubgroup.instNonarchimedeanAddGroup does not already prove at S.toAddSubgroup: a nonarchimedean ring is a nonarchimedean additive group, the two carriers agree, and the neighbourhood condition is the additive one verbatim. What the instance adds is the keying — typeclass search reaching for NonarchimedeanRing ↥S does not unfold Subring to AddSubgroup on its own.