From e7c3144dbdad7a976942a742d307002413370f84 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 15 Sep 2016 18:05:58 -0400 Subject: [PATCH] fill in sorry in spherical_fibrations --- homotopy/spherical_fibrations.hlean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 2dab9b5..c6e274a 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -1,7 +1,7 @@ import homotopy.join homotopy.smash open eq equiv trunc function bool join sphere sphere_index sphere.ops prod -open pointed sigma smash +open pointed sigma smash is_trunc namespace spherical_fibrations @@ -18,7 +18,10 @@ namespace spherical_fibrations pt = pt :> BG n definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) := - sorry + calc + G n ≃ Σ(p : S n..-1 = S n..-1), _ : sigma_eq_equiv + ... ≃ (S n..-1 = S n..-1) : sigma_equiv_of_is_contr_right + ... ≃ (S n..-1 ≃ S n..-1) : eq_equiv_equiv definition mirror (n : ℕ) : S n..-1 → G n := begin @@ -134,7 +137,7 @@ namespace spherical_fibrations - 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.→ + where ρ(n) is the n'th Radon-Hurwitz number.→ -/ -- tangent bundle on S 2: