import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.GroupAction.Defs
import Aesop

/-!
## 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
-/

/-- 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. -/
class AutAction: {A : Type u_1} →
  {B : Type u_2} →
    [inst : AddGroup A] →
      [inst_1 : AddGroup B] →
        {α : A → B →+ B} →
          α 0 = AddMonoidHom.id B → (∀ (a a' : A), α (a + a') = AddMonoidHom.comp (α a) (α a')) → AutAction α
AutAction {A: Type ?u.2
A B: Type ?u.5
B : Type _: Type (?u.2+1)
Type _} [AddGroup: Type ?u.8 → Type ?u.8
AddGroup A: Type ?u.2
A] [AddGroup: Type ?u.11 → Type ?u.11
AddGroup B: Type ?u.5
B] (α: A → B →+ B
α : A: Type ?u.2
A → (B: Type ?u.5
B →+ B: Type ?u.5
B)) where
  /-- The automorphism corresponding to the zero element is the identity. -/
  id_action: ∀ {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst_1 : AddGroup B] {α : A → B →+ B} [self : AutAction α],
  α 0 = AddMonoidHom.id B
id_action : α: A → B →+ B
α 0: ?m.81
0 = .id: (M : Type ?u.195) → [inst : AddZeroClass M] → M →+ M
.id _: Type ?u.195
_
  /-- The compatibility of group addition with the action by automorphisms. -/
  compatibility: ∀ {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst_1 : AddGroup B] {α : A → B →+ B} [self : AutAction α]
  (a a' : A), α (a + a') = AddMonoidHom.comp (α a) (α a')
compatibility : ∀ a: A
a a': A
a' : A: Type ?u.2
A, α: A → B →+ B
α (a: A
a + a': A
a') = (α: A → B →+ B
α a: A
a).comp: {M : Type ?u.344} →
  {N : Type ?u.343} →
    {P : Type ?u.342} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ P
comp (α: A → B →+ B
α a': A
a')


namespace AutAction

variable {A: Type ?u.4784
A B: Type ?u.5515
B : Type _: Type (?u.4787+1)
Type _} [AddGroup: Type ?u.17866 → Type ?u.17866
AddGroup A: Type ?u.582
A] [AddGroup: Type ?u.443 → Type ?u.443
AddGroup B: Type ?u.585
B] (α: A → B →+ B
α : A: Type ?u.7348
A → (B: Type ?u.437
B →+ B: Type ?u.437
B)) [AutAction: {A : Type ?u.510} → {B : Type ?u.509} → [inst : AddGroup A] → [inst : AddGroup B] → (A → B →+ B) → Type
AutAction α: A → B →+ B
α]

declare_aesop_rule_sets [AutAction]

attribute [aesop norm (rule_sets [AutAction])] id_action: ∀ {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst_1 : AddGroup B] {α : A → B →+ B} [self : AutAction α],
  α 0 = AddMonoidHom.id B
id_action
attribute [aesop norm (rule_sets [AutAction])] compatibility: ∀ {A : Type u_1} {B : Type u_2} [inst : AddGroup A] [inst_1 : AddGroup B] {α : A → B →+ B} [self : AutAction α]
  (a a' : A), α (a + a') = AddMonoidHom.comp (α a) (α a')
compatibility

/-- An action by automorphisms of additive groups is an additive group action. -/
instance toAddAction: AddAction A B
toAddAction : AddAction: (G : Type ?u.697) → Type ?u.696 → [inst : AddMonoid G] → Type (max?u.697?u.696)
AddAction A: Type ?u.582
A B: Type ?u.585
B where
  vadd := fun a: ?m.762
a b: ?m.765
b => α: A → B →+ B
α a: ?m.762
a b: ?m.765
b
  zero_vadd := by A: Type ?u.582

B: Type ?u.585

inst✝²: AddGroup A

inst✝¹: AddGroup B

α: A → B →+ B

inst✝: AutAction α

∀ (p : B), 0 +ᵥ p = paesop (rule_sets [AutAction]) (add norm unfold [HVAdd.hVAdd])
Goals accomplished! 🐙
  add_vadd  := by A: Type ?u.582

B: Type ?u.585

inst✝²: AddGroup A

inst✝¹: AddGroup B

α: A → B →+ B

inst✝: AutAction α

∀ (g₁ g₂ : A) (p : B), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)aesop (rule_sets [AutAction]) (add norm unfold [HVAdd.hVAdd])
Goals accomplished! 🐙

/-!
Some easy consequences of the definition of an action by automorphisms.
-/

@[aesop norm (rule_sets [AutAction])]
lemma vadd_eq: ∀ {a : A} {b : B}, a +ᵥ b = ↑(α a) b
vadd_eq : ∀ {a: A
a : A: Type ?u.4784
A} {b: B
b : B: Type ?u.4787
B}, a: A
a +ᵥ b: B
b = α: A → B →+ B
α a: A
a b: B
b := rfl: ∀ {α : Sort ?u.5467} {a : α}, a = a
rfl

@[aesop norm (rule_sets [AutAction])]
lemma vadd_zero: ∀ {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst_1 : AddGroup B] (α : A → B →+ B) [inst_2 : AutAction α]
  {a : A}, a +ᵥ 0 = 0
vadd_zero : ∀ {a: A
a : A: Type ?u.5512
A}, a: A
a +ᵥ (0: ?m.5640
0 : B: Type ?u.5515
B) = (0: ?m.5853
0 : B: Type ?u.5515
B) := by A: Type u_2

B: Type u_1

inst✝²: AddGroup A

inst✝¹: AddGroup B

α: A → B →+ B

inst✝: AutAction α

∀ {a : A}, a +ᵥ 0 = 0aesop (rule_sets [AutAction])
Goals accomplished! 🐙

@[aesop unsafe (rule_sets [AutAction])]
lemma vadd_dist: ∀ {a : A} {b b' : B}, a +ᵥ (b + b') = a +ᵥ b + (a +ᵥ b')
vadd_dist : ∀ {a: A
a : A: Type ?u.7348
A} {b: B
b b': B
b' : B: Type ?u.7351
B}, a: A
a +ᵥ (b: B
b + b': B
b') = (a: A
a +ᵥ b: B
b) + (a: A
a +ᵥ b': B
b') := by A: Type u_2

B: Type u_1

inst✝²: AddGroup A

inst✝¹: AddGroup B

α: A → B →+ B

inst✝: AutAction α

∀ {a : A} {b b' : B}, a +ᵥ (b + b') = a +ᵥ b + (a +ᵥ b')aesop (rule_sets [AutAction])
Goals accomplished! 🐙

@[aesop unsafe (rule_sets [AutAction])]
lemma compatibility': ∀ {A : Type u_2} {B : Type u_1} [inst : AddGroup A] [inst_1 : AddGroup B] (α : A → B →+ B) [inst_2 : AutAction α]
  {a a' : A} {b : B}, ↑(α a) (↑(α a') b) = ↑(α (a + a')) b
compatibility' : ∀ {a: A
a a': A
a' : A: Type ?u.11692
A} {b: B
b : B: Type ?u.11695
B}, α: A → B →+ B
α a: A
a (α: A → B →+ B
α a': A
a' b: B
b) = α: A → B →+ B
α (a: A
a + a': A
a') b: B
b := by A: Type u_2

B: Type u_1

inst✝²: AddGroup A

inst✝¹: AddGroup B

α: A → B →+ B

inst✝: AutAction α

∀ {a a' : A} {b : B}, ↑(α a) (↑(α a') b) = ↑(α (a + a')) baesop (rule_sets [AutAction])
Goals accomplished! 🐙 

@[aesop norm (rule_sets [AutAction])]
lemma act_neg_act: ∀ {a : A} {b : B}, ↑(α a) (↑(α (-a)) b) = b
act_neg_act {a: A
a : A: Type ?u.15917
A} {b: B
b : B: Type ?u.15920
B} : α: A → B →+ B
α a: A
a (α: A → B →+ B
α (-a: A
a) b: B
b) = b: B
b := by
  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) = brw [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) = bcompatibility': ∀ {A : Type ?u.16966} {B : Type ?u.16965} [inst : AddGroup A] [inst_1 : AddGroup B] (α : A → B →+ B)
  [inst_2 : AutAction α] {a a' : A} {b : B}, ↑(α a) (↑(α a') b) = ↑(α (a + a')) b
compatibility'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]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
  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) = baesop (erase compatibility) (rule_sets [AutAction])
Goals accomplished! 🐙

@[aesop unsafe (rule_sets [AutAction])]
lemma vadd_of_neg: ∀ {a : A} {b : B}, a +ᵥ -b = -(a +ᵥ b)
vadd_of_neg : ∀ {a: A
a : A: Type ?u.17860
A} {b: B
b : B: Type ?u.17863
B}, a: A
a +ᵥ (-b: B
b) = - (a: A
a +ᵥ b: B
b) := by 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)aesop (rule_sets [AutAction])
Goals accomplished! 🐙

end AutAction


/-!
### Cocycles
-/

/--
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". -/
class Cocycle: {Q : Type u_1} → {K : Type u_2} → [inst : AddGroup Q] → [inst : AddGroup K] → (Q → Q → K) → Type (maxu_1u_2)
Cocycle {Q: Type ?u.21201
Q K: Type ?u.21204
K : Type _: Type (?u.21204+1)
Type _} [AddGroup: Type ?u.21207 → Type ?u.21207
AddGroup Q: Type ?u.21201
Q] [AddGroup: Type ?u.21210 → Type ?u.21210
AddGroup K: Type ?u.21204
K] (c: Q → Q → K
c : Q: Type ?u.21201
Q → Q: Type ?u.21201
Q → K: Type ?u.21204
K) where
  /-- An action of the quotient on the kernel by automorphisms. -/
  α: {Q : Type u_1} →
  {K : Type u_2} → [inst : AddGroup Q] → [inst_1 : AddGroup K] → (c : Q → Q → K) → [self : Cocycle c] → Q → K →+ K
α : Q: Type ?u.21201
Q → (K: Type ?u.21204
K →+ K: Type ?u.21204
K)
  /-- A typeclass instance for the action by automorphisms. -/
  autAct: {Q : Type u_1} →
  {K : Type u_2} →
    [inst : AddGroup Q] → [inst_1 : AddGroup K] → {c : Q → Q → K} → [self : Cocycle c] → AutAction (Cocycle.α c)
autAct : AutAction: {A : Type ?u.21285} → {B : Type ?u.21284} → [inst : AddGroup A] → [inst : AddGroup B] → (A → B →+ B) → Type
AutAction α: Q → K →+ K
α
  /-- The value of the cocycle is zero when its inputs are zero, as a convention. -/
  cocycle_zero: ∀ {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c], c 0 0 = 0
cocycle_zero : c: Q → Q → K
c 0: ?m.21325
0 0: ?m.21434
0 = (0: ?m.21515
0 : K: Type ?u.21204
K)
  /-- The *cocycle condition*. -/
  cocycle_condition: ∀ {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c]
  (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')
cocycle_condition : ∀ q: Q
q q': Q
q' q'': Q
q'' : Q: Type ?u.21201
Q, c: Q → Q → K
c q: Q
q q': Q
q' + c: Q → Q → K
c (q: Q
q + q': Q
q') q'': Q
q'' = q: Q
q +ᵥ c: Q → Q → K
c q': Q
q' q'': Q
q'' + c: Q → Q → K
c q: Q
q (q': Q
q' + q'': Q
q'')


namespace Cocycle

/-!
A few deductions from the cocycle condition.
-/

declare_aesop_rule_sets [Cocycle]

variable {Q: Type ?u.22168
Q K: Type ?u.22079
K : Type _: Type (?u.22409+1)
Type _} [AddGroup: Type ?u.22415 → Type ?u.22415
AddGroup Q: Type ?u.22076
Q] [AddGroup: Type ?u.22073 → Type ?u.22073
AddGroup K: Type ?u.22412
K]
variable (c: Q → Q → K
c : Q: Type ?u.24409
Q → Q: Type ?u.22168
Q → K: Type ?u.22079
K) [ccl: Cocycle c
ccl : Cocycle: {Q : Type ?u.22095} →
  {K : Type ?u.22094} → [inst : AddGroup Q] → [inst : AddGroup K] → (Q → Q → K) → Type (max?u.22095?u.22094)
Cocycle c: Q → Q → K
c]

attribute [aesop norm (rule_sets [Cocycle])] Cocycle.cocycle_zero: ∀ {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c], c 0 0 = 0
Cocycle.cocycle_zero
attribute [aesop norm (rule_sets [Cocycle])] Cocycle.cocycle_condition: ∀ {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c]
  (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')
Cocycle.cocycle_condition

instance: {Q : Type u_1} →
  {K : Type u_2} → [inst : AddGroup Q] → [inst_1 : AddGroup K] → (c : Q → Q → K) → [ccl : Cocycle c] → AutAction (α c)
instance : AutAction: {A : Type ?u.22219} → {B : Type ?u.22218} → [inst : AddGroup A] → [inst : AddGroup B] → (A → B →+ B) → Type
AutAction ccl: Cocycle c
ccl.α: {Q : Type ?u.22235} →
  {K : Type ?u.22234} → [inst : AddGroup Q] → [inst_1 : AddGroup K] → (c : Q → Q → K) → [self : Cocycle c] → Q → K →+ K
α := ccl: Cocycle c
ccl.autAct: {Q : Type ?u.22282} →
  {K : Type ?u.22281} →
    [inst : AddGroup Q] → [inst_1 : AddGroup K] → {c : Q → Q → K} → [self : Cocycle c] → AutAction (α c)
autAct

@[aesop norm (rule_sets [Cocycle])]
lemma left_id: ∀ {q : Q}, c 0 q = 0
left_id {q: Q
q : Q: Type ?u.22409
Q} : c: Q → Q → K
c 0: ?m.22463
0 q: Q
q = (0: ?m.22575
0 : K: Type ?u.22412
K) := by
  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 = 0have := ccl: Cocycle c
ccl.cocycle_condition: ∀ {Q : Type ?u.22693} {K : Type ?u.22692} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c]
  (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')
cocycle_condition 0: ?m.22711
0 0: ?m.22820
0 q: Q
qQ: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddGroup K

c: Q → Q → K

ccl: Cocycle c

q: Q

this: c 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)

c 0 q = 0
  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 = 0aesop (rule_sets [Cocycle])
Goals accomplished! 🐙

@[aesop norm (rule_sets [Cocycle])]
lemma right_id: ∀ {q : Q}, c q 0 = 0
right_id {q: Q
q : Q: Type ?u.24409
Q} : c: Q → Q → K
c q: Q
q 0: ?m.24463
0 = (0: ?m.24575
0 : K: Type ?u.24412
K) := by
  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 = 0have := ccl: Cocycle c
ccl.cocycle_condition: ∀ {Q : Type ?u.24693} {K : Type ?u.24692} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c]
  (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')
cocycle_condition q: Q
q 0: ?m.24711
0 0: ?m.24820
0Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddGroup K

c: Q → Q → K

ccl: Cocycle c

q: Q

this: c q 0 + c (q + 0) 0 = q +ᵥ c 0 0 + c q (0 + 0)

c q 0 = 0
  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 = 0aesop (rule_sets [AutAction, Cocycle])
Goals accomplished! 🐙

@[aesop unsafe (rule_sets [Cocycle])]
lemma inv_rel: ∀ (q : Q), c q (-q) = q +ᵥ c (-q) q
inv_rel (q: Q
q : Q: Type ?u.30060
Q) : c: Q → Q → K
c q: Q
q (-q: Q
q) = q: Q
q +ᵥ (c: Q → Q → K
c (-q: Q
q) q: Q
q) := by
  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) qhave := ccl: Cocycle c
ccl.cocycle_condition: ∀ {Q : Type ?u.30315} {K : Type ?u.30314} [inst : AddGroup Q] [inst_1 : AddGroup K] {c : Q → Q → K} [self : Cocycle c]
  (q q' q'' : Q), c q q' + c (q + q') q'' = q +ᵥ c q' q'' + c q (q' + q'')
cocycle_condition q: Q
q (-q: Q
q) q: Q
qQ: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddGroup K

c: Q → Q → K

ccl: Cocycle c

q: Q

this: c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)

c q (-q) = q +ᵥ c (-q) q
  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) qaesop (rule_sets [AutAction, Cocycle])
Goals accomplished! 🐙

@[aesop unsafe (rule_sets [Cocycle])]
lemma inv_rel': ∀ (q : Q), c (-q) q = -q +ᵥ c q (-q)
inv_rel' (q: Q
q : Q: Type ?u.41077
Q) : c: Q → Q → K
c (-q: Q
q) q: Q
q = (-q: Q
q) +ᵥ (c: Q → Q → K
c q: Q
q (-q: Q
q)) := by
  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)have := inv_rel: ∀ {Q : Type ?u.41357} {K : Type ?u.41356} [inst : AddGroup Q] [inst_1 : AddGroup K] (c : Q → Q → K) [ccl : Cocycle c]
  (q : Q), c q (-q) = q +ᵥ c (-q) q
inv_rel c: Q → Q → K
c (-q: Q
q)Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddGroup K

c: Q → Q → K

ccl: Cocycle c

q: Q

this: c (-q) (- -q) = -q +ᵥ c (- -q) (-q)

c (-q) q = -q +ᵥ c q (-q)
  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)aesop
Goals accomplished! 🐙

end Cocycle