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

ink

class AutAction {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) : Type

• The automorphism corresponding to the zero element is the identity.

  id_action : α 0 = AddMonoidHom.id B

• The compatibility of group addition with the action by automorphisms.

  compatibility : ∀ (a a' : A), α (a + a') = AddMonoidHom.comp (α a) (α a')

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.

ink

instance AutAction.toAddAction {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) [inst : AutAction α] : AddAction A B

An action by automorphisms of additive groups is an additive group action.

Equations

• AutAction.toAddAction α = AddAction.mk (_ : ∀ (p : B), ↑(α 0) p = p) (_ : ∀ (g₁ g₂ : A) (p : B), ↑(α (g₁ + g₂)) p = ↑(α g₁) (↑(α g₂) p))

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

ink

theorem AutAction.vadd_eq {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) [inst : AutAction α] {a : A} {b : B} : a +ᵥ b = ↑(α a) b

ink

theorem AutAction.vadd_zero {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) [inst : AutAction α] {a : A} : a +ᵥ 0 = 0

ink

theorem AutAction.vadd_dist {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) [inst : AutAction α] {a : A} {b : B} {b' : B} : a +ᵥ (b + b') = a +ᵥ b + (a +ᵥ b')

ink

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

ink

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

ink

theorem AutAction.vadd_of_neg {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst : AddGroup B] (α : A → B →+ B) [inst : AutAction α] {a : A} {b : B} : a +ᵥ -b = -(a +ᵥ b)

Cocycles

ink

class Cocycle {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst : AddGroup K] (c : Q → Q → K) : Type (maxu_1u_2)

• An action of the quotient on the kernel by automorphisms.

  α : Q → K →+ K

• A typeclass instance for the action by automorphisms.

  autAct : AutAction α

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

  cocycle_zero : c 0 0 = 0

• The cocycle condition.

  cocycle_condition : ∀ (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')

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".

A few deductions from the cocycle condition.

ink

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

Equations

• Cocycle.instAutActionα c = Cocycle.autAct

ink

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

ink

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

ink

theorem Cocycle.inv_rel {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst : AddGroup K] (c : Q → Q → K) [ccl : Cocycle c] (q : Q) : c q (-q) = q +ᵥ c (-q) q

ink

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