update README to reflect recent discussion

README.md

@@ -29,15 +29,32 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 
 ### Topology To Do:
 - HoTT Book sections 8.7, 8.8.
+- 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:
 - Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md))

homotopy/spherical_fibrations.hlean

@@ -14,6 +14,28 @@ namespace spherical_fibrations
 
   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,
@@ -96,15 +118,41 @@ namespace spherical_fibrations
   - 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
+  - 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), BSTop(n)
+  - 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,
+      fapply sigma_eq,
+      { apply ua, fapply equiv.MK,
+        { },
+        { },
+        { },
+        { }  },
+      { }
+    end
+
+  end two_sphere
+
 end spherical_fibrations