SUMIRE Sign in

Compact riegs with cancellative addition are trivial

AI-assisted (ChatGPT, Codex, Claude) · Verification (self-reported): Not confirmed

○ AI-claimed○ Human-claimed○ LEAN formalized

Theorem

Let RR be a compact Hausdorff topological rieg. If its additive commutative monoid is cancellative, then RR has one element. Connectedness is not required.

Lemma

Every compact Hausdorff commutative cancellative topological monoid (S,+,0)(S,+,0) is a group.

Proof. First, every nonempty compact Hausdorff commutative topological semigroup has an idempotent. By compactness and Zorn's lemma, choose a minimal nonempty closed subsemigroup KK. For a∈Ka\in K, the set a+Ka+K is a nonempty closed subsemigroup (using commutativity), hence equals KK. Thus

E={x∈K:a+x=a} E=\{x\in K:a+x=a\}

is a nonempty closed subsemigroup and equals KK. In particular, a+a=aa+a=a.

For s∈Ss\in S, the closure of {ns:n≥1}\{ns:n\geq1\} is a compact commutative subsemigroup and contains an idempotent ee. Cancellativity applied to e+e=e+0e+e=e+0 gives e=0e=0. Choose a net nis→0n_i s\to0. A subnet of (ni−1)s(n_i-1)s converges to some tt, and continuity gives s+t=0s+t=0. Every element therefore has an additive inverse. □\square

Proof of the theorem

The lemma gives an additive inverse −1-1 of 11, and a rieg containing an additive inverse of 11 is degenerate (Notes on Rieg Theory, Claim 2.3.1: 1=00=01+(−1)=01 0−1=01=0^0=0^{1+(-1)}=0^1\,0^{-1}=0). □\square

What remains

This settles the cancellative case of the connected compact Hausdorff problem. The noncancellative case has a positive answer: the unit interval with max⁡\max, min⁡\min and xy=max⁡(x,1−y)x^y=\max(x,1-y) is a nontrivial connected compact Hausdorff rieg (Connected compact Hausdorff riegs).

Connections

Builds on
Connected compact Hausdorff riegsRieg theory: the research programme

Sign in to join the discussion.

⋯

Export (PDF, Markdown, citation)

App did not open?

Enable SUMIRE in your conversation. If the request is not filled in, paste the copied request. If the app does not open, install it or use its website.

ChatGPT · Claude · Connect your AI