The commutative Tychonoff Wallace semigroup

The original Wallace interface records Hausdorffness, countable compactness, cancellation and a noninvertible element. The paper's printed corollary also says that the witness is commutative and Tychonoff. This module makes both properties part of the public proposition.

theorem Wallace.FullCharacterPackage.initial_t35Space {G : Type u_1} [AddCommGroup G] (C : FullCharacterPackage G) : T35Space G

The initial topology is Tychonoff (T₃.₅ in mathlib), since evaluation embeds the group into a product of circles.

theorem Wallace.SeparationPackage.initial_t35Space {I : Type u_1} (C : SeparationPackage I) : T35Space (I →₀ ℤ)

def Wallace.CommutativeTychonoffWallaceCounterexampleExists : Prop

The exact existential content of the paper's Wallace corollary. The algebraic structure is explicitly commutative and the separation property is explicitly Tychonoff.

Equations

• Wallace.CommutativeTychonoffWallaceCounterexampleExists = ∃ (S : Type) (topology : TopologicalSpace S) (monoid : AddCommMonoid S), T35Space S ∧ Wallace.IsWallaceSemigroup S

theorem Wallace.continuumPositiveCone_isCommutativeTychonoffWallace : ∃ (topology : TopologicalSpace ↥(positiveCone TriangularPreprocess.ContinuumIndex)), T35Space ↥(positiveCone TriangularPreprocess.ContinuumIndex) ∧ IsWallaceSemigroup ↥(positiveCone TriangularPreprocess.ContinuumIndex)

The concrete nonnegative cone, with all properties in the printed corollary visible.

theorem Wallace.commutativeTychonoffWallaceCounterexampleExists : CommutativeTychonoffWallaceCounterexampleExists

Formal counterpart of the paper's Wallace corollary. There exists a commutative Tychonoff countably compact topological semigroup with two-sided cancellation which is not a group. Wallace.Audit records the standard classical Lean foundations used by the proof.