Excluding nontrivial convergent sequences

The separating package constructed for the Wallace semigroup has a stronger consequence than point separation. Every injective sequence has a genuine subsequence which converges, along a free ultrafilter, to a nonzero basis vector. In a Hausdorff topological group this rules out convergence of the original injective sequence: after translation by its alleged limit, the same subsequence would converge to zero along the free ultrafilter.

This observation avoids any separate oscillating-marker construction.

def Wallace.HasNonzeroLimitProperty (G : Type u) [TopologicalSpace G] [Zero G] : Prop

Every injective sequence has a strictly reindexed subsequence with a nonzero limit along a free ultrafilter.

Equations

• One or more equations did not get rendered due to their size.

theorem Wallace.SeparationPackage.hasNonzeroLimitProperty {I : Type u} (C : SeparationPackage I) : HasNonzeroLimitProperty (I →₀ ℤ)

A separation package has the nonzero ultrafilter-limit property: its prescribed limit is the fresh basis vector attached to the code of the sequence.

theorem Wallace.no_injective_sequence_converges_of_nonzeroLimitProperty {G : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [T2Space G] (hlimits : HasNonzeroLimitProperty G) (s : ℕ → G) : Function.Injective s → ¬∃ (x : G), Filter.Tendsto s Filter.atTop (nhds x)

In a Hausdorff topological group, the nonzero ultrafilter-limit property prevents every injective sequence from converging.

theorem Wallace.exists_injective_subsequence_of_infinite_range {X : Type u} {s : ℕ → X} (hinf : (Set.range s).Infinite) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Function.Injective (s ∘ φ)

Any sequence with infinite range has a strictly reindexed injective subsequence.

theorem Wallace.eventually_eq_limit_of_no_injective_sequence_converges {X : Type u} [TopologicalSpace X] [T1Space X] (hno : ∀ (s : ℕ → X), Function.Injective s → ¬∃ (x : X), Filter.Tendsto s Filter.atTop (nhds x)) {s : ℕ → X} {x : X} (hs : Filter.Tendsto s Filter.atTop (nhds x)) : ∀ᶠ (n : ℕ) in Filter.atTop, s n = x

In a T1 space where no injective sequence converges, every convergent sequence is eventually equal to its limit.