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

fill in sorry in spherical_fibrations

Browse source
This commit is contained in:
Floris van Doorn 2016-09-15 18:05:58 -04:00
parent 683a515178
commit e7c3144dbd
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
homotopy/spherical_fibrations.hlean
View file

@ -1,7 +1,7 @@
import homotopy.join homotopy.smash import homotopy.join homotopy.smash
open eq equiv trunc function bool join sphere sphere_index sphere.ops prod 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 namespace spherical_fibrations
@ -18,7 +18,10 @@ namespace spherical_fibrations
pt = pt :> BG n pt = pt :> BG n
definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) := 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 := definition mirror (n : ℕ) : S n..-1 → G n :=
begin begin
@ -134,7 +137,7 @@ namespace spherical_fibrations
- all bundles on S 3 are trivial, incl. tangent bundle - all bundles on S 3 are trivial, incl. tangent bundle
- Adams' result on vector fields on spheres: - Adams' result on vector fields on spheres:
there are maximally ρ(n)-1 indep.sections of the tangent bundle of S (n-1) 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: -- tangent bundle on S 2: