From fa25173a38557238a0f1f0dd868cbcc0c7a3aa16 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 10 Dec 2015 16:36:10 -0500
Subject: [PATCH] kernels

---
 group_theory/basic.hlean         | 12 +++--------
 group_theory/constructions.hlean | 36 +++++++++++++++++++++++++++++++-
 2 files changed, 38 insertions(+), 10 deletions(-)

diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean
index 9da1d98..f1dc834 100644
--- a/group_theory/basic.hlean
+++ b/group_theory/basic.hlean
@@ -54,9 +54,9 @@ namespace group
   theorem respect_inv (φ : G₁ →g G₂) (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
   eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
 
-  local attribute Pointed_of_Group [coercion]
-  definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂) : G₁ →* G₂ :=
-  pmap.mk φ !respect_one
+  --local attribute Pointed_of_Group [coercion]
+  --definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂) : G₁ →* G₂ :=
+  --pmap.mk φ !respect_one
 
   definition homomorphism_eq (p : group_fun φ ~ group_fun φ') : φ = φ' :=
   begin
@@ -72,10 +72,4 @@ namespace group
   definition homomorphism_id [constructor] (G : Group) : G → G :=
   homomorphism.mk id (λg h, idp)
 
-
-
-  -- TODO: maybe define this in more generality for pointed types?
-  definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _
-
-
 end group
diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 39dd861..2e1b242 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -8,7 +8,7 @@ Constructions of groups
 
 import .basic hit.set_quotient types.sigma types.list types.sum
 
-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
+open eq algebra is_trunc pi pointed set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
      equiv
 set_option class.force_new true
 namespace group
@@ -597,5 +597,39 @@ namespace group
         exact !respect_inv⁻¹}}
   end
 
+  section kernels
 
+  variables {G₁ G₂ : Group}
+
+  -- TODO: maybe define this in more generality for pointed types?
+  definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _
+
+  definition kernel_mul (φ : G₁ →g G₂) (g h : G₁) (H₁ : kernel φ g) (H₂ : kernel φ h) : kernel φ (g *[G₁] h) :=
+  begin
+    esimp at *,
+    exact calc
+      φ (g * h) = (φ g) * (φ h) : respect_mul
+            ... = 1 * (φ h)     : H₁
+            ... = 1 * 1         : H₂
+            ... = 1             : one_mul
+  end
+
+  definition kernel_inv (φ : G₁ →g G₂) (g : G₁) (H : kernel φ g) : kernel φ (g⁻¹) :=
+  begin
+    esimp at *,
+    exact calc
+      φ g⁻¹ = (φ g)⁻¹ : respect_inv
+        ... = 1⁻¹     : H
+        ... = 1       : one_inv
+  end
+
+  definition kernel_subgroup (φ : G₁ →g G₂) : subgroup_rel G₁ :=
+  ⦃ subgroup_rel,
+    R := kernel φ,
+    Rone := respect_one φ,
+    Rmul := kernel_mul φ,
+    Rinv := kernel_inv φ
+  ⦄
+
+  end kernels
 end group