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

README.md

@@ -1,8 +1,8 @@
 # Spectral Sequences
 
-Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. 
+Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
 
-#### Participants 
+#### Participants
 Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
 
 ## Resources
@@ -20,7 +20,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - some basic theory: product, tensor, hom, projective,
 - categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category),
 - exact sequences, short and long
-- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) 
+- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma)
 - [5-lemma](http://ncatlab.org/nlab/show/five+lemma)
 - [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology)
 - [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples
@@ -28,18 +28,36 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences)
 
 ### Topology To Do:
-- HoTT Book chapter 8
+- HoTT Book sections 8.7, 8.8.
-- fiber and cofiber sequences (is this in the library already?)
+- fiber sequence
+  + already have the LES
+  + need shift isomorphism
+  + Hom'ing into a fiber sequence gives another fiber sequence.
+- cofiber sequences
+  + Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber
+    sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence.
 - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension
+  + try indexing on arbitrary successor structure
+  + think about equivariant spectra indexed by representations of `G`
 - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification)
+  + adjoint to forgetful
+  + as sequential colimit, prove induction principle (if useful)
+  + connective spectrum: `is_conn n.-2 Eₙ`
 - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra
 - fiber and cofiber sequences of spectra, stability
+  + limits are levelwise
+  + colimits need to be spectrified
 - long exact sequences from (co)fiber sequences of spectra
+  + indexed on ℤ, need to splice together LES's
 - [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and spectra
 - Postnikov towers of spectra
+  + basic definition already there
+  + fibers of Postnikov sequence unstably and stably
 - exact couple of a tower of spectra
+  + need to splice together LES's
 
 ### Already Done:
-- pointed types
+- Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))
-- definition of algebraic structures such as groups, rings, fields, 
+- pointed types, maps, homotopies and equivalences
-- some algebra: quotient, product, free.
+- definition of algebraic structures such as groups, rings, fields
+- some algebra: quotient, product, free groups.

algebra/graded.hlean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2016 Egbert Rijke. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egbert Rijke
+
+Graded modules and rings.
+-/

algebra/module.hlean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad
+
+Modules prod vector spaces over a ring.
+
+(We use "left_module," which is more precise, because "module" is a keyword.)
+-/
+import algebra.field
+open algebra
+
+structure has_scalar [class] (F V : Type) :=
+(smul : F → V → V)
+
+infixl ` • `:73 := has_scalar.smul
+
+/- modules over a ring -/
+
+structure left_module [class] (R M : Type) [ringR : ring R]
+  extends has_scalar R M, add_comm_group M :=
+(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
+(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x)))
+(mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
+(one_smul : Π x, smul one x = x)
+
+section left_module
+  variables {R M : Type}
+  variable  [ringR : ring R]
+  variable  [moduleRM : left_module R M]
+  include   ringR moduleRM
+
+  -- Note: the anonymous include does not work in the propositions below.
+
+  proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
+  !left_module.smul_left_distrib
+
+  proposition smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
+  !left_module.smul_right_distrib
+
+  proposition mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
+  !left_module.mul_smul
+
+  proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul
+
+  proposition zero_smul (u : M) : (0 : R) • u = 0 :=
+  have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_right_distrib, *add_zero],
+  !add.left_cancel this
+
+  proposition smul_zero (a : R) : a • (0 : M) = 0 :=
+  have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
+  !add.left_cancel this
+
+  proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) :=
+  eq_neg_of_add_eq_zero (by rewrite [-smul_right_distrib, add.left_inv, zero_smul])
+
+  proposition neg_one_smul (u : M) : -(1 : R) • u = -u :=
+  by rewrite [neg_smul, one_smul]
+
+  proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) :=
+  by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul]
+
+  proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v :=
+  by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg]
+
+  proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
+  by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
+end left_module
+
+/- vector spaces -/
+
+structure vector_space [class] (F V : Type) [fieldF : field F]
+  extends left_module F V

homotopy/LES_applications.hlean

@@ -1,6 +1,7 @@
-import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group
+import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join
-open eq is_trunc pointed homotopy is_equiv fiber equiv trunc nat chain_complex prod fin algebra
+open eq is_trunc pointed is_conn is_equiv fiber equiv trunc nat chain_complex prod fin algebra
-     group trunc_index function
+     group trunc_index function join pushout
+
 namespace nat
   open sigma sum
   definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) :=
@@ -25,63 +26,16 @@ open nat
 
 namespace is_conn
 
