From daf34724689d753b2dfa921db869525d7de4cc74 Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 14:02:28 -0600
Subject: [PATCH] Start proving that the homology theory associated to a
 spectrum satisfies the ES axioms

---
 homology/homology.hlean | 53 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 32e79f8..ed8eeff 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -70,4 +70,57 @@ namespace homology
 
   end
 
+/- homology theory associated to a spectrum -/
+definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup :=
+shomotopy_group n (smash_spectrum X E)
+
+definition parametrized_homology {X : Type*} (E : X → spectrum) (n : ℤ) : AbGroup :=
+sorry
+
+definition ordinary_homology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
+homology X (EM_spectrum G) n
+
+definition ordinary_homology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup :=
+ordinary_homology X agℤ n
+
+notation `H_` n `[`:0 X:0 `, ` E:0 `]`:0 := homology X E n
+notation `H_` n `[`:0 X:0 `]`:0 := ordinary_homology_Z X n
+notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`:0 := r
+
+definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup :=
+H_ n[X₊, E]
+
+definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
+shomotopy_group_fun n (smash_spectrum_fun f g)
+
+definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} :=
+begin
+  refine homology_theory.mk _ _ _ _ _ _ _ _,
+  exact (λn X, H_ n[X, E]),
+  exact (λn X Y f, homology_functor f (sid E) n),
+  exact sorry, -- Hid is uninteresting but potentially very hard to prove
+  exact sorry,
+  exact sorry,
+  exact sorry,
+  exact sorry,
+  exact sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+--  (λn A, H^n[A, Y])
+--  (λn A B f, cohomology_isomorphism f Y n)
+--  (λn A, cohomology_isomorphism_refl A Y n)
+--  (λn A B f, cohomology_functor f Y n)
+--  (λn A B f g p, cohomology_functor_phomotopy p Y n)
+--  (λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
+--  (λn A x, cohomology_functor_pid A Y n x)
+--  (λn A B C g f x, cohomology_functor_pcompose g f Y n x)
+--  (λn A, cohomology_psusp A Y n)
+--  (λn A B f, cohomology_psusp_natural f Y n)
+--  (λn A B f, cohomology_exact f Y n)
+--  (λn I A H, spectrum_additive H A Y n)
+end
 end homology