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

fix error when compiling

Browse source
This commit is contained in:
Floris van Doorn 2017-06-06 13:26:18 -04:00
parent dcf0327e98
commit aef91cd344
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
homotopy/pushout.hlean
View file

@ -1,5 +1,5 @@
import algebra.exactness homotopy.cofiber homotopy.wedge
import ..algebra.exactness homotopy.cofiber homotopy.wedge
open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber

2
homotopy/spectrum.hlean
View file

@ -385,7 +385,7 @@ namespace spectrum
pseq_colim (spectrify_type_fun X n)
/-
Let Y = spectify X. Then
Let Y = spectify X ≡ colim_k Ω^k X (n + k). Then
Ω Y (n+1) ≡ Ω colim_k Ω^k X ((n + 1) + k)
... = colim_k Ω^{k+1} X ((n + 1) + k)
... = colim_k Ω^{k+1} X (n + (k + 1))