-  theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (k n : ℕ) (f : A →* B)
-    [H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
-  @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
-
-  -- TODO: use this for trivial_homotopy_group_of_is_conn (in homotopy.homotopy_group)
-  theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
-  begin
-    apply is_contr_equiv_closed,
-    apply trunc_trunc_equiv_left _ n k H
-  end
-
-  definition zero_le_of_nat (n : ℕ) : 0 ≤[ℕ₋₂] n :=
-  of_nat_le_of_nat (zero_le n)
-
-  local attribute is_conn_map [reducible] --TODO
-  theorem is_conn_map_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k)
-    [is_conn_map k f] : is_conn_map n f :=
-  λb, is_conn_of_le _ H
-
-  definition is_surjective_trunc_functor {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_surjective f]
-    : is_surjective (trunc_functor n f) :=
-  begin
-    cases n with n: intro b,
-    { exact tr (fiber.mk !center !is_prop.elim)},
-    { refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ},
-      clear b, intro b, induction H b with v, induction v with a p,
-      exact tr (fiber.mk (tr a) (ap tr p))}
-  end
-
-  definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B)
-    [H : is_surjective (g ∘ f)] : is_surjective g :=
-  begin
-    intro c,
-    induction H c with v, induction v with a p,
-    exact tr (fiber.mk (f a) p)
-  end
-
-  -- Lemma 7.5.14
-  theorem is_equiv_trunc_functor_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B)
-    [H : is_conn_map n f] : is_equiv (trunc_functor n f) :=
-  begin
-    exact sorry
-  end
-
-  definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) :=
-  by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse
-
   local attribute comm_group.to_group [coercion]
   local attribute is_equiv_tinverse [instance]
 
   theorem is_equiv_π_of_is_connected.{u} {A B : pType.{u}} (n k : ℕ) (f : A →* B)
-    [H : is_conn_map n f] (H2 : k ≤ n) : is_equiv (π→[k] f) :=
+    [H : is_conn_fun n f] (H2 : k ≤ n) : is_equiv (π→[k] f) :=
   begin
     induction k using rec_on_even_odd with k: cases k with k,
     { /- k = 0 -/
-      change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_map,
+      change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun,
-      refine is_conn_map_of_le f (zero_le_of_nat n)},
+      refine is_conn_fun_of_le f (zero_le_of_nat n)},
     { /- k > 0 even -/
       have H2' : 2 * k + 1 ≤ n, from le.trans !self_le_succ H2,
       exact
@@ -113,21 +67,53 @@ namespace is_conn
   end
 
   theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B)
-    [H : is_conn_map n f] : is_surjective (π→[n + 1] f) :=
+    [H : is_conn_fun n f] : is_surjective (π→[n + 1] f) :=
   begin
     induction n using rec_on_even_odd with n,
-    { cases n with n,
+    { have H3 : is_surjective (π→*[2*n + 1] f ∘* tinverse), from
-      { exact sorry},
+      @is_surjective_of_trivial _
-      { have H3 : is_surjective (π→*[2*(succ n) + 1] f ∘* tinverse), from
+        (LES_of_homotopy_groups3 f) _
-        @is_surjective_of_trivial _
+        (is_exact_LES_of_homotopy_groups3 f (n, 2))
-          (LES_of_homotopy_groups3 f) _
+        (@is_contr_HG_fiber_of_is_connected A B (2 * n) (2 * n) f H !le.refl),
-          (is_exact_LES_of_homotopy_groups3 f (succ n, 2))
+      exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*n + 1] f)) tinverse) H3},
-          (@is_contr_HG_fiber_of_is_connected A B (2 * succ n) (2 * succ n) f H !le.refl),
-        exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*(succ n) + 1] f)) tinverse) H3}},
     { exact @is_surjective_of_trivial _
         (LES_of_homotopy_groups3 f) _
         (is_exact_LES_of_homotopy_groups3 f (k, 5))
         (@is_contr_HG_fiber_of_is_connected A B (2 * k + 1) (2 * k + 1) f H !le.refl)}
   end
 
+  /- joins -/
+
+  definition join_empty_right [constructor] (A : Type) : join A empty ≃ A :=
+  begin
+    fapply equiv.MK,
+    { intro x, induction x with a o a o,
+      { exact a },
+      { exact empty.elim o },
+      { exact empty.elim o } },
+    { exact pushout.inl },
+    { intro a, reflexivity},
+    { intro x, induction x with a o a o,
+      { reflexivity },
+      { exact empty.elim o },
+      { exact empty.elim o } }
+  end
+
+  definition natural_square2 {A B X : Type} {f : A → X} {g : B → X} (h : Πa b, f a = g b)
+    {a a' : A} {b b' : B} (p : a = a') (q : b = b')
+    : square (ap f p) (ap g q) (h a b) (h a' b') :=
+  by induction p; induction q; exact hrfl
+
+  section
+    open sphere sphere_index
+
+    definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp
+    definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp
+    definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n :=
+    begin induction n with n IH, reflexivity, exact ap succ IH end
+    definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 :=
+    begin induction m with m IH, reflexivity, exact ap succ IH end
+
+  end
+
 end is_conn

