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

@[reducible, inline]

abbrev LeanPool.Polylean.K : Type

The kernel group - ℤ³, the free Abelian group on three generators.

Equations

• LeanPool.Polylean.K = (ℤ × ℤ × ℤ)

@[implicit_reducible]

instance LeanPool.Polylean.KGrp : AddCommGroup K

Equations

• LeanPool.Polylean.KGrp = inferInstance

@[implicit_reducible]

instance LeanPool.Polylean.instDecidableEqAddMonoidHomK : DecidableEq (K →+ K)

Equality of endomorphisms of K is decidable, as K is a free group with basis Unit ⊕ Unit ⊕ Unit.

Equations

• LeanPool.Polylean.instDecidableEqAddMonoidHomK = LeanPool.Polylean.decideHomsEqual

The quotient group

@[reducible, inline]

abbrev LeanPool.Polylean.Q : Type

The quotient group - ℤ/2 × ℤ/2, the Klein Four group.

Equations

• LeanPool.Polylean.Q = (Fin 2 × Fin 2)

@[implicit_reducible]

instance LeanPool.Polylean.QGrp : AddCommGroup Q

Equations

• LeanPool.Polylean.QGrp = inferInstance

The group elements

The generators of the free Abelian group K.

@[reducible, inline]

abbrev LeanPool.Polylean.K.x : K

The first generator of K.

Equations

• LeanPool.Polylean.K.x = (1, 0, 0)

@[reducible, inline]

abbrev LeanPool.Polylean.K.y : K

The second generator of K.

Equations

• LeanPool.Polylean.K.y = (0, 1, 0)

@[reducible, inline]

abbrev LeanPool.Polylean.K.z : K

The third generator of K.

Equations

• LeanPool.Polylean.K.z = (0, 0, 1)

The elements of the Klein Four group Q.

@[match_pattern]

def LeanPool.Polylean.Q.e : Q

The identity element of Q.

Equations

• LeanPool.Polylean.Q.e = (⟨0, LeanPool.Polylean.Q.e._proof_1⟩, ⟨0, LeanPool.Polylean.Q.e._proof_1⟩)

@[match_pattern]

def LeanPool.Polylean.Q.a : Q

The first generator of Q.

Equations

• LeanPool.Polylean.Q.a = (⟨1, LeanPool.Polylean.Q.a._proof_1⟩, ⟨0, LeanPool.Polylean.Q.e._proof_1⟩)

@[match_pattern]

def LeanPool.Polylean.Q.b : Q

The second generator of Q.

Equations

• LeanPool.Polylean.Q.b = (⟨0, LeanPool.Polylean.Q.e._proof_1⟩, ⟨1, LeanPool.Polylean.Q.a._proof_1⟩)

@[match_pattern]

def LeanPool.Polylean.Q.c : Q

The product of the first two generators of Q.

Equations

