From ead933e0a90d84f41698a820408246fdbbcdc653 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 17 Jul 2017 15:54:05 +0100 Subject: [PATCH] move spectrum files to separate directory --- algebra/spectral_sequence.hlean | 2 +- cohomology/basic.hlean | 2 +- cohomology/serre.hlean | 2 +- homology/basic.hlean | 2 +- homotopy/pointed_cubes.hlean => pointed_cubes.hlean | 2 +- homotopy/spectrum.hlean => spectrum/basic.hlean | 3 ++- homotopy/smash_spectrum.hlean => spectrum/smash.hlean | 2 +- {homotopy => spectrum}/spectrification.hlean | 2 +- homotopy/strunc.hlean => spectrum/trunc.hlean | 2 +- 9 files changed, 10 insertions(+), 9 deletions(-) rename homotopy/pointed_cubes.hlean => pointed_cubes.hlean (99%) rename homotopy/spectrum.hlean => spectrum/basic.hlean (99%) rename homotopy/smash_spectrum.hlean => spectrum/smash.hlean (97%) rename {homotopy => spectrum}/spectrification.hlean (99%) rename homotopy/strunc.hlean => spectrum/trunc.hlean (99%) diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index e56a60e..58f0fe1 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -5,7 +5,7 @@ -- Author: Floris van Doorn -import .graded ..homotopy.spectrum .product_group +import .graded ..spectrum.basic .product_group open algebra is_trunc left_module is_equiv equiv eq function nat sigma sigma.ops set_quotient diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 07b1f55..58bf35b 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Ulrik Buchholtz Reduced cohomology of spectra and cohomology theories -/ -import ..homotopy.spectrum ..algebra.arrow_group homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group +import ..spectrum.basic ..algebra.arrow_group ..homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 4f984dc..0de3132 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -1,4 +1,4 @@ -import ..algebra.spectral_sequence ..homotopy.strunc .basic +import ..algebra.spectral_sequence ..spectrum.trunc .basic open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv cohomology group sigma unit is_conn diff --git a/homology/basic.hlean b/homology/basic.hlean index c6ee35d..8d39387 100644 --- a/homology/basic.hlean +++ b/homology/basic.hlean @@ -6,7 +6,7 @@ Authors: Yuri Sulyma, Favonia, Floris van Doorn Reduced homology theories -/ -import ..homotopy.smash_spectrum ..homotopy.wedge +import ..spectrum.smash ..homotopy.wedge open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc function fwedge cofiber lift is_equiv choice algebra pi smash wedge diff --git a/homotopy/pointed_cubes.hlean b/pointed_cubes.hlean similarity index 99% rename from homotopy/pointed_cubes.hlean rename to pointed_cubes.hlean index 5266db8..592f8ea 100644 --- a/homotopy/pointed_cubes.hlean +++ b/pointed_cubes.hlean @@ -10,7 +10,7 @@ The goal of this file is to extend the library of pointed types and pointed maps -/ -import types.pointed2 ..pointed_pi +import types.pointed2 .pointed_pi open eq pointed diff --git a/homotopy/spectrum.hlean b/spectrum/basic.hlean similarity index 99% rename from homotopy/spectrum.hlean rename to spectrum/basic.hlean index 6d24ce3..b7550dd 100644 --- a/homotopy/spectrum.hlean +++ b/spectrum/basic.hlean @@ -5,7 +5,8 @@ Authors: Michael Shulman, Floris van Doorn, Egbert Rijke, Stefano Piceghello, Yu -/ -import homotopy.LES_of_homotopy_groups ..algebra.splice ..algebra.seq_colim .EM .fwedge .pointed_cubes +import homotopy.LES_of_homotopy_groups ..algebra.splice ..algebra.seq_colim ..homotopy.EM ..homotopy.fwedge + ..pointed_cubes open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group succ_str EM EM.ops function unit lift is_trunc diff --git a/homotopy/smash_spectrum.hlean b/spectrum/smash.hlean similarity index 97% rename from homotopy/smash_spectrum.hlean rename to spectrum/smash.hlean index fce02bf..5b78779 100644 --- a/homotopy/smash_spectrum.hlean +++ b/spectrum/smash.hlean @@ -1,4 +1,4 @@ -import .spectrification .smash_adjoint +import .spectrification ..homotopy.smash_adjoint open pointed is_equiv equiv eq susp succ_str smash int namespace spectrum diff --git a/homotopy/spectrification.hlean b/spectrum/spectrification.hlean similarity index 99% rename from homotopy/spectrification.hlean rename to spectrum/spectrification.hlean index 508fce8..23d8abf 100644 --- a/homotopy/spectrification.hlean +++ b/spectrum/spectrification.hlean @@ -1,4 +1,4 @@ -import .spectrum ..colim +import .basic ..colim open eq pointed succ_str is_equiv equiv spectrum.smap seq_colim nat diff --git a/homotopy/strunc.hlean b/spectrum/trunc.hlean similarity index 99% rename from homotopy/strunc.hlean rename to spectrum/trunc.hlean index 3569b86..4925e24 100644 --- a/homotopy/strunc.hlean +++ b/spectrum/trunc.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Ulrik Buchholtz Truncatedness and truncation of spectra -/ -import .spectrum .EM +import .basic open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM namespace spectrum