Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
import Mathlib.Algebra.Hom.Group
import Mathlib.GroupTheory.Submonoid.Operations
import UnitConjecture.Cocycle

/-!

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

namespace MetabelianGroup

variable {
Q: Type ?u.2
Q 
K: Type ?u.5
K : 
Type _: Type (?u.93304+1)
Type _} [
AddGroup: Type ?u.2670 β†’ Type ?u.2670
AddGroup 
Q: Type ?u.2
Q] [
AddCommGroup: Type ?u.2673 β†’ Type ?u.2673
AddCommGroup 
K: Type ?u.5
K]
variable (
c: Q β†’ Q β†’ K
c : 
Q: Type ?u.14
Q β†’ 
Q: Type ?u.81288
Q β†’ 
K: Type ?u.96
K) [
ccl: Cocycle c
ccl : 
Cocycle: {Q : Type ?u.1221} β†’
  {K : Type ?u.1220} β†’ [inst : AddGroup Q] β†’ [inst : AddGroup K] β†’ (Q β†’ Q β†’ K) β†’ Type (max?u.1221?u.1220)
Cocycle 
c: Q β†’ Q β†’ K
c]

declare_aesop_rule_sets [Metabelian]

/-- The multiplication operation defined using the cocycle.
The cocycle condition is crucially used in showing associativity and other properties. -/
@[reducible, aesop norm unfold (rule_sets [Metabelian])] 
def 
mul: K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul : (
K: Type ?u.96
K Γ— 
Q: Type ?u.93
Q) β†’ (
K: Type ?u.96
K Γ— 
Q: Type ?u.93
Q) β†’ (
K: Type ?u.96
K Γ— 
Q: Type ?u.93
Q)
  | (
k: K
k, 
q: Q
q), (
k': K
k', 
q': Q
q') => (
k: K
k + (
q: Q
q +α΅₯ 
k': K
k') + 
c: Q β†’ Q β†’ K
c 
q: Q
q 
q': Q
q', 
q: Q
q + 
q': Q
q')

/-- The identity element of the Metabelian group, 
  which is the ordered pair of the identities of the individual groups. -/
@[reducible, aesop norm unfold (rule_sets [Metabelian])] 
def 
e: {Q : Type u_1} β†’ {K : Type u_2} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e : 
K: Type ?u.1205
K Γ— 
Q: Type ?u.1202
Q := (
0: ?m.1291
0, 
0: ?m.1408
0)

/-- The inverse operation of the Metabelian group. -/
@[reducible, aesop norm unfold (rule_sets [Metabelian])] 
def 
inv: {Q : Type u_1} β†’
  {K : Type u_2} β†’ [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q
inv : 
K: Type ?u.1691
K Γ— 
Q: Type ?u.1688
Q β†’ 
K: Type ?u.1691
K Γ— 
Q: Type ?u.1688
Q
  | (
k: K
k, 
q: Q
q) => (- ((-
q: Q
q) +α΅₯ (
k: K
k  + 
c: Q β†’ Q β†’ K
c 
q: Q
q (-
q: Q
q))), -
q: Q
q)

/-!
Some of the standard lemmas to show that `K Γ— Q` has the structure of a group with the above operations.
-/

@[aesop norm (rule_sets [Metabelian])] 
lemma 
left_id: βˆ€ (g : K Γ— Q), mul c e g = g
left_id : βˆ€ (
g: K Γ— Q
g : 
K: Type ?u.2667
K Γ— 
Q: Type ?u.2664
Q), 
mul: {Q : Type ?u.2750} β†’
  {K : Type ?u.2749} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
e: {Q : Type ?u.2763} β†’ {K : Type ?u.2762} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e 
g: K Γ— Q
g = 
g: K Γ— Q
g
  | (
k: K
k, 
q: Q
q) => 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

mul c e (k, q) = (k, q)
Goals accomplished! πŸ™


@[aesop norm (rule_sets [Metabelian])]
lemma 
right_id: βˆ€ {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K) [ccl : Cocycle c]
  (g : K Γ— Q), mul c g e = g
right_id : βˆ€ (
g: K Γ— Q
g : 
K: Type ?u.5420
K Γ— 
Q: Type ?u.5417
Q), 
mul: {Q : Type ?u.5503} β†’
  {K : Type ?u.5502} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g 
e: {Q : Type ?u.5518} β†’ {K : Type ?u.5517} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e = 
g: K Γ— Q
g
  | (
k: K
k, 
q: Q
q) => 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

mul c (k, q) e = (k, q)
Goals accomplished! πŸ™


@[aesop norm (rule_sets [Metabelian])]
lemma 
left_inv: βˆ€ {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K) [ccl : Cocycle c]
  (g : K Γ— Q), mul c (inv c g) g = e
left_inv : βˆ€ (
g: K Γ— Q
g : 
K: Type ?u.10844
K Γ— 
Q: Type ?u.10841
Q), 
mul: {Q : Type ?u.10927} β†’
  {K : Type ?u.10926} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c (
inv: {Q : Type ?u.10940} β†’
  {K : Type ?u.10939} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q
inv 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g) 
g: K Γ— Q
g = 
e: {Q : Type ?u.11008} β†’ {K : Type ?u.11007} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e
  | (
k: K
k , 
q: Q
q) => 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

mul c (inv c (k, q)) (k, q) = e
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

this: c (-q) q = -q +α΅₯ c q (-q)

mul c (inv c (k, q)) (k, q) = e
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

mul c (inv c (k, q)) (k, q) = e
Goals accomplished! πŸ™


@[aesop norm (rule_sets [Metabelian])]
lemma 
right_inv: βˆ€ {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K) [ccl : Cocycle c]
  (g : K Γ— Q), mul c g (inv c g) = e
right_inv : βˆ€ (
g: K Γ— Q
g : 
K: Type ?u.27199
K Γ— 
Q: Type ?u.27196
Q), 
mul: {Q : Type ?u.27282} β†’
  {K : Type ?u.27281} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g (
inv: {Q : Type ?u.27297} β†’
  {K : Type ?u.27296} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q
inv 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g) = 
e: {Q : Type ?u.27363} β†’ {K : Type ?u.27362} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e
  | (
k: K
k, 
q: Q
q) => 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

mul c (k, q) (inv c (k, q)) = e
Goals accomplished! πŸ™


@[aesop unsafe (rule_sets [Metabelian])]
theorem 
mul_assoc: βˆ€ (g g' g'' : K Γ— Q), mul c (mul c g g') g'' = mul c g (mul c g' g'')
mul_assoc : βˆ€ (
g: K Γ— Q
g 
g': K Γ— Q
g' 
g'': K Γ— Q
g'' : 
K: Type ?u.41418
K Γ— 
Q: Type ?u.41415
Q), 
mul: {Q : Type ?u.41509} β†’
  {K : Type ?u.41508} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c (
mul: {Q : Type ?u.41522} β†’
  {K : Type ?u.41521} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g 
g': K Γ— Q
g') 
g'': K Γ— Q
g'' =  
mul: {Q : Type ?u.41590} β†’
  {K : Type ?u.41589} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
g: K Γ— Q
g (
mul: {Q : Type ?u.41603} β†’
  {K : Type ?u.41602} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c 
g': K Γ— Q
g' 
g'': K Γ— Q
g'')
  | (
k: K
k, 
q: Q
q), (
k': K
k', 
q': Q
q'), (
k'': K
k'', 
q'': Q
q'') => 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

mul c (mul c (k, q) (k', q')) (k'', q'') = mul c (k, q) (mul c (k', q') (k'', q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
k + ↑(Cocycle.Ξ± c q) k' + c q q' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'' =   k + (↑(Cocycle.Ξ± c q) k' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + ↑(Cocycle.Ξ± c q) (c q' q'')) + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

right
q + q' + q'' = q + (q' + q'')
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

mul c (mul c (k, q) (k', q')) (k'', q'') = mul c (k, q) (mul c (k', q') (k'', q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
k + ↑(Cocycle.Ξ± c q) k' + c q q' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'' =   k + (↑(Cocycle.Ξ± c q) k' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + ↑(Cocycle.Ξ± c q) (c q' q'')) + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

right
q + q' + q'' = q + (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
c q q' + (↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'') =   ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + (↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
k + ↑(Cocycle.Ξ± c q) k' + c q q' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'' =   k + (↑(Cocycle.Ξ± c q) k' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + ↑(Cocycle.Ξ± c q) (c q' q'')) + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

right
q + q' + q'' = q + (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
c q q' + (↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'') =   ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + (↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + (c q q' + c (q + q') q'') =   ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + (↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
c q q' + (↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'') =   ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + (↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
c q q' + c (q + q') q'' = ↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
c q q' + c (q + q') q'' = ↑(Cocycle.Ξ± c q) (c q' q'') + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

left
k + ↑(Cocycle.Ξ± c q) k' + c q q' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + c (q + q') q'' =   k + (↑(Cocycle.Ξ± c q) k' + ↑(Cocycle.Ξ± c q) (↑(Cocycle.Ξ± c q') k'') + ↑(Cocycle.Ξ± c q) (c q' q'')) + c q (q' + q'')
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

right
q + q' + q'' = q + (q' + q'')
Goals accomplished! πŸ™
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

mul c (mul c (k, q) (k', q')) (k'', q'') = mul c (k, q) (mul c (k', q') (k'', q''))
Q: Type u_2

K: Type u_1

inst: AddGroup Q

inst_1: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

q: Q

k': K

q': Q

k'': K

q'': Q

right
q + q' + q'' = q + (q' + q'')
Goals accomplished! πŸ™


/-- A group structure on `K Γ— Q` using the above multiplication operation. -/
instance 
metabelianGroup: Group (K Γ— Q)
metabelianGroup : 
Group: Type ?u.80409 β†’ Type ?u.80409
Group (
K: Type ?u.80333
K Γ— 
Q: Type ?u.80330
Q) :=
  {
    mul := 
mul: {Q : Type ?u.80429} β†’
  {K : Type ?u.80428} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q β†’ K Γ— Q
mul 
c: Q β†’ Q β†’ K
c,
    one := 
e: {Q : Type ?u.80548} β†’ {K : Type ?u.80547} β†’ [inst : AddGroup Q] β†’ [inst : AddCommGroup K] β†’ K Γ— Q
e,
    inv := 
inv: {Q : Type ?u.80632} β†’
  {K : Type ?u.80631} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’ K Γ— Q
inv 
c: Q β†’ Q β†’ K
c,

    mul_one := 
right_id: βˆ€ {Q : Type ?u.80604} {K : Type ?u.80603} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K)
  [ccl : Cocycle c] (g : K Γ— Q), mul c g e = g
right_id 
c: Q β†’ Q β†’ K
c,
    one_mul := 
left_id: βˆ€ {Q : Type ?u.80582} {K : Type ?u.80581} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K)
  [ccl : Cocycle c] (g : K Γ— Q), mul c e g = g
left_id 
c: Q β†’ Q β†’ K
c,
    mul_assoc := 
mul_assoc: βˆ€ {Q : Type ?u.80501} {K : Type ?u.80500} [inst : AddGroup Q] [inst_1 : 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'')
mul_assoc 
c: Q β†’ Q β†’ K
c,

    mul_left_inv := 
left_inv: βˆ€ {Q : Type ?u.80844} {K : Type ?u.80843} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K)
  [ccl : Cocycle c] (g : K Γ— Q), mul c (inv c g) g = e
left_inv 
c: Q β†’ Q β†’ K
c,
    div_eq_mul_inv := 
Q: Type ?u.80330

K: Type ?u.80333

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

βˆ€ (a b : K Γ— Q), a / b = a * b⁻¹
Q: Type ?u.80330

K: Type ?u.80333

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

a✝, b✝: K Γ— Q

a✝ / b✝ = a✝ * b✝⁻¹
Q: Type ?u.80330

K: Type ?u.80333

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

a✝, b✝: K Γ— Q

a✝ / b✝ = a✝ * b✝⁻¹
Q: Type ?u.80330

K: Type ?u.80333

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

βˆ€ (a b : K Γ— Q), a / b = a * b⁻¹
Goals accomplished! πŸ™

  }

@[aesop norm simp (rule_sets [Metabelian])]
theorem 
mul_def: βˆ€ {k k' : K} {q q' : Q}, (k, q) * (k', q') = (k + (q +α΅₯ k') + c q q', q + q')
mul_def {
k: K
k 
k': K
k' : 
K: Type ?u.81291
K} {
q: Q
q 
q': Q
q' : 
Q: Type ?u.81288
Q} : (
k: K
k, 
q: Q
q) * (
k': K
k', 
q': Q
q') = (
k: K
k + (
q: Q
q +α΅₯ 
k': K
k') + 
c: Q β†’ Q β†’ K
c 
q: Q
q 
q': Q
q', 
q: Q
q + 
q': Q
q') := 
rfl: βˆ€ {Ξ± : Sort ?u.82627} {a : Ξ±}, a = a
rfl

lemma 
kernel_pow: βˆ€ {Q : Type u_1} {K : Type u_2} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K) [ccl : Cocycle c] (k : K)
  (n : β„•), (k, 0) ^ n = (n β€’ k, 0)
kernel_pow (
k: K
k : 
K: Type ?u.82691
K) (
n: β„•
n : 
β„•: Type
β„•) : (
k: K
k, (
0: ?m.82781
0 : 
Q: Type ?u.82688
Q)) ^ 
n: β„•
n = (
n: β„•
n β€’ 
k: K
k, (
0: ?m.82990
0 : 
Q: Type ?u.82688
Q)) := 
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)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

zero
(k, 0) ^ Nat.zero = (Nat.zero β€’ k, 0)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

n✝: β„•

n_ih✝: (k, 0) ^ n✝ = (n✝ β€’ k, 0)

succ
(k, 0) ^ Nat.succ n✝ = (Nat.succ n✝ β€’ k, 0)
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)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

zero
(k, 0) ^ Nat.zero = (Nat.zero β€’ k, 0)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

k: K

n✝: β„•

n_ih✝: (k, 0) ^ n✝ = (n✝ β€’ k, 0)

succ
(k, 0) ^ Nat.succ n✝ = (Nat.succ n✝ β€’ k, 0)
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)
Goals accomplished! πŸ™



section Exactness

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

/-- The inclusion map from the kernel to the Metabelian group. -/
@[aesop norm unfold (rule_sets [Metabelian])]
def 
Kernel.inclusion: {Q : Type u_1} β†’
  {K : Type u_2} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ Multiplicative K β†’* K Γ— Q
Kernel.inclusion : (
Multiplicative: Type ?u.93385 β†’ Type ?u.93385
Multiplicative 
K: Type ?u.93307
K) β†’* (
K: Type ?u.93307
K Γ— 
Q: Type ?u.93304
Q) :=
  { toFun := (Β·, (0 : 
Q: Type ?u.93304
Q)),
    map_one' := 
rfl: βˆ€ {Ξ± : Sort ?u.94839} {a : Ξ±}, a = a
rfl,
    map_mul' := 
Q: Type ?u.93304

K: Type ?u.93307

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

βˆ€ (x y : Multiplicative K),
  ↑{ toFun := fun x => (x, 0), map_one' := (_ : (fun x => (x, 0)) 1 = (fun x => (x, 0)) 1) } (x * y) =     ↑{ toFun := fun x => (x, 0), map_one' := (_ : (fun x => (x, 0)) 1 = (fun x => (x, 0)) 1) } x *       ↑{ toFun := fun x => (x, 0), map_one' := (_ : (fun x => (x, 0)) 1 = (fun x => (x, 0)) 1) } y
Goals accomplished! πŸ™
 }

/-- A proof that the inclusion map is injective. -/
theorem 
Kernel.inclusion_inj: βˆ€ {Q : Type u_2} {K : Type u_1} [inst : AddGroup Q] [inst_1 : AddCommGroup K] (c : Q β†’ Q β†’ K) [ccl : Cocycle c],
  Function.Injective ↑(inclusion c)
Kernel.inclusion_inj : 
Function.Injective: {Ξ± : Sort ?u.146773} β†’ {Ξ² : Sort ?u.146772} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
Kernel.inclusion: {Q : Type ?u.146777} β†’
  {K : Type ?u.146776} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ Multiplicative K β†’* K Γ— Q
Kernel.inclusion 
c: Q β†’ Q β†’ K
c) := 
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

Function.Injective ↑(inclusion c)
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

aβ‚βœ, aβ‚‚βœ: Multiplicative K

↑(inclusion c) aβ‚βœ = ↑(inclusion c) aβ‚‚βœ β†’ aβ‚βœ = aβ‚‚βœ
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

aβ‚βœ, aβ‚‚βœ: Multiplicative K

↑(inclusion c) aβ‚βœ = ↑(inclusion c) aβ‚‚βœ β†’ aβ‚βœ = aβ‚‚βœ
Q: Type u_2

K: Type u_1

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

Function.Injective ↑(inclusion c)
Goals accomplished! πŸ™


/--- The projection map from the Metabelian group to the quotient. -/
@[aesop norm unfold (rule_sets [Metabelian])]
def 
Quotient.projection: K Γ— Q β†’* Multiplicative Q
Quotient.projection : 
K: Type ?u.149069
K Γ— 
Q: Type ?u.149066
Q β†’* (
Multiplicative: Type ?u.149149 β†’ Type ?u.149149
Multiplicative 
Q: Type ?u.149066
Q) :=
  { toFun := 
Prod.snd: {Ξ± : Type ?u.150484} β†’ {Ξ² : Type ?u.150483} β†’ Ξ± Γ— Ξ² β†’ Ξ²
Prod.snd,
    map_one' := 
rfl: βˆ€ {Ξ± : Sort ?u.150492} {a : Ξ±}, a = a
rfl
    map_mul' := 
Q: Type ?u.149066

K: Type ?u.149069

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

βˆ€ (x y : K Γ— Q),
  ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (x * y) =     ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } x *       ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } y
Q: Type ?u.149066

K: Type ?u.149069

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

fst✝¹: K

snd✝¹: Q

fst✝: K

snd✝: Q

↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } ((fst✝¹, snd✝¹) * (fst✝, snd✝)) =   ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (fst✝¹, snd✝¹) *     ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (fst✝, snd✝)
Q: Type ?u.149066

