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.
The finite Heisenberg group is the unique Sylow -subgroup of its coordinate upper-triangular group
Example
Let with , and let act by diagonal coordinate scaling. In the coordinate upper-triangular group , the subgroup is the unique Sylow -subgroup. See The external direct product with componentwise multiplication.
Facts & Assumptions
Given: The hypotheses and objects in the Example.
Let and be groups. Their external direct product has underlying set and componentwise operation The fact that this operation makes a group, with the indicated identity and inverses, is proved in thm-external-direct-product-is-a-group. Until that result is used, this definition introduces only the set and its componentwise binary operation. (The external direct product with componentwise multiplication).
For groups and , the componentwise operation of def-external-direct-product-of-groups makes a group. Its identity is , and Moreover the coordinate maps and are group homomorphisms. ( is a group with identity , coordinatewise inverses, and homomorphic coordinate projections).
An action of a group on a group by automorphisms is a homomorphism Here automorphisms are those of def-group-isomorphism-and-automorphism. Writing , this means that every is an automorphism of , , and . Equivalently, by thm-group-actions-correspond-to-homomorphisms, it is a group action (def-group-action) on the underlying set of for which every acting permutation is an automorphism. (An action of a group on a group by automorphisms).
For an action , the external semidirect product is with multiplication ( The external semidirect product ).
Let be an action by automorphisms. The multiplication makes a group with identity and inverse . ( The semidirect-product multiplication makes a group).
In , the canonical copies and are subgroups, is normal, their intersection is trivial, every element has a unique factorization , and (The canonical copy of is normal, the canonical copy of is a complement, and conjugation induces the action).
A Sylow -subgroup of a finite group is normal if and only if it is the unique Sylow -subgroup. (A Sylow -subgroup is normal if and only if it is unique).
For every prime , the operations of addition and multiplication on make it a field (def-field). (For every prime , the two operations on make it a field).
Let be a positive integer. Every class in (def-integers-modulo-n) contains exactly one integer with . Consequently the map is a bijection from the von Neumann natural to , and . This includes , where the only representative is . For , the map is a bijection . (For , every class in has one representative with , so ; while is in bijection with ).
For , the unit group is and Euler's totient is . (The unit group and Euler's totient for ).
Euler's totient satisfies . If is prime (def-prime), then . (, and for every prime ).
- If and are finite then is finite and (def-finite-cardinality). 2. Let and let be finite sets. Write Then is finite and , the right-hand product being the -valued one of def-nat-finite-sum-and-product. (The product rule: , and ).
Verification
In , expanding both triple products gives the same third coordinate ; hence the operation is associative, with identity and inverse .
For , the scaling factors on are , , and . This identity preserves the cross term , so the scaling is an automorphism, and coordinate multiplication makes a homomorphism.
The semidirect product is therefore defined, and its canonical copy of is normal.
Since and , has the full -part of ; normality makes it the unique Sylow -subgroup. For , is trivial and . This proves the stated claim.
Depends on
- The external direct product $G\times H$ with componentwise multiplication
- $G\times H$ is a group with identity $(e_G,e_H)$, coordinatewise inverses, and homomorphic coordinate projections
- An action of a group $H$ on a group $N$ by automorphisms
- The external semidirect product $N\rtimes_\alpha H$
- The semidirect-product multiplication makes $N\times H$ a group
- The canonical copy of $N$ is normal, the canonical copy of $H$ is a complement, and conjugation induces the action
- A Sylow $p$-subgroup is normal if and only if it is unique
- For every prime $p$, the two operations on $\mathbb{Z}/p$ make it a field
- For $n\ge 1$, every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$, so $\lvert\mathbb{Z}/n\rvert=n$; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$
- The unit group $(\mathbb{Z}/n)^\times$ and Euler's totient $\varphi(n)=\lvert(\mathbb{Z}/n)^\times\rvert$ for $n\ge1$
- $\varphi(1)=1$, and $\varphi(p)=p-1$ for every prime $p$
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 114 results over 22 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
- Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)