From b45e20d0ccab06f69257397fd5723bd6a4aeda02 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 9 Sep 2016 16:43:09 -0400 Subject: [PATCH] feat(cohomology): start on cohomology file --- homotopy/cohomology.hlean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 homotopy/cohomology.hlean diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean new file mode 100644 index 0000000..bd09458 --- /dev/null +++ b/homotopy/cohomology.hlean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2016 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +Reduced cohomology +-/ + +import .EM + +open spectrum int trunc pointed EM group algebra circle sphere + +definition cohomology [reducible] (X : Type*) (Y : spectrum) (n : ℤ) : Set := +ttrunc 0 (X →* Ω[2] (Y (n+2))) + +definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : Set := +cohomology X (EM_spectrum G) n + +definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : Set := +ordinary_cohomology X agℤ n + +notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n +notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n + +check H^3[S¹.,EM_spectrum agℤ] +check H^3[S¹.]