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

fix realprojective after sphere reindexing

Browse source
This commit is contained in:
Ulrik Buchholtz 2017-07-23 11:52:02 +02:00
parent 9a693f1ee3
commit d0995af5b5
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
homotopy/realprojective.hlean
View file

@ -200,8 +200,8 @@ structure two_cover :=
(cov_eq : Π x : carrier, ∥ bool = cov x ∥ ) (cov_eq : Π x : carrier, ∥ bool = cov x ∥ )
open two_cover open two_cover
definition empty_two_cover : two_cover := definition unit_two_cover : two_cover :=
two_cover.mk empty empty.elim (empty.rec _) two_cover.mk unit (λ u, bool) (λ u, tr idp)
open sigma.ops open sigma.ops
@ -221,7 +221,7 @@ begin
end end
definition realprojective_two_cover : ℕ → two_cover := definition realprojective_two_cover : ℕ → two_cover :=
nat.rec (two_cover_step empty_two_cover) (λ x, two_cover_step) nat.rec unit_two_cover (λ x, two_cover_step)
definition realprojective : ℕ → Type₀ := definition realprojective : ℕ → Type₀ :=
λ n, carrier (realprojective_two_cover n) λ n, carrier (realprojective_two_cover n)
@ -249,7 +249,7 @@ definition theorem_III_3 (n : ℕ)
: sphere n ≃ sigma (realprojective_cov n) := : sphere n ≃ sigma (realprojective_cov n) :=
begin begin
induction n with n IH, induction n with n IH,
{ symmetry, exact sorry }, { symmetry, apply sigma_unit_left },
{ apply equiv.trans (join_bool (sphere n))⁻¹ᵉ, { apply equiv.trans (join_bool (sphere n))⁻¹ᵉ,
apply equiv.trans (join_equiv_join erfl IH), apply equiv.trans (join_equiv_join erfl IH),
symmetry, refine equiv.trans _ !join_symm, symmetry, refine equiv.trans _ !join_symm,