homotopy/LES_of_homotopy_groups.hlean

@@ -208,9 +208,10 @@ namespace chain_complex
   theorem fiber_sequence_fun_eq : Π(x : fiber_sequence_carrier f (n + 4)),
     fiber_sequence_carrier_pequiv f n (fiber_sequence_fun f (n + 3) x) =
       ap1 (fiber_sequence_fun f n) (fiber_sequence_carrier_pequiv f (n + 1) x)⁻¹ :=
-  homotopy_of_inv_homotopy
+  begin
-    (pequiv.to_equiv (fiber_sequence_carrier_pequiv f (n + 1)))
+    apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv f (n + 1)),
-    (fiber_sequence_fun_eq_helper f n)
+    apply fiber_sequence_fun_eq_helper f n
+  end
 
   theorem fiber_sequence_fun_phomotopy :
     fiber_sequence_carrier_pequiv f n ∘*

homotopy/chain_complex.hlean

@@ -209,8 +209,8 @@ namespace chain_complex
     have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt,
     begin
       refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y,
-      refine inv_homotopy_of_homotopy (pequiv.to_equiv e) _,
+      apply inv_homotopy_of_homotopy_pre e,
-      apply inv_homotopy_of_homotopy, apply p
+      apply inv_homotopy_of_homotopy_pre, apply p
     end,
     induction (H _ H2) with x r,
     refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _,
@@ -495,7 +495,6 @@ namespace chain_complex
             pt_mul := one_mul,
             mul_pt := mul_one,
             mul_left_inv_pt := mul.left_inv⦄
-
   end
 
   -- the following theorems would also be true of the replace "is_contr" by "is_prop"

homotopy/join_theorem.hlean

@@ -0,0 +1,83 @@
+/-- Authors: Clive, Egbert --/
+
+import homotopy.connectedness homotopy.join
+
+open eq sigma pi function join is_conn is_trunc equiv is_equiv
+
+namespace retraction
+  variables {A B C : Type} (r2 : B → C) (r1 : A → B)
+
+
+  definition is_retraction_compose
+    [Hr2 : is_retraction r2] [Hr1 : is_retraction r1] :
+    is_retraction (r2 ∘ r1) :=
+  begin
+    cases Hr2 with s2 s2_is_right_inverse,
+    cases Hr1 with s1 s1_is_right_inverse,
+    fapply is_retraction.mk,
+    { exact s1 ∘ s2},
+    { intro b, esimp,
+      calc
+      r2 (r1 (s1 (s2 (b)))) = r2 (s2 (b)) : ap r2 (s1_is_right_inverse (s2 b))
+                        ... = b           : s2_is_right_inverse b
+
+    }, /-- QED --/
+  end
+
+  definition is_retraction_compose_equiv_left [Hr2 : is_equiv r2] [Hr1 : is_retraction r1] : is_retraction (r2 ∘ r1) :=
+  begin
+    apply is_retraction_compose,
+  end
+
+  definition is_retraction_compose_equiv_right [Hr2 : is_retraction r2] [Hr1 :  is_equiv r1] : is_retraction (r2 ∘ r1) :=
+  begin
+    apply is_retraction_compose,
+  end
+
+end retraction
+
+namespace is_conn
+section
+
+    open retraction
+
+    universe variable u
+    parameters (n : ℕ₋₂) {A : Type.{u}}
+    parameter sec : ΠV : trunctype.{u} n,
+                    is_retraction (const A : V → (A → V))
+
+    include sec
+
+    protected definition intro : is_conn n A :=
+    begin
+      apply is_conn_of_map_to_unit,
+      apply is_conn_fun.intro,
+      intro P,
+      refine is_retraction_compose_equiv_right (const A) (pi_unit_left P),
+    end
+end
+end is_conn
+
+section Join_Theorem
+
+variables (X Y : Type)
+          (m n : ℕ₋₂)
+          [HXm : is_conn m X]
+          [HYn : is_conn n Y]
+
+include HXm HYn
+
+theorem is_conn_join : is_conn (m +2+ n) (join X Y) :=
+begin
+  apply is_conn.intro,
+  intro V,
+  apply is_retraction_of_is_equiv,
+  apply is_equiv_of_is_contr_fun,
+  intro f,
+  refine is_contr_equiv_closed _,
+  {exact unit},
+  symmetry,
+  exact sorry
+end
+
+end Join_Theorem

