Merge remote-tracking branch 'origin/master'

# Conflicts:
#	group_theory/basic.hlean

README.md

@@ -28,6 +28,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
 
 ### Topology To Do:
+- HoTT Book chapter 8
 - fiber and cofiber sequences (is this in the library already?)
 - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
 - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)

group_theory/basic.hlean

@@ -13,14 +13,22 @@ Basic group theory
   The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
 -/
 
+<<<<<<< HEAD
 import algebra.group types.pointed types.pi
 
 open eq algebra pointed function is_trunc pi
 
+=======
+import types.pointed types.pi algebra.bundled algebra.category.category
+
+open eq algebra pointed function is_trunc pi category equiv is_equiv
+set_option class.force_new true
+>>>>>>> origin/master
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
   definition Pointed_of_Group (G : Group) : Type* := pointed.mk' G
+  definition hset_of_Group (G : Group) : hset := trunctype.mk G _
 
  -- print Type*
  -- print Pointed
@@ -43,7 +51,7 @@ namespace group
   abbreviation respect_mul := @homomorphism.p
   infix ` →g `:55 := homomorphism
 
-  variables {G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ φ' : G₁ →g G₂}
+  variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ φ' : G₁ →g G₂}
 
   theorem respect_one (φ : G₁ →g G₂) : φ 1 = 1 :=
   mul.right_cancel
@@ -55,8 +63,19 @@ 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₂ :=
+  definition is_hset_homomorphism [instance] (G₁ G₂ : Group) : is_hset (homomorphism G₁ G₂) :=
+  begin
+    assert H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
+    { fapply equiv.MK,
+      { intro φ, induction φ, constructor, assumption},
+      { intro v, induction v, constructor, assumption},
+      { intro v, induction v, reflexivity},
+      { intro φ, induction φ, reflexivity}},
+    apply is_trunc_equiv_closed_rev, exact H
+  end
+
+  definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂)
+    : Pointed_of_Group G₁ →* Pointed_of_Group G₂ :=
   pmap.mk φ !respect_one
 
   definition homomorphism_eq (p : group_fun φ ~ group_fun φ') : φ = φ' :=
@@ -67,16 +86,75 @@ namespace group
 
   /- categorical structure of groups + homomorphisms -/
 
-  definition homomorphism_compose [constructor] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ → G₃ :=
+  definition homomorphism_compose [constructor] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ :=
   homomorphism.mk (ψ ∘ φ) (λg h, ap ψ !respect_mul ⬝ !respect_mul)
 
-  definition homomorphism_id [constructor] (G : Group) : G → G :=
+  definition homomorphism_id [constructor] (G : Group) : G →g G :=
   homomorphism.mk id (λg h, idp)
 
+  infixr ` ∘g `:75 := homomorphism_compose
+  notation 1       := homomorphism_id _
 
+  structure isomorphism (A B : Group) :=
+    (to_hom : A →g B)
+    (is_equiv_to_hom : is_equiv to_hom)
 
-  -- TODO: maybe define this in more generality for pointed types?
-  definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _
+  infix ` ≃g `:25 := isomorphism
+  attribute isomorphism.to_hom [coercion]
+  attribute isomorphism.is_equiv_to_hom [instance]
 
+  definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ :=
+  equiv.mk φ _
+
+  definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ :=
+  homomorphism.mk φ⁻¹
+    abstract begin
+    intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
+    rewrite [respect_mul, +right_inv φ]
+    end end
+
+  definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=
+  isomorphism.mk 1 !is_equiv_id
+
+  definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ :=
+  isomorphism.mk (to_ginv φ) !is_equiv_inv
+
+  definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃)
+    : G₁ ≃g G₃ :=
+  isomorphism.mk (ψ ∘g φ) !is_equiv_compose
+
+  postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
+  infixl ` ⬝g `:75 := isomorphism.trans
+
+  -- TODO
+  -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) :=
+  -- begin
+  --   fapply equiv.MK,
+  --   { intro φ, fapply Group_eq, apply equiv_of_isomorphism φ, apply respect_mul},
+  --   { intro p, apply transport _ p, reflexivity},
+  --   { intro p, induction p, esimp, },
+  --   { }
+  -- end
+
+  /- category of groups -/
+
+  definition precategory_group [constructor] : precategory Group :=
+  precategory.mk homomorphism
+                 @homomorphism_compose
+                 @homomorphism_id
+                 (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp))
+                 (λG₁ G₂ φ, homomorphism_eq (λg, idp))
+                 (λG₁ G₂ φ, homomorphism_eq (λg, idp))
+
+  -- TODO
+  -- definition category_group : category Group :=
+  -- category.mk precategory_group
+  -- begin
+  --   intro G₁ G₂,
+  --   fapply adjointify,
+  --   { intro φ, fapply Group_eq, },
+  --   { },
+  --   { }
+  -- end
 
 end group

group_theory/constructions.hlean

@@ -31,7 +31,7 @@ namespace group
   abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup_rel.is_normal
 
   variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
-            {A : CommGroup}
+            {A B : CommGroup}
 
   theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) :=
   inv_inv h ▸ is_normal_subgroup N h⁻¹ r
@@ -596,5 +596,84 @@ namespace group
         exact !respect_inv⁻¹}}
   end
 
+  /- Free Commutative Group of a set -/
+
+/-  namespace tensor_group
+  variables {A B}
+  local abbreviation ι := @free_comm_group_inclusion
+
+  inductive tensor_rel_type : free_comm_group (hset_of_Group A ×t hset_of_Group B) → Type :=
+  | mul_left  : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b)  * ι (a₂, b)  * (ι (a₁ * a₂, b))⁻¹)
+  | mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁)  * ι (a, b₂)  * (ι (a, b₁ * b₂))⁻¹)
+
+  open tensor_rel_type
+
+  definition tensor_rel' (x : free_comm_group (hset_of_Group A ×t hset_of_Group B)) : hprop :=
+  ∥ tensor_rel_type x ∥
+
+  definition tensor_group_rel (A B : CommGroup)
+    : normal_subgroup_rel (free_comm_group (hset_of_Group A ×t hset_of_Group B)) :=
+  sorry /- relation generated by tensor_rel'-/
+
+  definition tensor_group [constructor] : CommGroup :=
+  quotient_comm_group (tensor_group_rel A B)
+
+  end tensor_group-/
+
+  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) _
+
+  theorem 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
+
+  theorem 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 [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
+  ⦃ subgroup_rel,
+    R := kernel φ,
+    Rone := respect_one φ,
+    Rmul := kernel_mul φ,
+    Rinv := kernel_inv φ
+  ⦄
+
+  theorem kernel_subgroup_isnormal (φ : G₁ →g G₂) (g : G₁) (h : G₁)
+    : kernel φ g → kernel φ (h * g * h⁻¹) :=
+  begin
+    esimp at *,
+    intro p,
+    exact calc
+      φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹)   : respect_mul
+                  ... = (φ h) * (φ g) * (φ h⁻¹) : respect_mul
+                  ... = (φ h) * 1 * (φ h⁻¹)     : p
+                  ... = (φ h) * (φ h⁻¹)         : mul_one
+                  ... = (φ h) * (φ h)⁻¹         : respect_inv
+                  ... = 1                       : mul.right_inv
+  end
+
+  definition kernel_normal_subgroup [constructor] (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
+  ⦃ normal_subgroup_rel,
+    kernel_subgroup φ,
+    is_normal := kernel_subgroup_isnormal φ
+  ⦄
+
+  end kernels
 
 end group