Merge branch 'master' of https://github.com/cmu-phil/Spectral

README.md

@@ -98,4 +98,4 @@ These projects are mostly done
 - We will try to make sure that this repository compiles with the newest version of Lean 2.
 - Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2).
 - Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot).
-- If you contribute, please use rebase instead off merge (e.g. `git pull -r`).
+- If you contribute, please use rebase instead of merge (e.g. `git pull -r`).

algebra/arrow_group.hlean

@@ -1,7 +1,11 @@
-/- various groups of maps. Most importantly we define a group structure on trunc 0 (A →* Ω B),
+/-
-   which is used in the definition of cohomology -/
+Copyright (c) 2016-2017 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Ulrik Buchholtz
 
---author: Floris van Doorn
+Various groups of maps. Most importantly we define a group structure
+on trunc 0 (A →* Ω B), which is used in the definition of cohomology.
+-/
 
 import algebra.group_theory ..pointed ..pointed_pi eq2 homotopy.susp
 open pi pointed algebra group eq equiv is_trunc trunc susp
@@ -242,5 +246,59 @@ namespace group
   definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup :=
   AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _
 
+  definition trunc_ppi_isomorphic_pmap (A B : Type*)
+    : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
+      ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
+  begin
+    apply trunc_isomorphism_of_equiv (ppi_equiv_pmap A (Ω B)),
+    intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
+  end
+
+  section
+
+  universe variables u v
+
+  variables {A : pType.{u}} {B : A → Type.{v}} {x₀ : B pt} {k l m : ppi_gen B x₀}
+
+  definition ppi_homotopy_of_eq_homomorphism (p : k = l) (q : l = m)
+    : ppi_homotopy_of_eq (p ⬝ q) = ppi_homotopy_of_eq p ⬝*' ppi_homotopy_of_eq q :=
+  begin
+    induction q, induction p, induction k with k q, induction q, reflexivity
+  end
+
+  protected definition ppi_mul_loop.lemma1 {X : Type} {x : X} (p q : x = x) (p_pt : idp = p) (q_pt : idp = q)
+    : refl (p ⬝ q) ⬝ whisker_left p q_pt⁻¹ ⬝ p_pt⁻¹ = p_pt⁻¹ ◾ q_pt⁻¹ :=
+  by induction p_pt; induction q_pt; reflexivity
+
+  protected definition ppi_mul_loop.lemma2 {X : Type} {x : X} (p q : x = x) (p_pt : p = idp) (q_pt : q = idp)
+    : refl (p ⬝ q) ⬝ whisker_left p q_pt ⬝ p_pt = p_pt ◾ q_pt :=
+  by rewrite [-(inv_inv p_pt),-(inv_inv q_pt)]; exact ppi_mul_loop.lemma1 p q p_pt⁻¹ q_pt⁻¹
+
+  definition ppi_mul_loop {h : Πa, B a} (f g : ppi_gen.mk h idp ~~* ppi_gen.mk h idp) : f ⬝*' g = ppi_mul f g :=
+  begin
+    apply ap (ppi_gen.mk (λa, f a ⬝ g a)),
+    apply ppi_gen.rec_on f, intros f' f_pt, apply ppi_gen.rec_on g, intros g' g_pt,
+    clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt
+  end
+
+  variable (k)
+
+  definition trunc_ppi_loop_isomorphism_lemma
+    : isomorphism.{(max u v) (max u v)}
+      (Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop))
+      (Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) :=
+  begin
+    apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k),
+    intro f g, induction k with k p, induction p,
+    apply trans (ppi_homotopy_of_eq_homomorphism f g),
+    exact ppi_mul_loop (ppi_homotopy_of_eq f) (ppi_homotopy_of_eq g)
+  end
+
+  end
+
+  definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*)
+    : Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group
+      ≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group :=
+  trunc_ppi_loop_isomorphism_lemma (ppi_const B)
 
 end group

homotopy/cohomology.hlean

@@ -1,7 +1,7 @@
 /-
 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
+Authors: Floris van Doorn, Ulrik Buchholtz
 
 Reduced cohomology of spectra and cohomology theories
 -/
@@ -80,7 +80,13 @@ sorry /- TODO FOR SSS -/
 
 definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
-sorry /- TODO FOR SSS -/
+begin
+  apply isomorphism.trans (trunc_ppi_loop_isomorphism (λx, Ω (Y x (n + 2))))⁻¹ᵍ,
+  apply homotopy_group_isomorphism_of_pequiv 0, esimp,
+  have q : sub 2 m = n + 2,
+  from (int.add_comm (of_nat 2) (-m) ⬝ ap (λk, k + of_nat 2) p),
+  rewrite q, symmetry, apply ppi_loop_pequiv
+end
 
 definition unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi {X : Type}
   (Y : X → spectrum) {n m : ℤ} (p : -m = n) : upH^n[(x : X), Y x] ≃g πₛ[m] (supi X Y) :=

