Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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 p-subgroup of its coordinate upper-triangular group

Example

Let Hp=Fp3 with (a,b,c)(a,b,c)=(a+a,b+b,c+c+ab), and let D=(Fp×)3 act by diagonal coordinate scaling. In the coordinate upper-triangular group Bp=HpD, the subgroup Hp is the unique Sylow p-subgroup. See The external direct product G×H with componentwise multiplication.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

Let G and H be groups. Their external direct product has underlying set G×H:={(g,h):gG, hH} and componentwise operation (g,h)(g,h):=(gg,hh). The fact that this operation makes G×H 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 G×H with componentwise multiplication).

[L2]

For groups G and H, the componentwise operation of def-external-direct-product-of-groups makes G×H a group. Its identity is (eG,eH), and (g,h)1=(g1,h1). Moreover the coordinate maps πG(g,h)=g and πH(g,h)=h are group homomorphisms. (G×H is a group with identity (eG,eH), coordinatewise inverses, and homomorphic coordinate projections).

[L3]

An action of a group H on a group N by automorphisms is a homomorphism α:HAut(N). Here automorphisms are those of def-group-isomorphism-and-automorphism. Writing αh=α(h), this means that every αh is an automorphism of N, αhk=αhαk, and α1=idN. Equivalently, by thm-group-actions-correspond-to-homomorphisms, it is a group action (def-group-action) on the underlying set of N for which every acting permutation is an automorphism. (An action of a group H on a group N by automorphisms).

[L4]

For an action α:HAut(N), the external semidirect product NαH is N×H with multiplication (n,h)(n,h)=(nαh(n),hh). ( The external semidirect product NαH).

[L5]

Let α:HAut(N) be an action by automorphisms. The multiplication (n,h)(n,h)=(nαh(n),hh) makes N×H a group with identity (1N,1H) and inverse (n,h)1=(αh1(n1),h1).. ( The semidirect-product multiplication makes N×H a group).

[L6]

In NαH, the canonical copies Nˉ={(n,1):nN} and Hˉ={(1,h):hH} are subgroups, Nˉ is normal, their intersection is trivial, every element has a unique factorization (n,1)(1,h), and (1,h)(n,1)(1,h)1=(αh(n),1). (The canonical copy of N is normal, the canonical copy of H is a complement, and conjugation induces the action).

[L7]

A Sylow p-subgroup of a finite group is normal if and only if it is the unique Sylow p-subgroup. (A Sylow p-subgroup is normal if and only if it is unique).

[L8]

For every prime p, the operations of addition and multiplication on Z/p make it a field (def-field). (For every prime p, the two operations on Z/p make it a field).

[L9]

Let n be a positive integer. Every class in Z/n (def-integers-modulo-n) contains exactly one integer r with 0r<n. Consequently the map r[r]n(0r<n) is a bijection from the von Neumann natural n to Z/n, and Z/n=n. This includes n=1, where the only representative is 0. For n=0, the map a[a]0 is a bijection ZZ/0. (For n1, every class in Z/n has one representative r with 0r<n, so Z/n=n; while Z/0 is in bijection with Z).

[L10]

For n1, the unit group is (Z/n)×:={uZ/n:some vZ/n satisfies uv=[1]n}, and Euler's totient is φ(n):=(Z/n)×. (The unit group (Z/n)× and Euler's totient φ(n)=(Z/n)× for n1).

[L11]

Euler's totient satisfies φ(1)=1. If p is prime (def-prime), then φ(p)=p1.. (φ(1)=1, and φ(p)=p1 for every prime p).

[L12]
  1. If A and B are finite then A×B is finite and A×B=AB (def-finite-cardinality). 2. Let mN and let A0,,Am1 be finite sets. Write i<mAi:={f:f is a function with domain m and f(i)Ai for every i<m}. Then i<mAi is finite and i<mAi=i<mAi, the right-hand product being the N-valued one of def-nat-finite-sum-and-product. (The product rule: A×B=AB, and i<mAi=i<mAi).

Verification

technique · direct
1.1

In Hp=Fp3, expanding both triple products gives the same third coordinate c+c+c+ab+ab+ab; hence the operation is associative, with identity (0,0,0) and inverse (a,b,c)1=(a,b,c+ab).

L1L2L3L4L5L6L7L8L9L10L11L12givenalgebra
2.1

For d=(d1,d2,d3)D=(Fp×)3, the scaling factors on a,b,c are λ=d1d21, μ=d2d31, and λμ=d1d31. This identity preserves the cross term ab, so the scaling is an automorphism, and coordinate multiplication makes DAut(Hp) a homomorphism.

step 1.1givenalgebra
3.1

The semidirect product Bp=HpD is therefore defined, and its canonical copy of Hp is normal.

step 2.1givenalgebra
4.1

Since Hp=p3 and Bp=p3(p1)3, Hp has the full p-part of Bp; normality makes it the unique Sylow p-subgroup. For p=2, D is trivial and Bp=Hp. This proves the stated claim.

step 1.1step 3.1givenalgebra

Depends on

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