Documentation

UnitConjecture.MetabelianGroup

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.

def MetabelianGroup.mul {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : 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

MetabelianGroup.mul c x x = match x, x with | (k, q), (k', q') => (k + (q +ᵥ k') + c q q', q + q')

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

K × Q

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

Equations

MetabelianGroup.e = (0, 0)

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

K × Q → K × Q

The inverse operation of the Metabelian group.

Equations

MetabelianGroup.inv c x = match x with | (k, q) => (-(-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 MetabelianGroup.left_id {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) :

MetabelianGroup.mul c MetabelianGroup.e g = g

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

MetabelianGroup.mul c g MetabelianGroup.e = g

theorem MetabelianGroup.left_inv {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) :

MetabelianGroup.mul c (MetabelianGroup.inv c g) g = MetabelianGroup.e

theorem MetabelianGroup.right_inv {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (g : K × Q) :

MetabelianGroup.mul c g (MetabelianGroup.inv c g) = MetabelianGroup.e

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

MetabelianGroup.mul c (MetabelianGroup.mul c g g') g'' = MetabelianGroup.mul c g (MetabelianGroup.mul c g' g'')

instance MetabelianGroup.metabelianGroup {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

Group (K × Q)

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

Equations

MetabelianGroup.metabelianGroup c = Group.mk (_ : ∀ (g : K × Q), MetabelianGroup.mul c (MetabelianGroup.inv c g) g = MetabelianGroup.e)

theorem MetabelianGroup.mul_def {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] {k : K} {k' : K} {q : Q} {q' : Q} :

(k, q) * (k', q') = (k + (q +ᵥ k') + c q q', q + q')

theorem MetabelianGroup.kernel_pow {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] (k : K) (n : ℕ) :

(k, 0) ^ n = (n • k, 0)

Exactness #

A proof that the Metabelian group G constructed as above indeed lies in middle of the short exact sequence 1 → K → G → Q → 1.

def MetabelianGroup.Kernel.inclusion {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

Multiplicative K →* K × Q

The inclusion map from the kernel to the Metabelian group.

Equations

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

theorem MetabelianGroup.Kernel.inclusion_inj {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

Function.Injective ↑(MetabelianGroup.Kernel.inclusion c)

A proof that the inclusion map is injective.

def MetabelianGroup.Quotient.projection {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

K × Q →* Multiplicative Q

The projection map from the Metabelian group to the quotient.

Equations

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

theorem MetabelianGroup.Quotient.projection_surj {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

Function.Surjective ↑(MetabelianGroup.Quotient.projection c)

A proof that the projection map is surjective.

theorem MetabelianGroup.exact_seq {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddCommGroup K] (c : Q → Q → K) [ccl : Cocycle c] :

MonoidHom.mrange (MetabelianGroup.Kernel.inclusion c) = MonoidHom.mker (MetabelianGroup.Quotient.projection c)

A proof that the image of the first map is the kernel of the second map.