The construction of the group P #
We construct the group P (the Promislow or Hantzsche–Wendt group) as a Metabelian group.
This is done via the cocycle construction, using the explicit action and cocycle described in Section 3.1 of Giles Gardam's paper (https://arxiv.org/abs/2102.11818).
The components of the group P #
The group P is constructed as a Metabelian group with kernel K := ℤ³ and quotient Q := ℤ/2 × ℤ/2.
The kernel group
Equality of endomorphisms of K is decidable, as K is a free group with basis Unit ⊕ Unit ⊕ Unit.
Equations
The quotient group
The group elements #
The generators of the free Abelian group K.
The elements of the Klein Four group Q.
The identity element of Q.
Equations
- Q.e = ({ val := 0, isLt := Q.e.proof_1 }, { val := 0, isLt := Q.e.proof_1 })
The first generator of Q.
Equations
- Q.a = ({ val := 1, isLt := Q.a.proof_1 }, { val := 0, isLt := Q.a.proof_2 })
The second generator of Q.
Equations
- Q.b = ({ val := 0, isLt := Q.b.proof_1 }, { val := 1, isLt := Q.b.proof_2 })
The product of the first two generators of Q.
Equations
- Q.c = ({ val := 1, isLt := Q.c.proof_1 }, { val := 1, isLt := Q.c.proof_1 })
The action of Q on K by automorphisms #
The action of the group Q on the kernel K by automorphisms required for constructing P.
A verification that the above action is indeed an action by automorphisms. This is done automatically with the machinery of decidable equality of homomorphisms on free groups.
Equations
- One or more equations did not get rendered due to their size.
The cocycle #
A verification that the cocycle function indeed satisfies the cocycle condition.
This check is performed fully automatically using previously defined decision procedures.
Equations
- P_cocycle = { α := action, autAct := inferInstance, cocycle_zero := P_cocycle.proof_2, cocycle_condition := P_cocycle.proof_3 }
The construction of P #
The construction of the group P as a Metabelian group from the given action and cocycle.