K: Type ?u.149069

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

fst✝¹: K

snd✝¹: Q

fst✝: K

snd✝: Q

↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } ((fst✝¹, snd✝¹) * (fst✝, snd✝)) =   ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (fst✝¹, snd✝¹) *     ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (fst✝, snd✝)
Q: Type ?u.149066

K: Type ?u.149069

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

βˆ€ (x y : K Γ— Q),
  ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } (x * y) =     ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } x *       ↑{ toFun := Prod.snd, map_one' := (_ : 1.snd = 1.snd) } y
Goals accomplished! πŸ™
 }

/-- A proof that the projection map is surjective. -/
theorem 
Quotient.projection_surj: Function.Surjective ↑(projection c)
Quotient.projection_surj : 
Function.Surjective: {Ξ± : Sort ?u.150912} β†’ {Ξ² : Sort ?u.150911} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Surjective (
Quotient.projection: {Q : Type ?u.150916} β†’
  {K : Type ?u.150915} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’* Multiplicative Q
Quotient.projection 
c: Q β†’ Q β†’ K
c) := 
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

Function.Surjective ↑(projection c)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

q: Multiplicative Q

βˆƒ a, ↑(projection c) a = q
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

q: Multiplicative Q

βˆƒ a, ↑(projection c) a = q
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

Function.Surjective ↑(projection c)
Goals accomplished! πŸ™