homotopy/sample.hlean

@@ -21,13 +21,13 @@ namespace homotopy
     assumption
   end
 
-  definition is_conn_map (n : trunc_index) {A B : Type} (f : A → B) : Type :=
+  definition is_conn_fun (n : trunc_index) {A B : Type} (f : A → B) : Type :=
   Πb : B, is_conn n (fiber f b)
 
-  namespace is_conn_map
+  namespace is_conn_fun
   section
     parameters {n : trunc_index} {A B : Type} {h : A → B}
-               (H : is_conn_map n h) (P : B → n -Type)
+               (H : is_conn_fun n h) (P : B → n -Type)
 
     private definition helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b :=
     λt b, trunc.rec (λx, point_eq x ▸ t (point x))
@@ -67,7 +67,7 @@ namespace homotopy
     include sec
 
     -- the other half of Lemma 7.5.7
-    definition intro : is_conn_map n h :=
+    definition intro : is_conn_fun n h :=
     begin
       intro b,
       apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b),
@@ -79,22 +79,22 @@ namespace homotopy
       exact apd10 (@right_inverse _ _ _ s (λa, tr (fiber.mk a idp))) a
     end
   end
-  end is_conn_map
+  end is_conn_fun
 
   -- Connectedness is related to maps to and from the unit type, first to
   section
     parameters (n : trunc_index) (A : Type)
 
     definition is_conn_of_map_to_unit
-      : is_conn_map n (λx : A, unit.star) → is_conn n A :=
+      : is_conn_fun n (λx : A, unit.star) → is_conn n A :=
     begin
-      intro H, unfold is_conn_map at H,
+      intro H, unfold is_conn_fun at H,
       rewrite [-(ua (fiber.fiber_star_equiv A))],
       exact (H unit.star)
     end
 
     -- now maps from unit
-    definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_map n (const unit a₀))
+    definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_fun n (const unit a₀))
       : is_conn n .+1 A :=
     is_contr.mk (tr a₀)
     begin
@@ -103,8 +103,8 @@ namespace homotopy
                             (@center _ (H a))
     end
 
-    definition is_conn_map_from_unit (a₀ : A) [H : is_conn n .+1 A]
+    definition is_conn_fun_from_unit (a₀ : A) [H : is_conn n .+1 A]
-      : is_conn_map n (const unit a₀) :=
+      : is_conn_fun n (const unit a₀) :=
     begin
       intro a,
       apply is_conn_equiv_closed n (equiv.symm (fiber_const_equiv A a₀ a)),
@@ -115,14 +115,14 @@ namespace homotopy
 
   -- Lemma 7.5.2
   definition minus_one_conn_of_surjective {A B : Type} (f : A → B)
-    : is_surjective f → is_conn_map -1 f :=
+    : is_surjective f → is_conn_fun -1 f :=
   begin
     intro H, intro b,
     exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
   end
 
   definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B)
-    : is_conn_map -1 f → is_surjective f :=
+    : is_conn_fun -1 f → is_surjective f :=
   begin
     intro H, intro b,
     exact @center (∥fiber f b∥) (H b),
@@ -141,7 +141,7 @@ namespace homotopy
 
     -- Lemma 7.5.4
     definition retract_of_conn_is_conn [instance] (r : arrow_hom f g) [H : is_retraction r]
-      (n : trunc_index) [K : is_conn_map n f] : is_conn_map n g :=
+      (n : trunc_index) [K : is_conn_fun n f] : is_conn_fun n g :=
     begin
       intro b, unfold is_conn,
       apply is_contr_retract (trunc_functor n (retraction_on_fiber r b)),
@@ -152,7 +152,7 @@ namespace homotopy
 
   -- Corollary 7.5.5
   definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
