Minimal construction interface for the Wallace counterexample

The construction supplies characters compatible with all prescribed ultrafilter limits and separating the points of the free group. For the Wallace corollary it is enough that, for every nonzero element x, one compatible character does not annihilate x. This file isolates precisely that output.

No topology on the free Abelian group and no compactness conclusion is stored in SeparationPackage; both are derived below from its algebraic and filter-theoretic fields.

def Wallace.InjectiveSequence' (G : Type u) : Type u

An injective sequence bundled with the proof of injectivity.

Equations

• Wallace.InjectiveSequence' G = { s : ℕ → G // Function.Injective s }

structure Wallace.SeparationPackage (I : Type u) : Type (u + 1)

The minimal post-fusion data needed for Wallace's problem.

The difficult construction must supply the coding, the prepared subsequences and free ultrafilters, and a compatible separating character for every nonzero element. The structure does not assume any topology or compactness property of the free Abelian group.

• Code : Type u

  Codes for injective sequences in the free Abelian group.

• codeEquiv : self.Code ≃ InjectiveSequence' (I →₀ ℤ)

  The identification of codes with injective sequences.

• codeIndex : self.Code → I

  The distinguished coordinate assigned to each code.

• subsequence : self.Code → ℕ → ℕ

  The selected subsequence of the sequence represented by each code.

• subsequence_strictMono (c : self.Code) : StrictMono (self.subsequence c)
• ultrafilter : self.Code → Ultrafilter ℕ

  The free ultrafilter along which the selected subsequence converges.

• ultrafilter_free (c : self.Code) : ↑(self.ultrafilter c) ≤ Filter.cofinite
• character : { x : I →₀ ℤ // x ≠ 0 } → (I →₀ ℤ) →+ UnitAddCircle

  A circle-valued character separating each nonzero group element.

• character_self_ne_zero (x : { x : I →₀ ℤ // x ≠ 0 }) : (self.character x) ↑x ≠ 0
• character_limit (c : self.Code) (x : { x : I →₀ ℤ // x ≠ 0 }) : Filter.Tendsto (fun (n : ℕ) => (self.character x) (↑(self.codeEquiv c) (self.subsequence c n))) (↑(self.ultrafilter c)) (nhds ((self.character x) (Finsupp.single (self.codeIndex c) 1)))

noncomputable def Wallace.SeparationPackage.evaluation {I : Type u} (C : SeparationPackage I) : (I →₀ ℤ) →+ { x : I →₀ ℤ // x ≠ 0 } → UnitAddCircle

Simultaneous evaluation by all compatible separating characters.

Equations

• C.evaluation = { toFun := fun (y : I →₀ ℤ) (x : { x : I →₀ ℤ // x ≠ 0 }) => (C.character x) y, map_zero' := ⋯, map_add' := ⋯ }

@[reducible]

noncomputable def Wallace.SeparationPackage.initialTopology {I : Type u} (C : SeparationPackage I) : TopologicalSpace (I →₀ ℤ)

The initial topology induced by the compatible separating characters.

Equations

• C.initialTopology = TopologicalSpace.induced (⇑C.evaluation) inferInstance

theorem Wallace.SeparationPackage.evaluation_injective {I : Type u} (C : SeparationPackage I) : Function.Injective ⇑C.evaluation

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

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

theorem Wallace.SeparationPackage.prepared_tendsto_basis {I : Type u} (C : SeparationPackage I) (c : C.Code) : Filter.Tendsto (fun (n : ℕ) => ↑(C.codeEquiv c) (C.subsequence c n)) (↑(C.ultrafilter c)) (nhds (Finsupp.single (C.codeIndex c) 1))

The prepared subsequence converges to its prescribed basis point in the initial topology.

theorem Wallace.SeparationPackage.positiveCone_hasWallaceLimitProperty {I : Type u} (C : SeparationPackage I) : HasWallaceLimitProperty (positiveCone I)

The package supplies the exact free-ultrafilter limit property used by the cone argument.