Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Sym(X)\operatorname{Sym}(X) is a group under composition, and it is non-abelian whenever XX has at least three distinct elements

Statement

For every set XX, the triple (Sym(X),,idX)(\operatorname{Sym}(X), \circ, \mathrm{id}_X) of The symmetric group Sym(X)\operatorname{Sym}(X): the bijections of a set XX under composition is a group (Group and abelian group); the inverse of a permutation ff is its inverse function f1f^{-1}.

If XX contains three distinct elements aa, bb, cc, then Sym(X)\operatorname{Sym}(X) is not abelian: the transpositions τ=(ab)\tau = (a\,b) and ρ=(bc)\rho = (b\,c) satisfy τρρτ\tau \circ \rho \ne \rho \circ \tau.

Facts & Assumptions

Given: A set XX; Sym(X)\operatorname{Sym}(X) the set of bijections XXX \to X with the operation fgf \circ g defined by (fg)(x)=f(g(x))(f \circ g)(x) = f(g(x)) and the element idX\mathrm{id}_X (The symmetric group Sym(X)\operatorname{Sym}(X): the bijections of a set XX under composition); and, for the second claim, three distinct elements a,b,cXa, b, c \in X together with the transpositions τ=(ab)\tau = (a\,b) and ρ=(bc)\rho = (b\,c) of The symmetric group Sym(X)\operatorname{Sym}(X): the bijections of a set XX under composition.

[L1]

A composite of two bijections XXX \to X is a bijection XXX \to X, so \circ is a binary operation on Sym(X)\operatorname{Sym}(X); idX\mathrm{id}_X is a bijection; and a bijection ff has a two-sided inverse function f1f^{-1}, which is itself a bijection (Injection, surjection, bijection, The symmetric group Sym(X)\operatorname{Sym}(X): the bijections of a set XX under composition).

[L2]

Two functions XXX \to X are equal exactly when they agree at every point of XX.

[L3]

A group is a monoid in which every element is invertible; a monoid is an associative operation with a two-sided identity (Group and abelian group, Semigroup and monoid, Left inverse, right inverse, and invertible element of a monoid).

Proof

technique · direct
1.1

Composition is associative: for f,g,hSym(X)f, g, h \in \operatorname{Sym}(X) and xXx \in X, both ((fg)h)(x)((f \circ g) \circ h)(x) and (f(gh))(x)(f \circ (g \circ h))(x) evaluate to f(g(h(x)))f(g(h(x))), so the two composites agree at every point and are equal.

L2given
1.2

idX\mathrm{id}_X is a two-sided identity: for fSym(X)f \in \operatorname{Sym}(X) and xXx \in X, (fidX)(x)=f(x)(f \circ \mathrm{id}_X)(x) = f(x) and (idXf)(x)=f(x)(\mathrm{id}_X \circ f)(x) = f(x), so fidX=f=idXff \circ \mathrm{id}_X = f = \mathrm{id}_X \circ f.

L1L2given
1.3

Every fSym(X)f \in \operatorname{Sym}(X) is invertible in Sym(X)\operatorname{Sym}(X): the inverse function f1f^{-1} is again a bijection XXX \to X, hence lies in Sym(X)\operatorname{Sym}(X), and it satisfies f1(f(x))=xf^{-1}(f(x)) = x and f(f1(x))=xf(f^{-1}(x)) = x for every xx, that is f1f=idX=ff1f^{-1} \circ f = \mathrm{id}_X = f \circ f^{-1}.

L1L2
1.4

The transposition τ=(ab)\tau = (a\,b) satisfies τ(a)=b\tau(a) = b, τ(b)=a\tau(b) = a and τ(x)=x\tau(x) = x for x{a,b}x \notin \{a,b\}; the transposition ρ=(bc)\rho = (b\,c) satisfies ρ(b)=c\rho(b) = c, ρ(c)=b\rho(c) = b and ρ(x)=x\rho(x) = x for x{b,c}x \notin \{b,c\}. Both are bijections of XX, being their own inverses.

givenL1
2.1

By steps 1.1 and 1.2 the pair (Sym(X),)(\operatorname{Sym}(X), \circ) with the element idX\mathrm{id}_X is a monoid; by step 1.3 every element of it is invertible; hence it is a group, and the inverse of ff is the inverse function f1f^{-1}.

step 1.1step 1.2step 1.3L3
2.2

Evaluate the two composites at cc. Since cac \ne a and cbc \ne b, τ(c)=c\tau(c) = c, so (ρτ)(c)=ρ(τ(c))=ρ(c)=b(\rho \circ \tau)(c) = \rho(\tau(c)) = \rho(c) = b. And ρ(c)=b\rho(c) = b, so (τρ)(c)=τ(ρ(c))=τ(b)=a(\tau \circ \rho)(c) = \tau(\rho(c)) = \tau(b) = a.

step 1.4given
3.1

The two composites take different values at cc, because aba \ne b; hence τρρτ\tau \circ \rho \ne \rho \circ \tau and Sym(X)\operatorname{Sym}(X) is not abelian.

step 2.2L2given
4.1

Sym(X)\operatorname{Sym}(X) is a group under composition, and it fails to be abelian as soon as XX has three distinct elements.

step 2.1step 3.1

Remarks

  • "Three distinct elements", not a cardinality hypothesis. The second claim is stated and proved with three named, pairwise distinct points of XX. No notion of the size of XX is used, so the statement is available for any XX whatever, finite or not, and needs nothing about counting.

  • For XX with at most two elements Sym(X)\operatorname{Sym}(X) is abelian: it has at most two elements itself, and any group with at most two elements is abelian, since one of any two of its elements is then the identity.

  • The witness pair τ,ρ\tau, \rho is reused on the companion page to show that the exponent law (gh)n=gnhn(gh)^n = g^n h^n genuinely needs its commuting hypothesis.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 18 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources