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.Data.Fin.Basic
import Mathlib.Algebra.Hom.Group
import UnitConjecture.MetabelianGroup
import UnitConjecture.AddFreeGroup

/-!
## The construction of the group `P`

We construct the group `P` (the *Promislow* or *Hantzsche–Wendt* group) as a Metabelian group.

This is done via the cocycle construction, using the explicit action and cocycle described in 
Section 3.1 of Giles Gardam's paper (https://arxiv.org/abs/2102.11818).
-/

section Components

declare_aesop_rule_sets [P]

/-! 
### The components of the group `P`
The group `P` is constructed as a Metabelian group with kernel `K := β„€Β³` and quotient `Q := β„€/2 Γ— β„€/2`. 
-/

/-! The *kernel* group -/

/-- The *kernel* group - `β„€Β³`, the free Abelian group on three generators. -/
@[aesop safe (rule_sets [P])]
abbrev 
K: Type
K := 
β„€: Type
β„€ Γ— 
β„€: Type
β„€ Γ— 
β„€: Type
β„€

instance 
KGrp: AddCommGroup K
KGrp : 
AddCommGroup: Type ?u.12 β†’ Type ?u.12
AddCommGroup 
K: Type
K := 
inferInstance: {Ξ± : Sort ?u.14} β†’ [i : Ξ±] β†’ Ξ±
inferInstance

/-- Equality of endomorphisms of `K` is decidable, as `K` is a free group with basis `Unit βŠ• Unit βŠ• Unit`.  -/

instance: DecidableEq (K β†’+ K)
instance : 
DecidableEq: Sort ?u.295 β†’ Sort (max1?u.295)
DecidableEq (
K: Type
K β†’+ 
K: Type
K) := 
decideHomsEqual: {F : Type ?u.333} β†’
  [inst : AddCommGroup F] β†’
    {X : Type ?u.332} β†’
      [inst_1 : EnumDecide.DecideForall X] β†’
        [fgp : AddFreeGroup F X] β†’
          {A : Type} β†’ [inst_2 : AddCommGroup A] β†’ [inst_3 : DecidableEq A] β†’ DecidableEq (F β†’+ A)
decideHomsEqual (X := 
Unit: Type
Unit βŠ• 
Unit: Type
Unit βŠ• 
Unit: Type
Unit)


/-! The *quotient* group -/

/-- The *quotient* group - `β„€/2 Γ— β„€/2`, the Klein Four group. -/
@[aesop safe (rule_sets [P])]
abbrev 
Q: ?m.1442
Q := 
Fin: β„• β†’ Type
Fin 
2: ?m.1447
2 Γ— 
Fin: β„• β†’ Type
Fin 
2: ?m.1457
2

instance 
QGrp: AddCommGroup Q
QGrp : 
AddCommGroup: Type ?u.1463 β†’ Type ?u.1463
AddCommGroup 
Q: Type
Q := 
inferInstance: {Ξ± : Sort ?u.1465} β†’ [i : Ξ±] β†’ Ξ±
inferInstance

section Elements

/-!
### The group elements
-/

namespace K

/-! The generators of the free Abelian group `K`. -/

/-- The first generator of `K`. -/
@[aesop norm unfold (rule_sets [P])]
abbrev 
x: K
x : 
K: Type
K := (
1: ?m.1889
1, 
0: ?m.1904
0, 
0: ?m.1911
0)
/-- The second generator of `K`. -/
@[aesop norm unfold (rule_sets [P])]
abbrev 
y: K
y : 
K: Type
K := (
0: ?m.1975
0, 
1: ?m.1990
1, 
0: ?m.1997
0)
/-- The third generator of `K`. -/
@[aesop norm unfold (rule_sets [P])]
abbrev 
z: K
z : 
K: Type
K := (
0: ?m.2052
0, 
0: ?m.2067
0, 
1: ?m.2070
1)

end K


namespace Q

/-! The elements of the Klein Four group `Q`. -/

/-- The identity element of `Q`. -/
@[aesop norm unfold (rule_sets [P]), match_pattern]
abbrev 
e: Q
e : 
Q: Type
Q := (⟨
0: ?m.2134
0, 
0 < 2
Goals accomplished! πŸ™
⟩, ⟨
0: ?m.2150
0, 
0 < 2
Goals accomplished! πŸ™
⟩)
/-- The first generator of `Q`. -/
@[aesop norm unfold (rule_sets [P]), match_pattern]
abbrev 
a: Q
a : 
Q: Type
Q := (⟨
1: ?m.2238
1, 
1 < 2
Goals accomplished! πŸ™
⟩, ⟨
0: ?m.2254
0, 
0 < 2
Goals accomplished! πŸ™
⟩)
/-- The second generator of `Q`. -/
@[aesop norm unfold (rule_sets [P]), match_pattern]
abbrev 
b: Q
b : 
Q: Type
Q := (⟨
0: ?m.2367
0, 
0 < 2
Goals accomplished! πŸ™
⟩, ⟨
1: ?m.2383
1, 
1 < 2
Goals accomplished! πŸ™
⟩)
/-- The product of the first two generators of `Q`. -/
@[aesop safe (rule_sets [P]), match_pattern]
abbrev 
c: Q
c : 
Q: Type
Q := (⟨
1: ?m.2496
1, 
1 < 2
Goals accomplished! πŸ™
⟩, ⟨
1: ?m.2512
1, 
1 < 2
Goals accomplished! πŸ™
⟩)

end Q


end Elements

end Components


section Action

/-! 
### The action of `Q` on `K` by automorphisms  
The action of the group `Q` on the kernel `K` by automorphisms required for constructing `P`. 
-/

/-- An abbreviation for the negation homomorphism on commutative groups. -/
@[aesop norm unfold (rule_sets [P])]
abbrev 
neg: (Ξ± : Type ?u.2596) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ ?m.2603 Ξ±
neg (
Ξ±: Type ?u.2596
Ξ± : 
Type _: Type (?u.2596+1)
Type _) [
SubtractionCommMonoid: Type ?u.2599 β†’ Type ?u.2599
SubtractionCommMonoid 
Ξ±: Type ?u.2596
Ξ±] := 
negAddMonoidHom: {Ξ± : Type ?u.2607} β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
negAddMonoidHom (Ξ± := 
Ξ±: Type ?u.2596
Ξ±)

attribute [aesop norm unfold (rule_sets [P])] 
negAddMonoidHom: {Ξ± : Type u_1} β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
negAddMonoidHom

