michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add homology_ordinary_theory and copyright statement.

Browse source
This commit is contained in:
favonia 2017-06-08 09:54:47 -06:00
parent 5b384882f8
commit a8592e0184
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
homology/homology.hlean
View file

@ -1,3 +1,11 @@
/-
Copyright (c) 2017 Yuri Sulyma, Favonia
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuri Sulyma, Favonia
Reduced homology theories
-/
import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
@ -20,6 +28,9 @@ namespace homology
(Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
(dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X))) (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} :=
(Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0))))
section section
parameter (theory : homology_theory) parameter (theory : homology_theory)
open homology_theory open homology_theory