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 and , left multiplication at the first syllable defines a permutation of the set of reduced words. One has and , so is a group homomorphism.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
For groups as in def-group, a syllable is a tagged pair with and . 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).
For every set , the triple of def-symmetric-group is a group (def-group); the inverse of a permutation is its inverse function . If contains three distinct elements , , , then is not abelian: the transpositions and satisfy . ( is a group under composition, and it is non-abelian whenever has at least three distinct elements).
Let and be monoids (def-semigroup-and-monoid). A monoid homomorphism from to is a function such that - (H1) for all ; - (H2) . Let and be groups (def-group). A group homomorphism from to is a function satisfying (H1) alone: Condition (H2) is not imposed for groups because it follows: a group homomorphism automatically satisfies and (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 is a monoid homomorphism, and a composite of monoid homomorphisms is one, since and ; the same computation, without the second clause, shows a composite of group homomorphisms is a group homomorphism. (Monoid homomorphism and group homomorphism).
Proof
Define to be the identity map, since is not a syllable and prepending it would leave a word that is not reduced. For , define by prepending when the word is empty or begins in another factor; when it begins , replace that syllable by and delete it if . Every value is again a reduced word.
Let , so also , and let be reduced. Three seam cases exhaust the definition. (a) empty or with first tag other than : , which begins , so replaces that syllable by and deletes it, returning . (b) with : , and replaces by , kept because , returning . (c) with , that is : , and is empty or has first tag other than because is reduced, so . Exchanging and gives the other composite, so is a two-sided inverse of ; with this makes every a permutation of the reduced words and [L2].
For both sides are immediate when or , so let and take reduced. (a) empty or with first tag other than : , and sends it to when and to when , which is in both subcases. (b) with : , and sends it to or, when , to ; splits on the same product and gives the same word. (c) with : , empty or with first tag other than , so ; and , so replaces by and also gives . Hence satisfies (H1) of [L3] into the symmetric group of [L2], and is a group homomorphism.
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
- George D. Torres, Combinatorial Group Theory, §2 (standard reference, not scraped)
- B. H. Neumann, Lectures on Topics in the Theory of Infinite Groups, Ch. 9 (standard reference, not scraped)