Steps toward Henkel's open mapping theorem #
Henkel's open mapping theorem says that a continuous surjective linear map between complete Hausdorff first-countable modules over a ring with a zero sequence of units is open. Its first half is a Baire-category argument, and this file collects the steps up to and including the one that consumes it. None of them needs the hypotheses the end of the proof needs — no completeness, no first countability, not even continuity of the map.
The Baire results below need a Baire target and an equivariant map, the latter being what lets a dilate pass through it. The approximation step at the end needs neither: it asks nothing of the map beyond being a function.
The argument is the classical one, with the zero sequence of units supplying the countability
Baire needs. Any neighbourhood U of zero in the domain has its dilates uₙ⁻¹ • U cover the
domain, indexed by ℕ (TauCeti.iUnion_inv_smul_eq_univ_of_tendsto_zero); a surjection carries
that cover to a cover of the target by the corresponding dilates of f '' U; Baire forces one of
their closures to have interior; and dilating back by a unit — a homeomorphism of the target —
moves that interior onto closure (f '' U) itself.
The interior is then upgraded to a neighbourhood of zero in the usual way: a difference D - D
of the closure with itself absorbs a translate of that interior, and D - D stays inside a
closure by TauCeti.closure_sub_closure_subset. Choosing the neighbourhood symmetric — which
Mathlib's exists_closed_nhds_zero_neg_eq_add_subset does in one step — turns that difference
back into the image of U.
What this does not give is that f '' U itself is a neighbourhood of zero, only its closure.
Removing that closure is the last step of Henkel's proof and is where completeness and first
countability enter; it is not proved here.
Main results #
TauCeti.nonempty_interior_closure_of_iUnion_smul: if countably many dilates of a set by a group acting continuously cover a Baire space, then the closure of that set has nonempty interior. This is the Baire argument by itself, with no map in sight.TauCeti.nonempty_interior_closure_image_of_tendsto_zero: the form Henkel's proof uses — along a zero sequence of units, the closure of the image of any neighbourhood of zero under a surjective equivariant map has nonempty interior.TauCeti.closure_image_mem_nhds_zero_of_tendsto_zero: that interior upgraded — the closure of the image of a neighbourhood of zero is a neighbourhood of zero.TauCeti.HasZeroSequenceOfUnits.nonempty_interior_closure_imageandTauCeti.HasZeroSequenceOfUnits.closure_image_mem_nhds_zero: the same two, taking the sequence from the class rather than from the caller.TauCeti.exists_mem_and_sub_mem_closure_image: one step of the approximation that consumes that neighbourhood — a point in the closure off '' Uis brought insideclosure (f '' V)by subtracting the image of somex ∈ U.
References #
- L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647. The Baire argument formalised here is the opening of its proof.
- Wedhorn, Adic Spaces, Theorem 6.16 and Propositions 6.17–6.18, which are proved from Henkel's theorem; downstream context for this file rather than its source.
The Baire step, on its own: if countably many dilates of V by elements of a group acting
continuously cover a Baire space, then closure V has nonempty interior.
Invertibility of the scalars is what makes the conclusion about V rather than about one dilate:
x ↦ g • x is then a homeomorphism, so it carries interior to interior and commutes with closure.
Countability of the index is the whole reason Henkel's hypothesis is a sequence of units — a
cover indexed by all of Aˣ would exhaust the space just as well but could not start a Baire
argument. Nothing else about either parameter is used, so the group is arbitrary and the index is
an arbitrary countable type; the caller below supplies Aˣ and ℕ.
The Baire step in the form Henkel's proof uses. Along a zero sequence of units, the closure of the image of a neighbourhood of zero under a surjective equivariant map has nonempty interior.
Besides the equivariance carried by MulActionHomClass — which is what lets a dilate pass
through the map — surjectivity is the only property used: together they turn the countable cover
of the domain by uₙ⁻¹ • U into a countable cover of the target. Continuity of the map is not
needed here and is not assumed; it enters Henkel's proof only afterwards.
The hypothesis hc is the one carried by
TauCeti.iUnion_inv_smul_eq_univ_of_tendsto_zero: continuity of the action in the scalar alone,
at zero, at every vector. ContinuousSMul A M implies it and is strictly stronger.
The Baire step under the class hypothesis. The same conclusion as
TauCeti.nonempty_interior_closure_image_of_tendsto_zero, with the zero sequence taken from
TauCeti.HasZeroSequenceOfUnits instead of supplied by the caller. This is the form a downstream
open mapping theorem wants, since the roadmap states Henkel's hypothesis as the class.
The closure of the image of a neighbourhood of zero is a neighbourhood of zero. This is
the strongest statement about f available without completeness or first countability; removing
the closure needs both and is not done here.
Additivity of f is used here and by none of the results above, which is why this and its
class-level companion carry the additive hypotheses on M and N and those do not.
The neighbourhood step under the class hypothesis. The same conclusion as
TauCeti.closure_image_mem_nhds_zero_of_tendsto_zero, with the zero sequence taken from
TauCeti.HasZeroSequenceOfUnits instead of supplied by the caller.
One step of Henkel's approximation. If y lies in the closure of f '' U, and the closure
of f '' V is a neighbourhood of zero, then some x ∈ U brings y within that closure: the
residual y - f x lies in closure (f '' V).
This is what turns the neighbourhood statement above into a construction. Iterating it down a
decreasing sequence of Vs produces a sequence of approximants whose residuals shrink, and it is
the convergence of the resulting series — where completeness and first countability enter — that
finally removes the closure from f '' U. Neither of those hypotheses is needed here.
Nothing is asked of f beyond being a function, and nothing of M at all: the step is about
closures and images, and it is the iteration that needs f additive and M complete.