Completion of strict exact sequences of nonarchimedean groups

A homomorphism of topological groups is strict (Topology.IsStrictMap) if it is continuous and open onto its image with the subspace topology. For first-countable nonarchimedean abelian groups, strictness and exactness survive passage to the separated completions: if G → H → K is exact with strict maps, then so is Completion G → Completion H → Completion K. No Hausdorff hypothesis is made on the original groups; an indiscrete group completes to zero.

This is how exactness of an algebraic complex of topological modules (for instance a Čech complex of localizations with adic topologies) becomes exactness of the complex of completions, which is the form used in sheafiness arguments for Huber rings. Applied at each degree, it shows that the completion of a strict exact complex of such groups is again strict and exact.

The proof factors a strict map f as the open surjection onto its range followed by the inclusion of the range (AddMonoidHom.completion_eq_comp_rangeRestrict). Completion keeps the first an open surjection (AddMonoidHom.surjective_completion) and turns the second into a uniform embedding whose image is the closure of the range (AddMonoidHom.range_completion). At the left end of a complex, an injective strict map is an embedding, and its completion is a uniform embedding by AddMonoidHom.isUniformEmbedding_completion.

Main results

• AddMonoidHom.range_completion_of_isStrictMap: the image of the completion of a strict map is the closure of the image of its range.
• AddMonoidHom.ker_completion_of_isStrictMap: the kernel of the completion of a strict map is the closure of the image of its kernel.
• AddMonoidHom.isStrictMap_completion: completion preserves strict maps.
• AddMonoidHom.exact_completion: completion preserves strict exact sequences.

References

• N. Bourbaki, Commutative Algebra, Chapter III, §2, no. 12, Lemma 2.
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, proof of (1.3).

theorem AddMonoidHom.range_completion_of_isStrictMap {G : Type u_1} {H : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] [AddGroup H] [UniformSpace H] [IsUniformAddGroup H] [(nhds 0).IsCountablyGenerated] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) : (f.completion ⋯).range = (AddSubgroup.map UniformSpace.Completion.toCompl f.range).topologicalClosure

The image of the completion of a strict homomorphism is the closure of the image of its range. Without strictness the image can be strictly smaller than this closure: the identity of ℤ, from the discrete to the p-adic topology, completes to the inclusion ℤ → ℤ_[p].

theorem AddMonoidHom.isStrictMap_completion {G : Type u_1} {H : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] [AddGroup H] [UniformSpace H] [IsUniformAddGroup H] [(nhds 0).IsCountablyGenerated] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) : Topology.IsStrictMap ⇑(f.completion ⋯)

Completion preserves strict homomorphisms out of a first-countable nonarchimedean group.

theorem AddMonoidHom.ker_completion_of_isStrictMap {G : Type u_1} {H : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] [AddGroup H] [UniformSpace H] [IsUniformAddGroup H] (f : G →+ H) (hf : Topology.IsStrictMap ⇑f) : (f.completion ⋯).ker = (AddSubgroup.map UniformSpace.Completion.toCompl f.ker).topologicalClosure

The kernel of the completion of a strict homomorphism is the closure of the image of its kernel. This extends AddMonoidHom.ker_completion from open maps to strict maps.

theorem AddMonoidHom.exact_completion {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [NonarchimedeanAddGroup M] [(nhds 0).IsCountablyGenerated] [AddCommGroup N] [UniformSpace N] [IsUniformAddGroup N] [NonarchimedeanAddGroup N] [AddGroup P] [UniformSpace P] [IsUniformAddGroup P] {f : M →+ N} {g : N →+ P} (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g) (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(f.completion ⋯) ⇑(g.completion ⋯)

Completion preserves strict exact sequences. If M → N → P is exact with strict maps, where M is a first-countable nonarchimedean group and N is a nonarchimedean group, then the sequence of separated completions is exact. Its maps are again strict by AddMonoidHom.isStrictMap_completion when M and N are first countable. No Hausdorff hypothesis is needed.