• LeanPool.Polylean.Q.c = (⟨1, LeanPool.Polylean.Q.a._proof_1⟩, ⟨1, LeanPool.Polylean.Q.a._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.

@[reducible, inline]

abbrev LeanPool.Polylean.neg (α : Type u_1) [SubtractionCommMonoid α] : α →+ α

An abbreviation for the negation homomorphism on commutative groups.

Equations

• LeanPool.Polylean.neg α = negAddMonoidHom

@[reducible]

def LeanPool.Polylean.action : Q → K →+ K

The action of Q on K by automorphisms. The action can be given a component-wise description in terms of id and neg, the identity and negation homomorphisms.

Equations

• LeanPool.Polylean.action (⟨0, ⋯⟩, ⟨0, ⋯⟩) = (AddMonoidHom.id ℤ).prodMap ((AddMonoidHom.id ℤ).prodMap (AddMonoidHom.id ℤ))
• LeanPool.Polylean.action (⟨1, ⋯⟩, ⟨0, ⋯⟩) = (AddMonoidHom.id ℤ).prodMap ((LeanPool.Polylean.neg ℤ).prodMap (LeanPool.Polylean.neg ℤ))
• LeanPool.Polylean.action (⟨0, ⋯⟩, ⟨1, ⋯⟩) = (LeanPool.Polylean.neg ℤ).prodMap ((AddMonoidHom.id ℤ).prodMap (LeanPool.Polylean.neg ℤ))
• LeanPool.Polylean.action (⟨1, ⋯⟩, ⟨1, ⋯⟩) = (LeanPool.Polylean.neg ℤ).prodMap ((LeanPool.Polylean.neg ℤ).prodMap (AddMonoidHom.id ℤ))

instance LeanPool.Polylean.instAutActionQKAction : AutAction action

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.

The cocycle

@[reducible]

def LeanPool.Polylean.cocycle : Q → Q → K

The cocycle in the construction of P.

Equations

• LeanPool.Polylean.cocycle (⟨1, ⋯⟩, ⟨0, ⋯⟩) (⟨1, ⋯⟩, ⟨0, ⋯⟩) = LeanPool.Polylean.K.x
• LeanPool.Polylean.cocycle (⟨1, ⋯⟩, ⟨0, ⋯⟩) (⟨1, ⋯⟩, ⟨1, ⋯⟩) = LeanPool.Polylean.K.x
• LeanPool.Polylean.cocycle (⟨0, ⋯⟩, ⟨1, ⋯⟩) (⟨0, ⋯⟩, ⟨1, ⋯⟩) = LeanPool.Polylean.K.y
• LeanPool.Polylean.cocycle (⟨1, ⋯⟩, ⟨1, ⋯⟩) (⟨0, ⋯⟩, ⟨1, ⋯⟩) = -LeanPool.Polylean.K.y
• LeanPool.Polylean.cocycle (⟨1, ⋯⟩, ⟨1, ⋯⟩) (⟨1, ⋯⟩, ⟨1, ⋯⟩) = LeanPool.Polylean.K.z
• LeanPool.Polylean.cocycle (⟨0, ⋯⟩, ⟨1, ⋯⟩) (⟨1, ⋯⟩, ⟨1, ⋯⟩) = -LeanPool.Polylean.K.x + -LeanPool.Polylean.K.z
• LeanPool.Polylean.cocycle (⟨1, ⋯⟩, ⟨1, ⋯⟩) (⟨1, ⋯⟩, ⟨0, ⋯⟩) = -LeanPool.Polylean.K.y + LeanPool.Polylean.K.z
• LeanPool.Polylean.cocycle (⟨0, ⋯⟩, ⟨1, ⋯⟩) (⟨1, ⋯⟩, ⟨0, ⋯⟩) = -LeanPool.Polylean.K.x + LeanPool.Polylean.K.y + -LeanPool.Polylean.K.z
• LeanPool.Polylean.cocycle x✝¹ x✝ = 0

@[implicit_reducible]

instance LeanPool.Polylean.PCocycle : Cocycle cocycle

A verification that the cocycle function indeed satisfies the cocycle condition. This check is performed fully automatically using previously defined decision procedures.

Equations

• One or more equations did not get rendered due to their size.

The construction of P

The construction of the group P as a Metabelian group from the given action and cocycle.

def LeanPool.Polylean.P : Type

the group P constructed via the cocycle construction

Equations

• LeanPool.Polylean.P = (LeanPool.Polylean.K × LeanPool.Polylean.Q)

@[implicit_reducible, instance 10000]

instance LeanPool.Polylean.P.PGrp : Group P

Equations

• LeanPool.Polylean.P.PGrp = LeanPool.Polylean.MetabelianGroup.metabelianGroup LeanPool.Polylean.cocycle

@[implicit_reducible]

def LeanPool.Polylean.P.instHMulProdKQ : HMul (K × Q) (K × Q) (K × Q)

Multiplication for P coming from its metabelian group structure.

Equations

• LeanPool.Polylean.P.instHMulProdKQ = { hMul := Mul.mul }

@[implicit_reducible]

def LeanPool.Polylean.P.instMulProdKQ : Mul (K × Q)

Multiplication for P coming from its metabelian group structure.

Equations

• LeanPool.Polylean.P.instMulProdKQ = { mul := Mul.mul }

@[reducible]

instance LeanPool.Polylean.P.instPow : Pow (K × Q) ℕ

Equations

• LeanPool.Polylean.P.instPow = { pow := fun (p : LeanPool.Polylean.K × LeanPool.Polylean.Q) (n : ℕ) => Monoid.npow n p }

@[implicit_reducible]

instance LeanPool.Polylean.P.instDecidableEq : DecidableEq P

Equations

• LeanPool.Polylean.P.instDecidableEq = LeanPool.Polylean.P.instDecidableEq._aux_1

@[simp]

theorem LeanPool.Polylean.P.mul (k k' : K) (q q' : Q) : (k, q) * (k', q') = (k + (action q) k' + cocycle q q', q + q')

A confirmation that multiplication in P is as expected from the Metabelian group structure.

theorem LeanPool.Polylean.P.one : 1 = ((0, 0, 0), Q.e)

theorem LeanPool.Polylean.P.kernel_pow (k : K) (n : ℕ) : (k, Q.e) ^ n = (n • k, Q.e)

Powers of kernel elements remain in the kernel.