The Wallace semigroup deduction

This file formalizes Section 9, the final deduction of the Wallace-semigroup corollary in the current paper under paper/.

The paper constructs a Hausdorff group topology on the free Abelian group and proves a free-ultrafilter subsequence limit property. Here that output is named HasWallaceLimitProperty. We prove from it that the nonnegative cone is Hausdorff, countably compact, cancellative on both sides, a topological semigroup, and not a group.

Every declaration in this file is proved from its explicitly stated hypotheses.

def Wallace.IsWallaceSemigroup (S : Type u) [TopologicalSpace S] [AddMonoid S] : Prop

The precise additive form of a Hausdorff Wallace semigroup.

The final conjunct says that the additive monoid has a noninvertible element, hence is not a group. An additive monoid is used rather than a bare semigroup because the counterexample in the paper is the nonnegative cone and contains zero.

Equations

• Wallace.IsWallaceSemigroup S = (ContinuousAdd S ∧ IsCancelAdd S ∧ T2Space S ∧ CountablyCompactSpace S ∧ ∃ (x : S), ¬IsAddUnit x)

def Wallace.HasInfiniteSetAccumulationProperty (X : Type u) [TopologicalSpace X] : Prop

A convenient unbundled form of the accumulation-point criterion used for countable compactness.

Equations

• Wallace.HasInfiniteSetAccumulationProperty X = ∀ (B : Set X), B.Infinite → ∃ (x : X), AccPt x (Filter.principal B)

theorem Wallace.countablyCompact_of_infiniteSet_accumulation {X : Type u} [TopologicalSpace X] [T1Space X] (hacc : HasInfiniteSetAccumulationProperty X) : CountablyCompactSpace X

In a T1 space, the accumulation-point property implies countable compactness.

This invokes mathlib's standard equivalence isCountablyCompact_iff_infinite_subset_has_accPt; it is not a custom compactness notion.

theorem Wallace.accPt_range_of_free_ultrafilter_limit {X : Type u} [TopologicalSpace X] {h : ℕ → X} {p : Ultrafilter ℕ} {x : X} (hinj : Function.Injective h) (hfree : ↑p ≤ Filter.cofinite) (htendsto : Filter.Tendsto h (↑p) (nhds x)) : AccPt x (Filter.principal (Set.range h))

An injective sequence converging along a free ultrafilter has its limit as an accumulation point of its range.

def Wallace.HasWallaceLimitProperty {F : Type u} [TopologicalSpace F] [AddZeroClass F] (P : AddSubmonoid F) : Prop

The exact part of the paper's construction used by the Wallace corollary.

Every injective sequence contained in P has a genuine subsequence (StrictMono φ) converging to a point of P along a free ultrafilter.

Equations

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

theorem Wallace.tendsto_subtype_of_tendsto {X : Type u} [TopologicalSpace X] {P : Set X} {p : Filter ℕ} {u : ℕ → X} {x : X} (hu : ∀ (n : ℕ), u n ∈ P) (hx : x ∈ P) (htendsto : Filter.Tendsto u p (nhds x)) : Filter.Tendsto (fun (n : ℕ) => ⟨u n, ⋯⟩) p (nhds ⟨x, hx⟩)

A limit in the ambient space is also a limit in a subspace when the sequence and its limit lie in that subspace.

theorem Wallace.infiniteSet_accumulation_of_wallaceLimitProperty {F : Type u} [TopologicalSpace F] [AddZeroClass F] (P : AddSubmonoid F) (hlimits : HasWallaceLimitProperty P) : HasInfiniteSetAccumulationProperty ↥P

The paper's free-ultrafilter limit property gives the accumulation-point property on the subspace P.

theorem Wallace.not_isAddUnit_of_neg_not_mem {F : Type u} [AddCommGroup F] (P : AddSubmonoid F) {a : F} (ha : a ∈ P) (hneg : -a ∉ P) : ¬IsAddUnit ⟨a, ha⟩

The algebraic witness a ∈ P, -a ∉ P is not an additive unit of the cone.

theorem Wallace.addSubmonoid_isWallace {F : Type u} [TopologicalSpace F] [AddCommGroup F] [ContinuousAdd F] [T2Space F] (P : AddSubmonoid F) (hcompact : CountablyCompactSpace ↥P) {a : F} (ha : a ∈ P) (hneg : -a ∉ P) : IsWallaceSemigroup ↥P

A countably compact additive submonoid P of a Hausdorff Abelian group with continuous addition is a Wallace semigroup whenever a ∈ P and -a ∉ P for some a.

theorem Wallace.addSubmonoid_isWallace_of_accumulation {F : Type u} [TopologicalSpace F] [AddCommGroup F] [ContinuousAdd F] [T2Space F] (P : AddSubmonoid F) (hacc : HasInfiniteSetAccumulationProperty ↥P) {a : F} (ha : a ∈ P) (hneg : -a ∉ P) : IsWallaceSemigroup ↥P

The Wallace conclusion from the exact accumulation-point hypothesis.

theorem Wallace.addSubmonoid_isWallace_of_limitProperty {F : Type u} [TopologicalSpace F] [AddCommGroup F] [ContinuousAdd F] [T2Space F] (P : AddSubmonoid F) (hlimits : HasWallaceLimitProperty P) {a : F} (ha : a ∈ P) (hneg : -a ∉ P) : IsWallaceSemigroup ↥P

The Wallace conclusion from the free-ultrafilter limit property proved in the paper.

def Wallace.positiveCone (ι : Type u) : AddSubmonoid (ι →₀ ℤ)

The coordinatewise nonnegative cone in the free Abelian group ι →₀ ℤ.

Equations

• Wallace.positiveCone ι = { carrier := {x : ι →₀ ℤ | ∀ (i : ι), 0 ≤ x i}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem Wallace.single_one_mem_positiveCone (ι : Type u) (i : ι) : Finsupp.single i 1 ∈ positiveCone ι

theorem Wallace.neg_single_one_not_mem_positiveCone (ι : Type u) (i : ι) : -Finsupp.single i 1 ∉ positiveCone ι

theorem Wallace.positiveCone_isWallace_of_limitProperty (ι : Type u) [TopologicalSpace (ι →₀ ℤ)] [IsTopologicalAddGroup (ι →₀ ℤ)] [T2Space (ι →₀ ℤ)] (i : ι) (hlimits : HasWallaceLimitProperty (positiveCone ι)) : IsWallaceSemigroup ↥(positiveCone ι)

The formalized Wallace deduction for a free Abelian group: if the topology has the exact free-ultrafilter limit property constructed by the paper, its nonnegative cone is a Wallace semigroup.