Lifting a convergent family along a surjection

A family g : ι → N converges to n₀ along the cofinite filter when all but finitely many of its members lie in any given neighbourhood of n₀. This file shows that a surjection which carries the neighbourhood filter of m₀ into that of n₀ lifts such a family to one converging to m₀: the lift can be chosen convergent, not merely made to exist.

Openness is not the hypothesis, and would not suffice on its own. IsOpenMap φ puts the image of a neighbourhood of m₀ around φ m₀, which is a neighbourhood of n₀ only when φ m₀ = n₀. The hypothesis used here is 𝓝 n₀ ≤ Filter.map φ (𝓝 m₀), which is exactly what the proof consumes; a zero-preserving open surjection — an A-linear map, say — is one way to supply it, and that is the form TauCeti.Huber uses it in.

That the lifts exist pointwise is only surjectivity. The content is that they can be chosen uniformly enough to still converge, and this genuinely needs a construction: choosing a preimage of g α for each α independently can leave the lifts spread out even when the g α collapse to n₀. The fix is to choose the preimage of g α from a neighbourhood whose index grows with α, so that convergence is forced by the choice rather than hoped for.

Main results

• exists_lift_tendsto_cofinite_nhds: the lifting statement.

Implementation notes

Countability of 𝓝 m₀ enters only through Filter.exists_antitone_basis, which supplies the antitone basis the lifts are drawn from. It is taken as an instance rather than as a basis in the statement, so a caller neither has to produce a basis nor to re-prove the image condition index by index: 𝓝 n₀ ≤ Filter.map φ (𝓝 m₀) gives the latter uniformly.

The index of the neighbourhood a lift is drawn from is Nat.findGreatest (fun m ↦ g α ∈ φ '' V m) (r α), where r is an injection of ι into ℕ — one exists because ι is countable, and it tends to infinity cofinitely because cofinite is atTop on ℕ. The cap by r α is what makes the definition total. Without it the natural index is the largest m with g α ∈ φ '' V m, and no largest one need exist: the set of such m can be empty, which is the common case, and it can equally be unbounded, when g α lies in every φ '' V m. Nat.findGreatest returns a usable index in both cases, so capping removes them rather than splitting on them.

No algebraic structure is used: M and N carry only a topology and a distinguished point. In particular the neighbourhoods drawn from are not assumed to be subgroups, which the argument would need if it ever added two lifts — it never does, choosing each independently. Nothing about m₀ and n₀ is used beyond their neighbourhood filters — no zero, and no algebra.

theorem TauCeti.exists_lift_tendsto_cofinite_nhds {ι : Type u_1} [Countable ι] {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] {m₀ : M} {n₀ : N} [(nhds m₀).IsCountablyGenerated] (φ : M → N) (hsurj : Function.Surjective φ) (hmap : nhds n₀ ≤ Filter.map φ (nhds m₀)) (g : ι → N) (hg : Filter.Tendsto g Filter.cofinite (nhds n₀)) : ∃ (f : ι → M), (∀ (α : ι), φ (f α) = g α) ∧ Filter.Tendsto f Filter.cofinite (nhds m₀)

A convergent family lifts to a convergent family. If φ is surjective and carries the neighbourhood filter of m₀ into that of n₀, then any family tending to n₀ cofinitely has a φ-preimage family tending to m₀ cofinitely.

Pointwise lifting is surjectivity alone; the statement is that a single choice of lifts can be made to converge. Note that IsOpenMap φ supplies the filter hypothesis only together with φ m₀ = n₀; openness by itself places the images around φ m₀, not around n₀.

Two countability hypotheses are essential, and both are instance arguments rather than explicit ones. [(𝓝 m₀).IsCountablyGenerated] is what produces the antitone basis the lifts are drawn from, and [Countable ι] — from the variable block — is what supplies the injection ι ↪ ℕ that caps the construction. Neither is bookkeeping: without the first there is no sequence of neighbourhoods to index, and without the second the cap has nothing to grow along.