/-- A temporary notation for easily describing products of additive monoid homomorphisms. -/
local infixr:100 " Γ— " => 
AddMonoidHom.prodMap: {M : Type u_1} β†’
  {N : Type u_2} β†’
    [inst : AddZeroClass M] β†’
      [inst_1 : AddZeroClass N] β†’
        {M' : Type u_3} β†’
          {N' : Type u_4} β†’
            [inst_2 : AddZeroClass M'] β†’ [inst_3 : AddZeroClass N'] β†’ (M β†’+ M') β†’ (N β†’+ N') β†’ M Γ— N β†’+ M' Γ— N'
AddMonoidHom.prodMap

/-- The action of `Q` on `K` by automorphisms.
The action can be given a component-wise description in terms of `id` and `neg`, the identity and negation homomorphisms. -/
@[aesop norm unfold (rule_sets [P]), reducible] 
def 
action: Q β†’ K β†’+ K
action : 
Q: Type
Q β†’ (
K: Type
K β†’+ 
K: Type
K)
  | 
.e: Q
.e =>  
.id: (M : Type ?u.12036) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€  Γ—  
.id: (M : Type ?u.12135) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€  Γ—  
.id: (M : Type ?u.12137) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€
  | 
.a: Q
.a =>  
.id: (M : Type ?u.12253) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€  Γ—  
neg: (Ξ± : Type ?u.12343) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€  Γ—  
neg: (Ξ± : Type ?u.12375) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€
  | 
.b: Q
.b =>  
neg: (Ξ± : Type ?u.12475) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€  Γ—  
.id: (M : Type ?u.12569) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€  Γ—  
neg: (Ξ± : Type ?u.12571) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€
  | 
.c: Q
.c =>  
neg: (Ξ± : Type ?u.15224) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€  Γ—  
neg: (Ξ± : Type ?u.15318) β†’ [inst : SubtractionCommMonoid Ξ±] β†’ Ξ± β†’+ Ξ±
neg 
β„€: Type
β„€  Γ—  
.id: (M : Type ?u.15324) β†’ [inst : AddZeroClass M] β†’ M β†’+ M
.id 
β„€: Type
β„€

/-- A verification that the above action is indeed an action by automorphisms.
  This is done automatically with the machinery of decidable equality of homomorphisms on free groups. -/

instance: AutAction action
instance : 
AutAction: {A : Type ?u.24646} β†’ {B : Type ?u.24645} β†’ [inst : AddGroup A] β†’ [inst : AddGroup B] β†’ (A β†’ B β†’+ B) β†’ Type
AutAction 
action: Q β†’ K β†’+ K
action :=
  { id_action := 
rfl: βˆ€ {Ξ± : Sort ?u.24832} {a : Ξ±}, a = a
rfl
    compatibility := 
βˆ€ (a a' : Q), action (a + a') = AddMonoidHom.comp (action a) (action a')
Goals accomplished! πŸ™
 }

end Action


section Cocycle

/-! ### The cocycle -/

open K Q in
/-- The cocycle in the construction of `P`. -/
@[aesop norm unfold (rule_sets [P]), reducible]
def 
cocycle: Q β†’ Q β†’ K
cocycle : 
Q: Type
Q β†’ 
Q: Type
Q β†’ 
K: Type
K
  | 
a: Fin 2 Γ— Fin 2
a , 
a: Q
a  => 
x: K
x
  | 
a: Fin 2 Γ— Fin 2
a , 
c: Fin 2 Γ— Fin 2
c  => 
x: K
x
  | 
b: Fin 2 Γ— Fin 2
b , 
b: Fin 2 Γ— Fin 2
b  => 
y: K
y
  | 
c: Fin 2 Γ— Fin 2
c , 
b: Fin 2 Γ— Fin 2
b  => -
y: K
y
  | 
c: Q
c , 
c: Fin 2 Γ— Fin 2
c  => 
z: K
z
  | 
b: Q
b , 
c: Fin 2 Γ— Fin 2
c  => -
x: K
x + -
z: K
z
  | 
c: Q
c , 
a: Q
a  => -
y: K
y + 
z: K
z
  | 
b: Fin 2 Γ— Fin 2
b , 
a: Fin 2 Γ— Fin 2
a  => -
x: K
x + 
y: K
y + -
z: K
z
  | _ , _  => 
0: ?m.31421
0

/-- A verification that the `cocycle` function indeed satisfies the cocycle condition.
  This check is performed fully automatically using previously defined decision procedures. -/
instance 
P_cocycle: Cocycle cocycle
P_cocycle : 
Cocycle: {Q : Type ?u.37883} β†’
  {K : Type ?u.37882} β†’ [inst : AddGroup Q] β†’ [inst : AddGroup K] β†’ (Q β†’ Q β†’ K) β†’ Type (max?u.37883?u.37882)
Cocycle 
cocycle: Q β†’ Q β†’ K
cocycle :=
  { Ξ± := 
action: Q β†’ K β†’+ K
action
    autAct := 
inferInstance: {Ξ± : Sort ?u.38041} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
    cocycle_zero := 
rfl: βˆ€ {Ξ± : Sort ?u.38051} {a : Ξ±}, a = a
rfl
    cocycle_condition := 
βˆ€ (q q' q'' : Q), cocycle q q' + cocycle (q + q') q'' = q +α΅₯ cocycle q' q'' + cocycle q (q' + q'')
Goals accomplished! πŸ™
 }

end Cocycle


section MetabelianGroup

/-! 
### The construction of `P`
The construction of the group `P` as a Metabelian group from the given action and cocycle.
-/

/-- the group `P` constructed via the cocycle construction -/
@[aesop norm unfold (rule_sets [P])]
def 
P: Type
P := 
K: Type
K Γ— 
Q: Type
Q

namespace P

instance (priority := high) 
PGrp: Group P
PGrp : 
Group: Type ?u.69897 β†’ Type ?u.69897
Group 
P: Type
P := 
MetabelianGroup.metabelianGroup: {Q : Type ?u.69900} β†’
  {K : Type ?u.69899} β†’
    [inst : AddGroup Q] β†’ [inst_1 : AddCommGroup K] β†’ (c : Q β†’ Q β†’ K) β†’ [ccl : Cocycle c] β†’ Group (K Γ— Q)
MetabelianGroup.metabelianGroup 
cocycle: Q β†’ Q β†’ K
cocycle

-- Priorities to resolve the conflict between the direct product and Metabelian group structure on `K Γ— Q` 
scoped 
instance: HMul (K Γ— Q) (K Γ— Q) (K Γ— Q)
instance (priority := high) : 
HMul: Type ?u.70494 β†’ Type ?u.70493 β†’ outParam (Type ?u.70492) β†’ Type (max(max?u.70494?u.70493)?u.70492)
HMul (
K: Type
K Γ— 
Q: Type
Q) (
K: Type
K Γ— 
Q: Type
Q) (
K: Type
K Γ— 
Q: Type
Q) := ⟨
PGrp: Group P
PGrp.
mul: {Ξ± : Type ?u.70527} β†’ [self : Mul Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
mul⟩
scoped 
instance: Mul (K Γ— Q)
instance (priority := high) : 
Mul: Type ?u.71100 β†’ Type ?u.71100
Mul (
K: Type
K Γ— 
Q: Type
Q) := ⟨
PGrp: Group P
PGrp.
mul: {Ξ± : Type ?u.71121} β†’ [self : Mul Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
mul⟩
scoped 
instance: Pow (K Γ— Q) β„•
instance (priority := high + 1) : 
Pow: Type ?u.71553 β†’ Type ?u.71552 β†’ Type (max?u.71553?u.71552)
Pow (
K: Type
K Γ— 
Q: Type
Q) 
β„•: Type
β„• := 
PGrp: Group P
PGrp.
toMonoid: {G : Type ?u.71560} β†’ [self : DivInvMonoid G] β†’ Monoid G
toMonoid.
Pow: {M : Type ?u.71563} β†’ [inst : Monoid M] β†’ Pow M β„•
Pow


instance: DecidableEq P
instance : 
DecidableEq: Sort ?u.71891 β†’ Sort (max1?u.71891)
DecidableEq 
P: Type
P := 
inferInstanceAs: (Ξ± : Sort ?u.71895) β†’ [i : Ξ±] β†’ Ξ±
inferInstanceAs <| 
DecidableEq: Sort ?u.71896 β†’ Sort (max1?u.71896)
DecidableEq (
K: Type
K Γ— 
Q: Type
Q)

/-- A confirmation that multiplication in `P` is as expected from the Metabelian group structure. -/
@[aesop norm (rule_sets [P]), simp]
theorem 
mul: βˆ€ (k k' : K) (q q' : Q), (k, q) * (k', q') = (k + ↑(action q) k' + cocycle q q', q + q')
mul (
k: K
k 
k': K
k' : 
K: Type
K) (
q: Q
q 
q': Q
q' : 
Q: Type
Q) : (
k: K
k, 
q: Q
q) * (
k': K
k', 
q': Q
q') = (
k: K
k + 
action: Q β†’ K β†’+ K
action 
q: Q
q 
k': K
k' + 
cocycle: Q β†’ Q β†’ K
cocycle 
q: Q
q 
q': Q
q', 
q: Q
q + 
q': Q
q') := 
rfl: βˆ€ {Ξ± : Sort ?u.73697} {a : Ξ±}, a = a
rfl

@[aesop norm (rule_sets [P])]
theorem 
one: 1 = ((0, 0, 0), Q.e)
one : (
1: ?m.73929
1 : 
P: Type
P) = ((
0: ?m.74201
0, 
0: ?m.74215
0, 
0: ?m.74225
0), 
Q.e: Q
Q.e) := 
rfl: βˆ€ {Ξ± : Sort ?u.77001} {a : Ξ±}, a = a
rfl 

end P

end MetabelianGroup