Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Factor elements act by mutually inverse permutations on reduced syllable words

Statement

For each iIi\in I and gGig\in G_i, left multiplication at the first syllable defines a permutation Pi,gP_{i,g} of the set of reduced words. One has Pi,g1=Pi,g1P_{i,g}^{-1}=P_{i,g^{-1}} and Pi,gh=Pi,gPi,hP_{i,gh}=P_{i,g}\circ P_{i,h}, so gPi,gg\mapsto P_{i,g} is a group homomorphism.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

For groups as in def-group, a syllable is a tagged pair (i,g)(i,g) with iIi\in I and gGi{ei}g\in G_i\setminus\{e_i\}. A reduced syllable word is a finite list of syllables, indexed by a natural length as in def-natural-numbers, in which adjacent tags differ. The empty list is allowed. At a concatenation seam, adjacent syllables from the same factor are multiplied and an identity result is deleted; this elementary reduction is repeated until the seam is reduced. (Reduced syllable words in a family of groups).

[L2]

For every set XX, the triple (Sym(X),,idX)(\operatorname{Sym}(X), \circ, \mathrm{id}_X) of def-symmetric-group is a group (def-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. (Sym(X)\operatorname{Sym}(X) is a group under composition, and it is non-abelian whenever XX has at least three distinct elements).

[L3]

Let (M,,e)(M,\cdot,e) and (M,,e)(M',\cdot',e') be monoids (def-semigroup-and-monoid). A monoid homomorphism from MM to MM' is a function f:MMf : M \to M' such that - (H1) f(xy)=f(x)f(y)f(x \cdot y) = f(x) \cdot' f(y) for all x,yMx, y \in M; - (H2) f(e)=ef(e) = e'. Let GG and GG' be groups (def-group). A group homomorphism from GG to GG' is a function f:GGf : G \to G' satisfying (H1) alone: f(xy)  =  f(x)f(y)for all x,yG.f(xy) \;=\; f(x)\, f(y) \qquad \text{for all } x, y \in G . Condition (H2) is not imposed for groups because it follows: a group homomorphism automatically satisfies f(e)=ef(e) = e' and f(x1)=f(x)1f(x^{-1}) = f(x)^{-1} (lem-group-homomorphism-basic-properties). For monoids it does not follow and must be assumed, which is why the two definitions differ. A homomorphism from a structure to itself is an endomorphism. The identity map of MM is a monoid homomorphism, and a composite of monoid homomorphisms is one, since (gf)(xy)=g(f(x)f(y))=g(f(x))g(f(y))(g \circ f)(xy) = g(f(x)f(y)) = g(f(x))\,g(f(y)) and (gf)(e)=g(e)=e(g \circ f)(e) = g(e') = e''; the same computation, without the second clause, shows a composite of group homomorphisms is a group homomorphism. (Monoid homomorphism and group homomorphism).

Proof

technique · direct
1.1

Define Pi,eiP_{i,e_i} to be the identity map, since (i,ei)(i,e_i) is not a syllable and prepending it would leave a word that is not reduced. For geig\ne e_i, define Pi,gP_{i,g} by prepending (i,g)(i,g) when the word is empty or begins in another factor; when it begins (i,h)(i,h), replace that syllable by (i,gh)(i,gh) and delete it if gh=eigh=e_i. Every value is again a reduced word.

givenL1L2L3
2.1

Let geig\ne e_i, so also g1eig^{-1}\ne e_i, and let ww be reduced. Three seam cases exhaust the definition. (a) ww empty or with first tag other than ii: Pi,g(w)=(i,g)wP_{i,g}(w)=(i,g)w, which begins (i,g)(i,g), so Pi,g1P_{i,g^{-1}} replaces that syllable by (i,g1g)=(i,ei)(i,g^{-1}g)=(i,e_i) and deletes it, returning ww. (b) w=(i,h)ww=(i,h)w' with gheigh\ne e_i: Pi,g(w)=(i,gh)wP_{i,g}(w)=(i,gh)w', and Pi,g1P_{i,g^{-1}} replaces (i,gh)(i,gh) by (i,g1gh)=(i,h)(i,g^{-1}gh)=(i,h), kept because heih\ne e_i, returning ww. (c) w=(i,h)ww=(i,h)w' with gh=eigh=e_i, that is h=g1h=g^{-1}: Pi,g(w)=wP_{i,g}(w)=w', and ww' is empty or has first tag other than ii because ww is reduced, so Pi,g1(w)=(i,g1)w=(i,h)w=wP_{i,g^{-1}}(w')=(i,g^{-1})w'=(i,h)w'=w. Exchanging gg and g1g^{-1} gives the other composite, so Pi,g1P_{i,g^{-1}} is a two-sided inverse of Pi,gP_{i,g}; with Pi,ei=idP_{i,e_i}=\mathrm{id} this makes every Pi,gP_{i,g} a permutation of the reduced words and Pi,g1=Pi,g1P_{i,g}^{-1}=P_{i,g^{-1}} [L2].

step 1.1L1L2
3.1

For Pi,gh=Pi,gPi,hP_{i,gh}=P_{i,g}\circ P_{i,h} both sides are immediate when g=eig=e_i or h=eih=e_i, so let g,heig,h\ne e_i and take ww reduced. (a) ww empty or with first tag other than ii: Pi,h(w)=(i,h)wP_{i,h}(w)=(i,h)w, and Pi,gP_{i,g} sends it to (i,gh)w(i,gh)w when gheigh\ne e_i and to ww when gh=eigh=e_i, which is Pi,gh(w)P_{i,gh}(w) in both subcases. (b) w=(i,a)ww=(i,a)w' with haeiha\ne e_i: Pi,h(w)=(i,ha)wP_{i,h}(w)=(i,ha)w', and Pi,gP_{i,g} sends it to (i,gha)w(i,gha)w' or, when gha=eigha=e_i, to ww'; Pi,gh(w)P_{i,gh}(w) splits on the same product (gh)a=gha(gh)a=gha and gives the same word. (c) w=(i,a)ww=(i,a)w' with ha=eiha=e_i: Pi,h(w)=wP_{i,h}(w)=w', empty or with first tag other than ii, so Pi,g(w)=(i,g)wP_{i,g}(w')=(i,g)w'; and gha=geigha=g\ne e_i, so Pi,ghP_{i,gh} replaces (i,a)(i,a) by (i,g)(i,g) and also gives (i,g)w(i,g)w'. Hence gPi,gg\mapsto P_{i,g} satisfies (H1) of [L3] into the symmetric group of [L2], and is a group homomorphism.

step 2.1L1L2L3

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 21 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