From 3bc528a17cb69ffb0f4a7d86ba444ee05fd6493e Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 14:11:42 -0600 Subject: [PATCH] Unfinished stuff. --- homology/homology.hlean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/homology/homology.hlean b/homology/homology.hlean index 6fe727b..f5e029b 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -79,6 +79,14 @@ namespace homology } end + definition Hfwehce (n : ℤ) {I : Set} (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) := + (isomorphism.mk _ (Hadditive theory n X))⁻¹ᵍ + + definition Hpwedge (n : ℤ) (A B : Type*) : HH theory n (pwedge A B) ≃g HH theory n A ×g HH theory n B := + calc HH theory n (pwedge A B) ≃g HH theory n (fwedge (bool.rec A B)) : by exact sorry + ... ≃g dirsum (λb, HH theory n (bool.rec A B b)) : by exact sorry + ... ≃g HH theory n A ×g HH theory n B : by exact sorry + end /- homology theory associated to a spectrum -/