Metabelian groups

Metabelian groups are group extensions 1 → K → G → Q → 1 with both the kernel and the quotient Abelian. Such an extension is determined by data:

• a group action of Q on K by automorphisms
• a cocyle c: Q → Q → K

We define the cocycle condition and construct a group structure on a structure extending K × Q. The main step is to show that the cocyle condition implies associativity.

@[reducible]

def LeanPool.Polylean.MetabelianGroup.mul {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] : K × Q → K × Q → K × Q

The multiplication operation defined using the cocycle. The cocycle condition is crucially used in showing associativity and other properties.

Equations

• LeanPool.Polylean.MetabelianGroup.mul c (k, q) (k', q') = (k + (LeanPool.Polylean.Cocycle.α c q) k' + c q q', q + q')

@[reducible]

def LeanPool.Polylean.MetabelianGroup.e {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddCommGroup K] : K × Q

The identity element of the Metabelian group, which is the ordered pair of the identities of the individual groups.

Equations

• LeanPool.Polylean.MetabelianGroup.e = (0, 0)

@[reducible]

def LeanPool.Polylean.MetabelianGroup.inv {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] : K × Q → K × Q

The inverse operation of the Metabelian group.

Equations

• LeanPool.Polylean.MetabelianGroup.inv c (k, q) = (-(LeanPool.Polylean.Cocycle.α c (-q)) (k + c q (-q)), -q)

Some of the standard lemmas to show that K × Q has the structure of a group with the above operations.

theorem LeanPool.Polylean.MetabelianGroup.left_id {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) : mul c e g = g

theorem LeanPool.Polylean.MetabelianGroup.right_id {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) : mul c g e = g

theorem LeanPool.Polylean.MetabelianGroup.left_inv {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) : mul c (inv c g) g = e

theorem LeanPool.Polylean.MetabelianGroup.right_inv {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) : mul c g (inv c g) = e

theorem LeanPool.Polylean.MetabelianGroup.mul_assoc {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g g' g'' : K × Q) : mul c (mul c g g') g'' = mul c g (mul c g' g'')

@[reducible]

def LeanPool.Polylean.MetabelianGroup.metabelianGroup {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] : Group (K × Q)

A group structure on K × Q using the above multiplication operation.

Equations

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