-    (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g :=
+    (p : f ~ g) (H : is_conn_fun n f) : is_conn_fun n g :=
   @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
 
   -- all types are -2-connected
@@ -181,8 +181,8 @@ namespace homotopy
       { intros H,
         change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'),
         generalize a',
-        apply is_conn_map.elim
+        apply is_conn_fun.elim
-              (is_conn_map_from_unit n A a)
+              (is_conn_fun_from_unit n A a)
               (λx : A, trunctype.mk' n (ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid x))),
         intros,
         change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a),

homotopy/sec83.hlean

@@ -1,44 +0,0 @@
--- Section 8.3
-
-import types.trunc types.pointed homotopy.connectedness homotopy.sphere homotopy.circle algebra.group algebra.homotopy_group
-
-open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed trunc_index homotopy
-
-
--- Lemma 8.3.1
-
-theorem trivial_homotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k)
-  : is_contr (πg[k+1] A) :=
-begin
-  apply is_trunc_trunc_of_is_trunc,
-  apply is_contr_loop_of_is_trunc,
-  apply @is_trunc_of_le A n _,
-  exact of_nat_le_of_nat H
-end
-
--- Lemma 8.3.2
-theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
-  : is_contr (π[k] A) :=
-begin
-    have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H,
-    have H3 : is_contr (ptrunc k A),
-    begin
-      fapply is_contr_equiv_closed,
-      { apply trunc_trunc_equiv_left _ k n H2}
-    end,
-    have H4 : is_contr (Ω[k](ptrunc k A)),
-      from !is_trunc_loop_of_is_trunc,
-    apply is_trunc_equiv_closed_rev,
-    { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
-end
-
--- Corollary 8.3.3
-open sphere.ops sphere_index
-theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
-begin
-  cases n with n,
-  { exfalso, apply not_lt_zero, exact H},
-  { have H2 : k ≤ n, from le_of_lt_succ H,
-    apply @(trivial_homotopy_group_of_is_conn _ H2),
-    rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere}
-end

homotopy/sec86.hlean

@@ -1,45 +1,276 @@
+-- TODO: in wedge connectivity and is_conn.elim, unbundle P
 
+import  homotopy.wedge types.pi .LES_applications --TODO: remove
 
-import  homotopy.wedge types.pi
+open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index
 
-open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc
+  -- definition iterated_loop_ptrunc_pequiv_con' (n : ℕ₋₂) (k : ℕ) (A : Type*)
+  --   (p q : Ω[k](ptrunc (n+k) (Ω A))) :
+  --   iterated_loop_ptrunc_pequiv n k (Ω A) (loop_mul trunc_concat p q) =
+  --   trunc_functor2 (loop_mul concat) (iterated_loop_ptrunc_pequiv n k (Ω A) p)
+  --                                    (iterated_loop_ptrunc_pequiv n k (Ω A) q) :=
+  -- begin
+  --   revert n p q, induction k with k IH: intro n p q,
+  --   { reflexivity},
+  --   { exact sorry}
+  -- end
 
-section freudenthal
+  -- example : ((@add.{0} trunc_index has_add_trunc_index n
+  --               (trunc_index.of_nat
+  --                  (@add.{0} nat nat._trans_of_decidable_linear_ordered_semiring_17 nat.zero
+  --                     (@one.{0} nat nat._trans_of_decidable_linear_ordered_semiring_21))))) = (0 : ℕ₋₂) := proof idp qed
 
-parameters {A : Type*} (n : ℕ) [is_conn n A]
+  definition iterated_loop_ptrunc_pequiv_con (n : ℕ₋₂) (k : ℕ) (A : Type*)
-
+    (p q : Ω[k + 1](ptrunc (n+k+1) A)) :
---set_option pp.notation false
+    iterated_loop_ptrunc_pequiv n (k+1) A (p ⬝ q) =
-
+    trunc_concat (iterated_loop_ptrunc_pequiv n (k+1) A p)
-protected definition my_wedge_extension.ext : Π {A : Type*} {B : Type*} (n m : ℕ) [cA : is_conn n (carrier A)] [cB : is_conn m (carrier B)]
+                 (iterated_loop_ptrunc_pequiv n (k+1) A q) :=
-(P : carrier A → carrier B → (m+n)-Type) (f : Π (a : carrier A), trunctype.carrier (P a (Point B)))
-(g : Π (b : carrier B), trunctype.carrier (P (Point A) b)),
-  f (Point A) = g (Point B) → (Π (a : carrier A) (b : carrier B), trunctype.carrier (P a b)) :=
-sorry
-
-definition code_fun (a : A) (q : north = north :> susp A)
-  : trunc (n * 2) (fiber (pmap.to_fun (loop_susp_unit A)) q) → trunc (n * 2) (fiber merid (q ⬝ merid a)) :=
-begin
-  intro x, induction x with x,
-  esimp at *, cases x with a' p,
---  apply my_wedge_extension.ext n n,
-  exact sorry
-end
-
-definition code (y : susp A) :  north = y → Type :=
-susp.rec_on y
-  (λp, trunc (2*n) (fiber (loop_susp_unit A) p))
-  (λq, trunc (2*n) (fiber merid q))
   begin
-    intros,
-    apply arrow_pathover_constant_right,
-    intro q, rewrite [transport_eq_r],
-    apply ua,
     exact sorry
+    -- induction k with k IH,
+    -- { replace (nat.zero + 1) with (nat.succ nat.zero), esimp [iterated_loop_ptrunc_pequiv],
+    --   exact sorry},
+    -- { exact sorry}
   end
 
-definition freudenthal_suspension  : is_conn_map (n*2) (loop_susp_unit A) :=
+  theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
-sorry
+    (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) :=
+  by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,ap_inv,elim_merid]; apply cast_ua_inv_fn
 
+  definition is_conn_trunc (A : Type) (n k : ℕ₋₂) [H : is_conn n A]
+    : is_conn n (trunc k A) :=
+  begin
+    apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
+  end
 
+  section open sphere sphere.ops
+  definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
+  end
 
-end freudenthal
+namespace freudenthal section
+
+  parameters {A : Type*} {n : ℕ} [is_conn n A]
+
+  --porting from Agda
+  -- definition Q (x : susp A) : Type :=
+  -- trunc (k) (north = x)
+
+  definition up (a : A) : north = north :> susp A := -- up a = loop_susp_unit A a
+  merid a ⬝ (merid pt)⁻¹
+
+  definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A :=
+  begin
+    have is_conn n (ptrunc (n + n) A), from !is_conn_trunc,
+    refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _,
+    { exact tr},
+    { exact id},
+    { reflexivity}
+  end
+
+  definition code_merid_β_left (a : A) : code_merid a pt = tr a :=
+  by apply wedge_extension.β_left
+
+  definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b :=
+  by apply wedge_extension.β_right
+
+  definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt :=
+  begin
+    symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh
+  end
+
+  definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) :=
+  begin
+    have Πa, is_trunc n.-2.+1 (is_equiv (code_merid a)),
+      from λa, is_trunc_of_le _ !minus_one_le_succ,
+    refine is_conn.elim (n.-1) _ _ a,
+    { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))}
+  end
+
+  definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A :=
+  equiv.mk _ (is_equiv_code_merid a)
+
+  definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x :=
+  begin
+    refine ap010 @(is_equiv.inv _) _ x ⬝ _,
+    { exact homotopy_closed id (homotopy.symm code_merid_β_right)},
+    { apply is_conn.elim_β},
+    { reflexivity}
+  end
+
+  definition code [unfold 4] : susp A → Type :=
+  susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv
+
+  definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) :=
+  begin
+    induction x with a: esimp,
+    { exact _},
+    { exact _},
+    { apply is_prop.elimo}
+  end
+  local attribute is_trunc_code [instance]
+
+  definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) :=
+  trunc_functor (n + n) up
+
+  definition decode_north_pt : decode_north (tr pt) = tr idp :=
+  ap tr !con.right_inv
+
+  definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) :=
+  trunc_functor (n + n) merid
+
+  definition encode' {x : susp A} (p : north = x) : code x :=
+  transport code p (tr pt)
+
+  definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x :=
+  begin
+    induction p with p,
+    exact transport code p (tr pt)
+  end
+
+  theorem encode_decode_north (c : code north) : encode (decode_north c) = c :=
+  begin
+    have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _,
+    esimp at *,
+    induction c with a,
+    rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*,
+             code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt]
+  end
+
+  definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover_constant_left_id_right,
+    apply square_of_eq,
+    exact whisker_right !con.right_inv (merid a)
+  end
+
+  definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover_constant_left_id_right,
+    apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹
+  end
+
+  definition decode_coh_lem {A : Type} {a a' : A} (p : a = a')
+    : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ :=
+  by induction p; reflexivity
+
+  theorem decode_coh (a : A) : decode_north =[merid a] decode_south :=
+  begin
+    apply arrow_pathover_left, intro c, esimp at *,
+    induction c with a',
+    rewrite [↑code, elim_type_merid, ▸*],
+    refine wedge_extension.ext n n _ _ _ _ a a',
+    { exact decode_coh_f},
+    { exact decode_coh_g},
+    { clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _,
+      { refine ap (λp, trunc_pathover (eq_pathover_constant_left_id_right (square_of_eq p))) _,
+        apply decode_coh_lem},
+      { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}}
+  end
+
+  definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) :=
+  begin
+    induction x with a,
+    { exact decode_north c},
+    { exact decode_south c},
+    { exact decode_coh a}
+  end
+
+  theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p :=
+  begin
+    induction p with p, induction p, esimp, apply decode_north_pt
+  end
+
+  parameters (A n)
+  definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) :=
+  equiv.MK decode_north encode decode_encode encode_decode_north
+
+  definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) :=
+  pequiv_of_equiv equiv' decode_north_pt
+
+  -- can we get this?
+  -- definition freudenthal_suspension  : is_conn_fun (n+n) (loop_susp_unit A) :=
+  -- begin
+  --   intro p, esimp at *, fapply is_contr.mk,
+  --   { note c := encode (tr p), esimp at *, induction c with a, },
+  --   { exact sorry}
+  -- end
+
+-- {- Used to prove stability in iterated suspensions -}
+-- module FreudenthalIso
+--   {i} (n : ℕ₋₂) (k : ℕ) (t : k ≠ O) (kle : ⟨ k ⟩ ≤T S (n +2+ S n))
+--   (X : Ptd i) (cX : is-connected (S (S n)) (fst X)) where
+
+--   open FreudenthalEquiv n (⟨ k ⟩) kle (fst X) (snd X) cX public
+
+--   hom : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level
+--      →ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level
+--   hom = record {
+--     f = fst F;
+--     pres-comp = ap^-conc^ k t (decodeN , decodeN-pt) }
+--     where F = ap^ k (decodeN , decodeN-pt)
+
+--   iso : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level
+--      ≃ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level
+--   iso = (hom , is-equiv-ap^ k (decodeN , decodeN-pt) (snd eq))
+
+end end freudenthal
+
+open algebra
+definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : ptrunc k A ≃* ptrunc k (Ω (psusp A)) :=
+have H' : k ≤[ℕ₋₂] n + n,
+  by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H,
+ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n)
+
+definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : trunc k A ≃ trunc k (Ω (psusp A)) :=
+freudenthal_pequiv A H
+
+namespace sphere
+  open ops algebra pointed function
+
+  definition stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) :=
+  begin
+    have H' : k ≤ 2 * pred n,
+    begin
+      rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)),
+      apply pred_le_pred, apply pred_le_pred, exact H
+    end,
+    have is_conn (of_nat (pred n)) (S. n),
+    begin
+      cases n with n,
+      { exfalso, exact not_succ_le_zero _ H},
+      { esimp, apply is_conn_psphere}
+    end,
+    refine pequiv_of_eq (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) k)) ⬝e* _,
+    rewrite psphere_succ,
+    refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _,
+    refine loopn_pequiv_loopn k (freudenthal_pequiv _ H')⁻¹ᵉ* ⬝e* _,
+    exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
+  end
+
+--print phomotopy_group_pequiv_loop_ptrunc
+--print iterated_loop_ptrunc_pequiv
+  -- definition to_fun_stability_pequiv (k n : ℕ) (H : k + 3 ≤ 2 * n) --(p : π*[k + 1] (S. (n+1)))
+  --   : stability_pequiv (k+1) n H = _ ∘ _ ∘ cast (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) (k+1))) :=
+  -- sorry
+
+  -- definition stability (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) :=
+  -- begin
+  --   fapply Group_eq,
+  --   { refine equiv_of_pequiv (stability_pequiv _ _ _), rewrite succ_add, exact H},
+  --   { intro g h, esimp, }
+  -- end
+
+end sphere
+
+/-
+  changes in book:
+  proof 8.6.15: also mention that we ignore multiplication
+  proof 8.4.4: respects points
+  proof 8.4.8: do k=0 separately
+-/