homotopy/strunc.hlean

@@ -1,19 +1,44 @@
+/-
+Copyright (c) 2017 Floris van Doorn and Ulrik Buchholtz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Ulrik Buchholtz
+
+Truncatedness and truncation of spectra
+-/
+
 import .spectrum .EM
 
 namespace int
 
   -- TODO move this
-  open trunc_index nat algebra
+  open nat algebra
   section
   private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
   le.intro (
-    calc n + 1 + -[1+ k] + k = n + 1 - (k + 1) + k : by reflexivity
+    calc n + 1 + -[1+ k] + k
-                         ... = n                   : sorry) /- TODO FOR SSS -/
+      = n + 1 + (-(k + 1)) + k : by reflexivity
+  ... = n + 1 + (-1 - k) + k    : by krewrite (neg_add_rev k 1)
+  ... = n + 1 + (-1 - k + k)    : add.assoc
+  ... = n + 1 + (-1 + -k + k)   : by reflexivity
+  ... = n + 1 + (-1 + (-k + k)) : add.assoc
+  ... = n + 1 + (-1 + 0)        : add.left_inv
+  ... = n + (1 + (-1 + 0))      : add.assoc
+  ... = n                       : int.add_zero)
 
   private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k :=
   le.intro (
-    calc -[1+ n] + 1 + k + n = - (n + 1) + 1 + k + n : by reflexivity
+    calc -[1+ n] + 1 + k + n
-                         ... = k                     : sorry) /- TODO FOR SSS -/
+      = - (n + 1) + 1 + k + n : by reflexivity
+  ... = -n - 1 + 1 + k + n    : by rewrite (neg_add n 1)
+  ... = -n + (-1 + 1) + k + n : by krewrite (int.add_assoc (-n) (-1) 1)
+  ... = -n + 0 + k + n        : add.left_inv 1
+  ... = -n + k + n            : int.add_zero
+  ... = k + -n + n            : int.add_comm
+  ... = k + (-n + n)          : int.add_assoc
+  ... = k + 0                 : add.left_inv n
+  ... = k                     : int.add_zero)
+
+  open trunc_index
 
   definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) :=
   begin

move_to_lib.hlean

@@ -439,6 +439,13 @@ namespace group
   definition isomorphism_of_is_contr {G H : Group} (hG : is_contr G) (hH : is_contr H) : G ≃g H :=
   trivial_group_of_is_contr G ⬝g (trivial_group_of_is_contr H)⁻¹ᵍ
 
+  definition trunc_isomorphism_of_equiv {A B : Type} [inf_group A] [inf_group B] (f : A ≃ B)
+    (h : is_mul_hom f) : Group.mk (trunc 0 A) (trunc_group A) ≃g Group.mk (trunc 0 B) (trunc_group B) :=
+  begin
+    apply isomorphism_of_equiv (equiv.mk (trunc_functor 0 f) (is_equiv_trunc_functor 0 f)), intros x x',
+    induction x with a, induction x' with a', apply ap tr, exact h a a'
+  end
+
 end group open group
 
 namespace fiber

pointed_pi.hlean

@@ -190,27 +190,13 @@ namespace pointed
     induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
   end
 
-  definition ppi_loop_equiv_lemma (p : k ~ k)
-    : (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k) ≃ (p pt = idp) :=
-    calc (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k)
-      ≃ (p pt ⬝ ppi_gen.resp_pt k = idp ⬝ ppi_gen.resp_pt k)
-        : equiv_eq_closed_right (p pt ⬝ ppi_gen.resp_pt k) (inverse (idp_con (ppi_gen.resp_pt k)))
-  ... ≃ (p pt = idp)
-        : eq_equiv_con_eq_con_right
-
   variables (k l)
+
   definition ppi_loop_equiv : (k = k) ≃ Π*(a : A), Ω (pType.mk (B a) (k a)) :=
-    calc (k = k) ≃ (k ~~* k)
+  begin
-                   : ppi_eq_equiv
+    induction k with k p, induction p,
-             ... ≃ Σ(p : k ~ k), p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k
+    exact ppi_eq_equiv (ppi_gen.mk k idp) (ppi_gen.mk k idp)
-                   : ppi_homotopy.sigma_char k k
+  end
-             ... ≃ Σ(p : k ~ k), p pt = idp
-                   : sigma_equiv_sigma_right
-                       (λ p, ppi_loop_equiv_lemma p)
-             ... ≃ Π*(a : A), pType.mk (k a = k a) idp
-                   : ppi.sigma_char
-             ... ≃ Π*(a : A), Ω (pType.mk (B a) (k a))
-                   : erfl
 
   variables {k l}
   -- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l :=