Cocycles and Group actions by automorphisms

The definitions of cocycles and group actions by automorphisms, which are required for the Metabelian construction.

Overview

• AutAction - the definition of an action of one group on another by automorphisms. This is done as a typeclass representing the property of being an action by automorphisms.
• Cocycle - the definition of a cocycle associated with a certain action by automorphisms. This is also done as a typeclass with the function as an explicit argument and the action as a field of the structure.

Actions by automorphisms

class LeanPool.Polylean.AutAction {A : Type u_1} {B : Type u_2} [AddGroup A] [AddGroup B] (α : A → B →+ B) : Prop

An action of an additive group on another additive group by automorphisms. There is a closely related typeclass DistribMulAction in Mathlib that uses multiplicative notation.

• id_action : α 0 = AddMonoidHom.id B

  The automorphism corresponding to the zero element is the identity.

• compatibility (a a' : A) : α (a + a') = (α a).comp (α a')

  The compatibility of group addition with the action by automorphisms.

Some easy consequences of the definition of an action by automorphisms.

theorem LeanPool.Polylean.AutAction.apply_zero {A : Type u_2} {B : Type u_1} [AddGroup B] (α : A → B →+ B) {a : A} : (α a) 0 = 0

theorem LeanPool.Polylean.AutAction.zero_apply {A : Type u_2} {B : Type u_1} [AddGroup A] [AddGroup B] (α : A → B →+ B) [AutAction α] {b : B} : (α 0) b = b

theorem LeanPool.Polylean.AutAction.apply_add {A : Type u_2} {B : Type u_1} [AddGroup B] (α : A → B →+ B) {a : A} {b b' : B} : (α a) (b + b') = (α a) b + (α a) b'

theorem LeanPool.Polylean.AutAction.compatibility' {A : Type u_2} {B : Type u_1} [AddGroup A] [AddGroup B] (α : A → B →+ B) [AutAction α] {a a' : A} {b : B} : (α a) ((α a') b) = (α (a + a')) b

theorem LeanPool.Polylean.AutAction.act_neg_act {A : Type u_2} {B : Type u_1} [AddGroup A] [AddGroup B] (α : A → B →+ B) [AutAction α] {a : A} {b : B} : (α a) ((α (-a)) b) = b

theorem LeanPool.Polylean.AutAction.apply_neg {A : Type u_2} {B : Type u_1} [AddGroup B] (α : A → B →+ B) {a : A} {b : B} : (α a) (-b) = -(α a) b

Cocycles

class LeanPool.Polylean.Cocycle {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddGroup K] (c : Q → Q → K) : Type (max u_1 u_2)

A cocycle associated with a certain action of Q on K via automorphisms is a function from Q × Q to K satisfying a certain requirement known as the "cocycle condition".

• α : Q → K →+ K

  An action of the quotient on the kernel by automorphisms.

• autAct : AutAction (α c)

  A typeclass instance for the action by automorphisms.

• cocycle_zero : c 0 0 = 0

  The value of the cocycle is zero when its inputs are zero, as a convention.

• cocycle_condition (q q' q'' : Q) : c q q' + c (q + q') q'' = (α c q) (c q' q'') + c q (q' + q'')

  The cocycle condition.

A few deductions from the cocycle condition.

instance LeanPool.Polylean.Cocycle.instAutActionα {Q : Type u_1} {K : Type u_2} [AddGroup Q] [AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] : AutAction (α c)

theorem LeanPool.Polylean.Cocycle.left_id {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] {q : Q} : c 0 q = 0

theorem LeanPool.Polylean.Cocycle.right_id {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] {q : Q} : c q 0 = 0

theorem LeanPool.Polylean.Cocycle.inv_rel {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] (q : Q) : c q (-q) = (α c q) (c (-q) q)

theorem LeanPool.Polylean.Cocycle.inv_rel' {Q : Type u_2} {K : Type u_1} [AddGroup Q] [AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] (q : Q) : c (-q) q = (α c (-q)) (c q (-q))