cohomology: define cohomology as abelian groups and define the functorial action

algebra/arrow_group.hlean

@@ -0,0 +1,60 @@
+
+import algebra.group_theory ..move_to_lib
+open pi pointed algebra group eq equiv is_trunc
+
+namespace group
+
+  /- Group of functions whose codomain is a group -/
+  definition group_arrow [instance] (A B : Type) [group B] : group (A → B) :=
+  begin
+    fapply group.mk,
+    { intro f g a, exact f a * g a },
+    { apply is_trunc_arrow },
+    { intros, apply eq_of_homotopy, intro a, apply mul.assoc },
+    { intro a, exact 1 },
+    { intros, apply eq_of_homotopy, intro a, apply one_mul },
+    { intros, apply eq_of_homotopy, intro a, apply mul_one },
+    { intro f a, exact (f a)⁻¹ },
+    { intros, apply eq_of_homotopy, intro a, apply mul.left_inv }
+  end
+
+  definition Group_arrow (A : Type) (G : Group) : Group :=
+  Group.mk (A → G) _
+
+  definition comm_group_arrow [instance] (A B : Type) [comm_group B] : comm_group (A → B) :=
+  ⦃comm_group, group_arrow A B,
+     mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄
+
+  definition CommGroup_arrow (A : Type) (G : CommGroup) : CommGroup :=
+  CommGroup.mk (A → G) _
+
+  definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) :=
+  begin
+    fapply pgroup.mk,
+    { intro f g, apply pmap.mk (λa, f a * g a),
+      exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul },
+    { apply is_trunc_pmap },
+    { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc },
+    { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt },
+    { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul },
+    { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one },
+    { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv }
+  end
+
+  definition Group_pmap (A : Type*) (G : Group) : Group :=
+  Group_of_pgroup (ppmap A (pType_of_Group G))
+
+  definition CommGroup_pmap (A : Type*) (G : CommGroup) : CommGroup :=
+  CommGroup.mk (A →* pType_of_Group G)
+  ⦃ comm_group, Group.struct (Group_pmap A G),
+    mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄
+
+  definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : CommGroup) :
+    Group_pmap A G →g Group_pmap A' G :=
+  begin
+    fapply homomorphism.mk,
+    { intro g, exact g ∘* f},
+    { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity }
+  end
+
+end group

homotopy/cohomology.hlean

@@ -6,17 +6,17 @@ Authors: Floris van Doorn
 Reduced cohomology
 -/
 
-import .EM
+import .EM algebra.arrow_group
 
-open spectrum int trunc pointed EM group algebra circle sphere
+open eq spectrum int trunc pointed EM group algebra circle sphere nat
 
-definition cohomology [reducible] (X : Type*) (Y : spectrum) (n : ℤ) : Set :=
-ttrunc 0 (X →* Ω[2] (Y (n+2)))
+definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup :=
+CommGroup_pmap X (πag[2] (Y (2+n)))
 
-definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : Set :=
+definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : CommGroup :=
 cohomology X (EM_spectrum G) n
 
-definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : Set :=
+definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : CommGroup :=
 ordinary_cohomology X agℤ n
 
 notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n
@@ -24,3 +24,19 @@ notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n
 
 check H^3[S¹*,EM_spectrum agℤ]
 check H^3[S¹*]
+
+definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : CommGroup :=
+cohomology X₊ Y n
+
+definition cohomology_homomorphism [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
+  (n : ℤ) : cohomology X Y n →g cohomology X' Y n :=
+Group_pmap_homomorphism f (πag[2] (Y (2+n)))
+
+definition cohomology_homomorphism_id (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) :
+  cohomology_homomorphism (pid X) Y n f ~* f :=
+!pcompose_pid
+
+definition cohomology_homomorphism_compose {X X' X'' : Type*} (g : X'' →* X') (f : X' →* X)
+  (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_homomorphism (f ∘* g) Y n h ~*
+  cohomology_homomorphism g Y n (cohomology_homomorphism f Y n h) :=
+!passoc⁻¹*

move_to_lib.hlean

@@ -21,6 +21,10 @@ open sigma
 
 namespace group
   open is_trunc
+
+  theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 :=
+  iff.mpr (inv_eq_one_iff_eq_one a) H
+
   definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1
 
   definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group}
@@ -41,6 +45,20 @@ namespace group
     (φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ :=
   homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h))
 
+  definition Group_of_pgroup (G : Type*) [pgroup G] : Group :=
+  Group.mk G _
+
+  definition pgroup_pType_of_Group [instance] (G : Group) : pgroup (pType_of_Group G) :=
+  ⦃ pgroup, Group.struct G,
+    pt_mul := one_mul,
+    mul_pt := mul_one,
+    mul_left_inv_pt := mul.left_inv ⦄
+
+  definition comm_group_pType_of_Group [instance] (G : CommGroup) : comm_group (pType_of_Group G) :=
+  CommGroup.struct G
+
+  abbreviation gid [constructor] := @homomorphism_id
+
 end group open group
 
 namespace pi -- move to types.arrow
@@ -96,6 +114,16 @@ namespace pointed
     all_goals reflexivity
   end
 
+  definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] : is_trunc n (A →* B) :=
+  is_trunc_equiv_closed_rev _ !pmap.sigma_char
+
+  definition is_trunc_ppmap [instance] (n : ℕ₋₂) {A B : Type*} [is_trunc n B] :
+    is_trunc n (ppmap A B) :=
+  !is_trunc_pmap
+
+  definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g :=
+  pmap_eq p !is_set.elim
+
   definition phomotopy.sigma_char [constructor] {A B : Type*} (f g : A →* B) : (f ~* g) ≃ Σ(p : f ~ g), p pt ⬝ resp_pt g = resp_pt f :=
   begin
     fapply equiv.MK : intros h,