Removing the closure from Henkel's approximation

The Baire step of Henkel's open mapping theorem produces a point of closure (f '' U), not of f '' U, and every step after it inherits that closure. This file removes it: over a complete source with a basis of open subgroups at zero, a point of closure (f '' V 0) really is the image of a point of V 0.

Three ingredients meet here, and each supplies exactly one thing.

• The approximating sequence of TauCeti/Topology/Algebra/OpenMapping/Sequence.lean gives errors x n ∈ V n whose partial sums leave a residual in closure (f '' V (n + 1)).
• Completeness turns those errors into an actual sum: they tend to zero along the basis, and a null sequence in a complete nonarchimedean group is summable.
• Regularity of the target sends the residuals to zero. Continuity controls f '' V (n + 1) and never its closure, so it cannot do this alone; what does it is that a neighbourhood of zero in N contains the closure of a neighbourhood (hasBasis_nhds_closure).

The subgroups do the rest of the work: the sum of the errors stays inside V 0 because V 0 is a subgroup and, being a neighbourhood of zero, is closed.

Main results

• TauCeti.mem_image_of_mem_closure_image: closure (f '' V 0) ⊆ f '' V 0, in the presence of a basis of subgroups, completeness, and the neighbourhood hypothesis the Baire step supplies.

References

• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647.

theorem TauCeti.mem_image_of_mem_closure_image {M : Type u_1} {N : Type u_2} [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [CompleteSpace M] [AddGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [T0Space N] {F : Type u_3} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (hf : ContinuousAt (⇑f) 0) {V : ℕ → AddSubgroup M} (hV : (nhds 0).HasAntitoneBasis fun (n : ℕ) => ↑(V n)) (hVN : ∀ (n : ℕ), closure (⇑f '' ↑(V (n + 1))) ∈ nhds 0) {y : N} (hy : y ∈ closure (⇑f '' ↑(V 0))) : y ∈ ⇑f '' ↑(V 0)

Henkel's approximation converges. Let V be an antitone basis of subgroups at zero in a complete group M, let f : M → N be an additive map continuous at zero, and suppose each closure (f '' V (n + 1)) is a neighbourhood of zero — which is what the Baire step of Henkel's theorem provides. Then every point of closure (f '' V 0) is already the image of a point of V 0.

M is not assumed nonarchimedean: a basis of subgroups at zero is exactly that condition, and the proof reconstructs the instance from hV. N need not be commutative, and separation of it is used only to identify the two limits of the partial sums.