homotopy/spherical_fibrations.hlean

@@ -0,0 +1,152 @@
+import homotopy.join homotopy.smash
+
+open eq equiv trunc function bool join sphere sphere_index sphere.ops prod
+open pointed sigma smash
+
+namespace spherical_fibrations
+
+  /- classifying type of spherical fibrations -/
+  definition BG (n : ℕ) : Type₁ :=
+  Σ(X : Type₀), ∥ X ≃ S n..-1 ∥
+
+  definition pointed_BG [instance] [constructor] (n : ℕ) : pointed (BG n) :=
+  pointed.mk ⟨ S n..-1 , tr erfl ⟩
+
+  definition pBG [constructor] (n : ℕ) : Type* := pointed.mk' (BG n)
+
+  definition G (n : ℕ) : Type₁ :=
+  pt = pt :> BG n
+
+  definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) :=
+  sorry
+
+  definition mirror (n : ℕ) : S n..-1 → G n :=
+  begin
+    intro v, apply to_inv (G_char n),
+    exact sorry
+  end
+
+/-
+  Can we give a fibration P : S n → Type, P base = F n = Ω(BF n) = (S. n ≃* S. n)
+  and total space sigma P ≃ G (n+1) = Ω(BG (n+1)) = (S n.+1 ≃ S .n+1)
+
+  Yes, let eval : BG (n+1) → S n be the evaluation map
+-/
+
+  definition S_of_BG (n : ℕ) : Ω(pBG (n+1)) → S n :=
+  λ f, f..1 ▸ base
+
+  definition BG_succ (n : ℕ) : BG n → BG (n+1) :=
+  begin
+    intro X, cases X with X p,
+    apply sigma.mk (susp X), induction p with f, apply tr,
+    apply susp.equiv f
+  end
+
+  /- classifying type of pointed spherical fibrations -/
+  definition BF (n : ℕ) : Type₁ :=
+  Σ(X : Type*), ∥ X ≃* S. n ∥
+
+  definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) :=
+  pointed.mk ⟨ S. n , tr pequiv.rfl ⟩
+
+  definition pBF [constructor] (n : ℕ) : Type* := pointed.mk' (BF n)
+
+  definition BF_succ (n : ℕ) : BF n → BF (n+1) :=
+  begin
+    intro X, cases X with X p,
+    apply sigma.mk (psusp X), induction p with f, apply tr,
+    apply susp.psusp_equiv f
+  end
+
+  definition BF_of_BG {n : ℕ} : BG n → BF n :=
+  begin
+    intro X, cases X with X p,
+    apply sigma.mk (pointed.MK (susp X) susp.north),
+    induction p with f, apply tr,
+    apply pequiv_of_equiv (susp.equiv f),
+    reflexivity
+  end
+
+  definition BG_of_BF {n : ℕ} : BF n → BG (n + 1) :=
+  begin
+    intro X, cases X with X hX,
+    apply sigma.mk (carrier X), induction hX with fX,
+    apply tr, exact fX
+  end
+
+  definition BG_mul {n m : ℕ} (X : BG n) (Y : BG m) : BG (n + m) :=
+  begin
+    cases X with X pX, cases Y with Y pY,
+    apply sigma.mk (join X Y),
+    induction pX with fX, induction pY with fY,
+    apply tr, rewrite add_sub_one,
+    exact (join.equiv_closed fX fY) ⬝e (join.spheres n..-1 m..-1)
+  end
+
+  definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) :=
+  begin
+    cases X with X hX, cases Y with Y hY,
+    apply sigma.mk (psmash X Y),
+    induction hX with fX, induction hY with fY, apply tr,
+    exact sorry -- needs smash.spheres : psmash (S. n) (S. m) ≃ S. (n + m)
+  end
+
+  definition BF_of_BG_mul (n m : ℕ) (X : BG n) (Y : BG m)
+    : BF_of_BG (BG_mul X Y) = BF_mul (BF_of_BG X) (BF_of_BG Y) :=
+  sorry
+
+  -- Thom spaces
+  namespace thom
+    variables {X : Type} {n : ℕ} (α : X → BF n)
+
+    -- the canonical section of an F-object
+    protected definition sec (x : X) : carrier (sigma.pr1 (α x)) :=
+    Point _
+
+    open pushout sigma
+
+    definition thom_space : Type :=
+    pushout (λx : X, ⟨x , thom.sec α x⟩) (const X unit.star)
+  end thom
+
+/-
+  Things to do:
+  - Orientability and orientations
+    * Thom class u ∈ ~Hⁿ(Tξ)
+    * eventually prove Thom-Isomorphism (Rudyak IV.5.7)
+  - define BG∞ and BF∞ as colimits of BG n and BF n
+  - Ω(BF n) = ΩⁿSⁿ₁ + ΩⁿSⁿ₋₁ (self-maps of degree ±1)
+  - succ_BF n is (n - 2) connected (from Freudenthal)
+  - pfiber (BG_of_BF n) ≃* S. n
+  - π₁(BF n)=π₁(BG n)=ℤ/2ℤ
+  - double covers BSG and BSF
+  - O : BF n → BG 1 = Σ(A : Type), ∥ A = bool ∥
+  - BSG n = sigma O
+  - π₁(BSG n)=π₁(BSF n)=O
+  - BSO(n),
+  - find BF' n : Type₀ with BF' n ≃ BF n etc.
+  - canonical bundle γₙ : ℝP(n) → ℝP∞=BO(1) → Type₀
+     prove T(γₙ) = ℝP(n+1)
+  - BG∞ = BF∞ (in fact = BGL₁(S), the group of units of the sphere spectrum)
+  - clutching construction:
+     any f : S n → SG(n)  gives S n.+1 → BSG(n)  (mut.mut. for O(n),SO(n),etc.)
+  - all bundles on S 3 are trivial, incl. tangent bundle
+  - Adams' result on vector fields on spheres:
+     there are maximally ρ(n)-1 indep.sections of the tangent bundle of S (n-1)
+     where ρ(n) is the n'th Radon-Hurwitz number.→ 
+-/
+
+-- tangent bundle on S 2:
+
+  namespace two_sphere
+
+    definition tau : S 2 → BG 2 :=
+    begin
+      intro v, induction v with x, do 2 exact pt,
+      exact sorry
+    end
+
+  end two_sphere
+
+end spherical_fibrations