Completions of nonarchimedean groups and rings

Three facts about the Hausdorff completion that need only the additive, resp. ring, structure: the closure of the image of an open additive subgroup is open, the kernel of the completion map is the closure of the zero ideal, and integral closedness of an open subring survives completion.

They are stated here rather than alongside the Huber-ring theory that uses them, since none mentions a pair of definition or an adic topology, and they live in the UniformSpace.Completion namespace of the construction they describe rather than in a TauCeti one.

The last of the three is Huber's Lemma 2.4.3(iv), Wedhorn's Lemma 7.47(4): if G is open and integrally closed in A, the closure Ĝ of its image in Â is integrally closed in Â. The proof below is Huber's. The integral closure H of Ĝ in Â contains the open subring Ĝ, hence is open, so every neighbourhood of a point of H meets the image of A inside H. For such an image i b, an integral relation over Ĝ is perturbed one coefficient at a time into a relation whose coefficients come from G; openness of Ĝ keeps the value of the perturbed relation at i b inside Ĝ, and an open G is closed, hence exactly the preimage of Ĝ, so that value is the image of an element of G. Subtracting it from the constant term leaves an integral relation for b over G, so b ∈ G, and i b therefore lies in the image of G.

Main results

• UniformSpace.Completion.isOpen_closure_image_coe: the closure in Â of the image of an open additive subgroup of A is open, and UniformSpace.Completion.isOpen_topologicalClosure_map_coeRingHom says the same of an open subring.
• UniformSpace.Completion.preimage_closure_image_coe: for an open subgroup G, the preimage under A → Â of the closure of the image of G is G itself. With the openness result above this is the bijection of Wedhorn's Example 5.33 between the open subgroups of A and of Â.
• UniformSpace.Completion.ker_coeRingHom: the kernel of A → Â is the closure of ⊥.
• UniformSpace.Completion.isIntegrallyClosedIn_topologicalClosure_map_coeRingHom: Huber's Lemma 2.4.3(iv), the closure in Â of the image of an open subring of A integrally closed in A is integrally closed in Â.

References

• Wedhorn, Adic Spaces, Proposition and Definition 5.32 and Example 5.33, for the completion of a topological group and ring; ker_coeRingHom is the statement there that the completion map has kernel closure {0}. Lemma 7.47(4) there is the statement that integral closedness of an open subring survives completion.
• R. Huber, Bewertungsspektrum und rigide Geometrie, Regensburger Mathematische Schriften 23, Universität Regensburg, 1993, Lemma 2.4.3(iv), whose proof UniformSpace.Completion.isIntegrallyClosedIn_topologicalClosure_map_coeRingHom follows.
• Mathlib's Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean, whose openness proof runs the same closure_image_mem_nhds-then-isOpen_of_mem_nhds argument these proofs follow.

theorem UniformSpace.Completion.isOpen_closure_image_coe {A : Type u_1} [AddGroup A] [UniformSpace A] [IsUniformAddGroup A] {G : AddSubgroup A} (hG : IsOpen ↑G) : IsOpen (closure (coe' '' ↑G))

The closure in the completion of the image of an open additive subgroup is open. Only the additive structure is involved.

theorem UniformSpace.Completion.preimage_closure_image_coe {A : Type u_1} [AddGroup A] [UniformSpace A] [SeparatelyContinuousAdd A] {G : AddSubgroup A} (hG : IsOpen ↑G) : coe' ⁻¹' closure (coe' '' ↑G) = ↑G

An open additive subgroup is recovered from the closure of its image. For G open, the preimage under A → Â of the closure of the image of G is G itself.

For a uniform additive group, this is the injectivity half of the bijection G ↦ closure (ι '' G) between the open subgroups of A and those of Â (Wedhorn, Example 5.33); isOpen_closure_image_coe says the map lands in open subgroups. No separation assumption on A is needed. Separate continuity of addition suffices for this preimage equality: an open subgroup is closed, and the completion map induces the topology on A.

@[simp]

theorem UniformSpace.Completion.coe_coeRingHom {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] : ⇑coeRingHom = coe'

The completion map A →+* Â, read as a function, is the coercion A → Â. Mathlib's Filter.Germ.coe_coeRingHom is the same statement for germs.

theorem UniformSpace.Completion.ker_coeRingHom {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] : RingHom.ker coeRingHom = ⊥.closure

The kernel of the completion map A → Â is the closure of the zero ideal.

theorem UniformSpace.Completion.coe_topologicalClosure_map_coeRingHom {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (G : Subring A) : ↑(Subring.map coeRingHom G).topologicalClosure = closure (coe' '' ↑G)

The closure Ĝ in Â of the image of a subring G of A is, as a set, the closure of the image of G under the completion coercion. This unfolds Subring.topologicalClosure and Subring.map in one step; it is how every argument below passes between Ĝ and that closure.

@[simp]

theorem UniformSpace.Completion.mem_topologicalClosure_map_coeRingHom_iff {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {G : Subring A} {x : Completion A} : x ∈ (Subring.map coeRingHom G).topologicalClosure ↔ x ∈ closure (coe' '' ↑G)

Membership in the closure Ĝ in Â of the image of a subring G of A, in the form the closure API consumes. This is the mem_-half of the pair whose coe_ half is above; the proofs below pass between the two forms at three separate sites.

theorem UniformSpace.Completion.isOpen_topologicalClosure_map_coeRingHom {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {G : Subring A} (hG : IsOpen ↑G) : IsOpen ↑(Subring.map coeRingHom G).topologicalClosure

The closure in Â of the image of an open subring of A is open: the subring form of isOpen_closure_image_coe.

theorem UniformSpace.Completion.isIntegrallyClosedIn_topologicalClosure_map_coeRingHom {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {G : Subring A} (hG : IsOpen ↑G) [IsIntegrallyClosedIn (↥G) A] : IsIntegrallyClosedIn (↥(Subring.map coeRingHom G).topologicalClosure) (Completion A)

Huber's Lemma 2.4.3(iv): the closure in Â of the image of an open subring G of A that is integrally closed in A is integrally closed in Â.