/-- A proof that the image of the first map is the kernel of the second map. -/
theorem 
exact_seq: MonoidHom.mrange (Kernel.inclusion c) = MonoidHom.mker (Quotient.projection c)
exact_seq : 
MonoidHom.mrange: {M : Type ?u.151557} β†’
  {N : Type ?u.151556} β†’
    [inst : MulOneClass M] β†’
      [inst_1 : MulOneClass N] β†’ {F : Type ?u.151555} β†’ [mc : MonoidHomClass F M N] β†’ F β†’ Submonoid N
MonoidHom.mrange (
Kernel.inclusion: {Q : Type ?u.151565} β†’
  {K : Type ?u.151564} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ Multiplicative K β†’* K Γ— Q
Kernel.inclusion 
c: Q β†’ Q β†’ K
c) = 
MonoidHom.mker: {M : Type ?u.152059} β†’
  {N : Type ?u.152058} β†’
    [inst : MulOneClass M] β†’
      [inst_1 : MulOneClass N] β†’ {F : Type ?u.152057} β†’ [mc : MonoidHomClass F M N] β†’ F β†’ Submonoid M
MonoidHom.mker (
Quotient.projection: {Q : Type ?u.152067} β†’
  {K : Type ?u.152066} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ K Γ— Q β†’* Multiplicative Q
Quotient.projection 
c: Q β†’ Q β†’ K
c) := 
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

MonoidHom.mrange (Kernel.inclusion c) = MonoidHom.mker (Quotient.projection c)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

fst✝: K

snd✝: Q

h.mk
(fst✝, snd✝) ∈ MonoidHom.mrange (Kernel.inclusion c) ↔ (fst✝, snd✝) ∈ MonoidHom.mker (Quotient.projection c)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

fst✝: K

snd✝: Q

h.mk
(fst✝, snd✝) ∈ MonoidHom.mrange (Kernel.inclusion c) ↔ (fst✝, snd✝) ∈ MonoidHom.mker (Quotient.projection c)
Q: Type u_1

K: Type u_2

inst✝¹: AddGroup Q

inst✝: AddCommGroup K

c: Q β†’ Q β†’ K

ccl: Cocycle c

MonoidHom.mrange (Kernel.inclusion c) = MonoidHom.mker (Quotient.projection c)
Goals accomplished! πŸ™


end Exactness

end MetabelianGroup