Full topological consequences of the character construction

This file isolates the exact output needed to obtain the group theorem, rather than only its nonnegative-cone consequence. A FullCharacterPackage codes every injective sequence, assigns it a genuine subsequence and a free ultrafilter, and supplies a point-separating family of circle-valued characters for which that subsequence has a prescribed nonzero limit.

The initial topology of such a package is Hausdorff, is a group topology, is countably compact, and has no non-eventually-constant convergent sequences. Its canonical induced uniformity is totally bounded, which is the uniform formulation of precompactness used here.

Countable compactness from the nonzero-limit property

theorem Wallace.infiniteSet_accumulation_of_nonzero_ultrafilter_limits {X : Type u} [TopologicalSpace X] [Zero X] (hlimits : HasNonzeroLimitProperty X) : HasInfiniteSetAccumulationProperty X

The nonzero ultrafilter-limit property gives an accumulation point for every infinite set.

theorem Wallace.countablyCompact_of_nonzero_ultrafilter_limits {X : Type u} [TopologicalSpace X] [Zero X] [T1Space X] (hlimits : HasNonzeroLimitProperty X) : CountablyCompactSpace X

In a T₁ space, the package's ultrafilter limits imply countable compactness.

A group-independent character package

structure Wallace.FullCharacterPackage (G : Type u) [AddCommGroup G] : Type (max u (v + 1))

The exact character data from which all conclusions of the group theorem follow. This interface applies without change to free Abelian groups and rational vector groups.

• Code : Type v

  Codes for injective sequences in G.

• codeEquiv : self.Code ≃ InjectiveSequence' G

  The identification of codes with injective sequences.

• 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
• limitPoint : self.Code → G

  The prescribed nonzero limit of the selected subsequence.

• limitPoint_ne_zero (c : self.Code) : self.limitPoint c ≠ 0
• CharacterIndex : Type v

  Indices for the separating family of circle-valued characters.

• character : self.CharacterIndex → G →+ UnitAddCircle

  The separating family of circle-valued additive characters.

• character_detects (x : G) : x ≠ 0 → ∃ (j : self.CharacterIndex), (self.character j) x ≠ 0
• character_limit (c : self.Code) (j : self.CharacterIndex) : Filter.Tendsto (fun (n : ℕ) => (self.character j) (↑(self.codeEquiv c) (self.subsequence c n))) (↑(self.ultrafilter c)) (nhds ((self.character j) (self.limitPoint c)))

def Wallace.FullCharacterPackage.evaluation {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : G →+ C.CharacterIndex → UnitAddCircle

Simultaneous evaluation by all characters in the package.

Equations

• C.evaluation = { toFun := fun (x : G) (j : C.CharacterIndex) => (C.character j) x, map_zero' := ⋯, map_add' := ⋯ }

@[reducible]

def Wallace.FullCharacterPackage.initialTopology {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : TopologicalSpace G

The initial topology generated by the package's characters.

Equations

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

@[reducible]

noncomputable def Wallace.FullCharacterPackage.initialUniformSpace {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : UniformSpace G

The uniformity pulled back from the compact power of the circle.

Equations

• C.initialUniformSpace = UniformSpace.comap (⇑C.evaluation) inferInstance

theorem Wallace.FullCharacterPackage.initialUniformSpace_toTopology {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : C.initialUniformSpace.toTopologicalSpace = C.initialTopology

theorem Wallace.FullCharacterPackage.initial_isUniformAddGroup {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : IsUniformAddGroup G

The pulled-back uniformity is the canonical uniform group structure induced by the diagonal homomorphism.

theorem Wallace.FullCharacterPackage.evaluation_injective {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : Function.Injective ⇑C.evaluation

theorem Wallace.FullCharacterPackage.initial_isTopologicalAddGroup {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : IsTopologicalAddGroup G

theorem Wallace.FullCharacterPackage.initial_t2Space {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : T2Space G

theorem Wallace.FullCharacterPackage.prepared_tendsto_limitPoint {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) (c : C.Code) : Filter.Tendsto (fun (n : ℕ) => ↑(C.codeEquiv c) (C.subsequence c n)) (↑(C.ultrafilter c)) (nhds (C.limitPoint c))

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

theorem Wallace.FullCharacterPackage.hasNonzeroLimitProperty {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : HasNonzeroLimitProperty G

theorem Wallace.FullCharacterPackage.initial_countablyCompactSpace {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : CountablyCompactSpace G

theorem Wallace.FullCharacterPackage.initial_noInjectiveConvergentSequences {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) (s : ℕ → G) : Function.Injective s → ¬∃ (x : G), Filter.Tendsto s Filter.atTop (nhds x)

theorem Wallace.FullCharacterPackage.initial_onlyEventuallyConstantConvergentSequences {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) (s : ℕ → G) (x : G) : Filter.Tendsto s Filter.atTop (nhds x) → ∀ᶠ (n : ℕ) in Filter.atTop, s n = x

theorem Wallace.FullCharacterPackage.initial_totallyBounded {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : TotallyBounded Set.univ

The induced uniformity is totally bounded because the target is a compact power of the circle.

The package already constructed for the free Abelian group

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

Regard the existing free-Abelian separation package as a full character package.

Equations

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

theorem Wallace.SeparationPackage.full_initialTopology_eq {I : Type u} (C : SeparationPackage I) : C.toFullCharacterPackage.initialTopology = C.initialTopology

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

theorem Wallace.SeparationPackage.initial_noInjectiveConvergentSequences {I : Type u} (C : SeparationPackage I) (s : ℕ → I →₀ ℤ) : Function.Injective s → ¬∃ (x : I →₀ ℤ), Filter.Tendsto s Filter.atTop (nhds x)

theorem Wallace.SeparationPackage.initial_onlyEventuallyConstantConvergentSequences {I : Type u} (C : SeparationPackage I) (s : ℕ → I →₀ ℤ) (x : I →₀ ℤ) : Filter.Tendsto s Filter.atTop (nhds x) → ∀ᶠ (n : ℕ) in Filter.atTop, s n = x

@[reducible]

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

The uniform structure induced by all characters in the separation package.

Equations

• C.initialUniformSpace = C.toFullCharacterPackage.initialUniformSpace

theorem Wallace.SeparationPackage.initialUniformSpace_toTopology {I : Type u} (C : SeparationPackage I) : C.initialUniformSpace.toTopologicalSpace = C.initialTopology

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

theorem Wallace.SeparationPackage.initial_totallyBounded {I : Type u} (C : SeparationPackage I) : TotallyBounded Set.univ

Publication-level theorem interfaces

def Wallace.HasMainGroupTopology (G : Type u) [AddCommGroup G] : Prop

The exact topological conclusion shared by the free-Abelian and rational-vector-group results. Total boundedness is stated for a compatible uniformity inducing the displayed topology.

Equations

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

theorem Wallace.FullCharacterPackage.hasMainGroupTopology {G : Type u} [AddCommGroup G] (C : FullCharacterPackage G) : HasMainGroupTopology G

A full character package proves the complete group-topology conclusion.

@[reducible, inline]

abbrev Wallace.RationalVectorGroupConclusion (I : Type u) : Prop

Exact statement of the rational-vector-group proposition for an arbitrary index type.

Equations

• Wallace.RationalVectorGroupConclusion I = Wallace.HasMainGroupTopology (I →₀ ℚ)

theorem Wallace.FullCharacterPackage.rationalVectorGroupConclusion {I : Type u} (C : FullCharacterPackage (I →₀ ℚ)) : RationalVectorGroupConclusion I

Once the construction is instantiated on the rational direct sum, the rational proposition follows through exactly the same topology argument.