make pointed suspension and spheres the default
There is one proof in realprojective which I couldn't quite fix, so for now I left a sorry
This commit is contained in:
Floris van Doorn
parent
a5c80f79c6
commit
3367c20f9d
23 changed files with 360 additions and 333 deletions
|
|
@ -22,3 +22,13 @@ Some of these things still need to be changes, some of them are already changed,
|
|||
- Type class inference for equivalences doesn't really work in Lean, since it recognizes that `f ∘ id` is definitionally `f`, hence it can always apply `is_equiv_compose` and get trapped in a loop.
|
||||
- Coercions should all be defined *immediately* after defining a structure, *before* declaring any
|
||||
instances. This is because the coercion graph is updated after each declared coercion.
|
||||
- When you have a functor in two arguments (`→`, `×`, `Π`, `Σ`, pointed versions of these, `=`, `∧`,
|
||||
`∨`, and so on), the functoriality should be stated in both arguments at once, and the special
|
||||
cases where only one argument changes should be a special case of that one. This makes it easier
|
||||
to prove properties about the functorial action, because you only have to do work once (although
|
||||
that work is sometimes twice as much, but sometimes much less). We haven't always done this,
|
||||
because it's sometimes easier to define a special case first (even though later you probably still
|
||||
have to define the general case). Note that for `=` this gives square filling as primitive,
|
||||
instead of concatenation (which can be seen as functoriality in the second argument), and Dan
|
||||
Licata argued for that as primitive instead of concatenation. On the other hand, the definition
|
||||
of the more general functor might be more complicated, in which case definitional reduction won't be as nice
|
||||
|
|
@ -58,8 +58,8 @@ namespace group
|
|||
refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp }
|
||||
end
|
||||
|
||||
definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) :
|
||||
loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) :=
|
||||
definition loop_susp_intro_pmap_mul {X Y : Type*} (f g : susp X →* Ω Y) :
|
||||
loop_susp_intro (pmap_mul f g) ~* pmap_mul (loop_susp_intro f) (loop_susp_intro g) :=
|
||||
pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose
|
||||
|
||||
definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) :=
|
||||
|
|
|
|||
|
|
@ -74,28 +74,28 @@ section prod
|
|||
definition wpr2 (A B : Type*) : (A ∨ B) →* B :=
|
||||
pmap.mk (wedge.elim (pconst A B) (pid B) idp) idp
|
||||
|
||||
definition ppr1_pprod_of_pwedge (A B : Type*)
|
||||
: ppr1 ∘* pprod_of_pwedge A B ~* wpr1 A B :=
|
||||
definition ppr1_pprod_of_wedge (A B : Type*)
|
||||
: ppr1 ∘* pprod_of_wedge A B ~* wpr1 A B :=
|
||||
begin
|
||||
fconstructor,
|
||||
{ intro w, induction w with a b,
|
||||
{ reflexivity },
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover, apply hdeg_square,
|
||||
apply trans (ap_compose ppr1 (pprod_of_pwedge A B) (pushout.glue star)),
|
||||
apply trans (ap_compose ppr1 (pprod_of_wedge A B) (pushout.glue star)),
|
||||
krewrite pushout.elim_glue, krewrite pushout.elim_glue } },
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition ppr2_pprod_of_pwedge (A B : Type*)
|
||||
: ppr2 ∘* pprod_of_pwedge A B ~* wpr2 A B :=
|
||||
definition ppr2_pprod_of_wedge (A B : Type*)
|
||||
: ppr2 ∘* pprod_of_wedge A B ~* wpr2 A B :=
|
||||
begin
|
||||
fconstructor,
|
||||
{ intro w, induction w with a b,
|
||||
{ reflexivity },
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover, apply hdeg_square,
|
||||
apply trans (ap_compose ppr2 (pprod_of_pwedge A B) (pushout.glue star)),
|
||||
apply trans (ap_compose ppr2 (pprod_of_wedge A B) (pushout.glue star)),
|
||||
krewrite pushout.elim_glue, krewrite pushout.elim_glue } },
|
||||
{ reflexivity }
|
||||
end
|
||||
|
|
@ -103,7 +103,7 @@ section prod
|
|||
end prod
|
||||
structure co_h_space [class] (A : Type*) :=
|
||||
(comul : A →* (A ∨ A))
|
||||
(colaw : pprod_of_pwedge A A ∘* comul ~* pdiag A)
|
||||
(colaw : pprod_of_wedge A A ∘* comul ~* pdiag A)
|
||||
|
||||
open co_h_space
|
||||
|
||||
|
|
@ -113,18 +113,18 @@ definition co_h_space_of_counit_laws {A : Type*}
|
|||
: co_h_space A :=
|
||||
co_h_space.mk c (pair_phomotopy
|
||||
(calc
|
||||
ppr1 ∘* pprod_of_pwedge A A ∘* c
|
||||
~* (ppr1 ∘* pprod_of_pwedge A A) ∘* c
|
||||
: (passoc ppr1 (pprod_of_pwedge A A) c)⁻¹*
|
||||
ppr1 ∘* pprod_of_wedge A A ∘* c
|
||||
~* (ppr1 ∘* pprod_of_wedge A A) ∘* c
|
||||
: (passoc ppr1 (pprod_of_wedge A A) c)⁻¹*
|
||||
... ~* wpr1 A A ∘* c
|
||||
: pwhisker_right c (ppr1_pprod_of_pwedge A A)
|
||||
: pwhisker_right c (ppr1_pprod_of_wedge A A)
|
||||
... ~* pid A : l)
|
||||
(calc
|
||||
ppr2 ∘* pprod_of_pwedge A A ∘* c
|
||||
~* (ppr2 ∘* pprod_of_pwedge A A) ∘* c
|
||||
: (passoc ppr2 (pprod_of_pwedge A A) c)⁻¹*
|
||||
ppr2 ∘* pprod_of_wedge A A ∘* c
|
||||
~* (ppr2 ∘* pprod_of_wedge A A) ∘* c
|
||||
: (passoc ppr2 (pprod_of_wedge A A) c)⁻¹*
|
||||
... ~* wpr2 A A ∘* c
|
||||
: pwhisker_right c (ppr2_pprod_of_pwedge A A)
|
||||
: pwhisker_right c (ppr2_pprod_of_wedge A A)
|
||||
... ~* pid A : r))
|
||||
|
||||
section
|
||||
|
|
@ -134,20 +134,20 @@ section
|
|||
definition counit_left : wpr1 A A ∘* comul A ~* pid A :=
|
||||
calc
|
||||
wpr1 A A ∘* comul A
|
||||
~* (ppr1 ∘* (pprod_of_pwedge A A)) ∘* comul A
|
||||
: (pwhisker_right (comul A) (ppr1_pprod_of_pwedge A A))⁻¹*
|
||||
... ~* ppr1 ∘* ((pprod_of_pwedge A A) ∘* comul A)
|
||||
: passoc ppr1 (pprod_of_pwedge A A) (comul A)
|
||||
~* (ppr1 ∘* (pprod_of_wedge A A)) ∘* comul A
|
||||
: (pwhisker_right (comul A) (ppr1_pprod_of_wedge A A))⁻¹*
|
||||
... ~* ppr1 ∘* ((pprod_of_wedge A A) ∘* comul A)
|
||||
: passoc ppr1 (pprod_of_wedge A A) (comul A)
|
||||
... ~* pid A
|
||||
: pwhisker_left ppr1 (colaw A)
|
||||
|
||||
definition counit_right : wpr2 A A ∘* comul A ~* pid A :=
|
||||
calc
|
||||
wpr2 A A ∘* comul A
|
||||
~* (ppr2 ∘* (pprod_of_pwedge A A)) ∘* comul A
|
||||
: (pwhisker_right (comul A) (ppr2_pprod_of_pwedge A A))⁻¹*
|
||||
... ~* ppr2 ∘* ((pprod_of_pwedge A A) ∘* comul A)
|
||||
: passoc ppr2 (pprod_of_pwedge A A) (comul A)
|
||||
~* (ppr2 ∘* (pprod_of_wedge A A)) ∘* comul A
|
||||
: (pwhisker_right (comul A) (ppr2_pprod_of_wedge A A))⁻¹*
|
||||
... ~* ppr2 ∘* ((pprod_of_wedge A A) ∘* comul A)
|
||||
: passoc ppr2 (pprod_of_wedge A A) (comul A)
|
||||
... ~* pid A
|
||||
: pwhisker_left ppr2 (colaw A)
|
||||
|
||||
|
|
@ -169,7 +169,7 @@ end
|
|||
section
|
||||
variable (A : Type*)
|
||||
|
||||
definition pinch : ⅀ A →* pwedge (⅀ A) (⅀ A) :=
|
||||
definition pinch : ⅀ A →* wedge (⅀ A) (⅀ A) :=
|
||||
begin
|
||||
fapply pmap.mk,
|
||||
{ intro sa, induction sa with a,
|
||||
|
|
@ -178,7 +178,7 @@ section
|
|||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition co_h_space_psusp : co_h_space (⅀ A) :=
|
||||
definition co_h_space_susp : co_h_space (⅀ A) :=
|
||||
co_h_space_of_counit_laws (pinch A)
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ exit
|
|||
open susp
|
||||
|
||||
|
||||
definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A :=
|
||||
definition susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : susp A :=
|
||||
begin
|
||||
induction x using smash.elim,
|
||||
{ induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ },
|
||||
|
|
@ -102,7 +102,7 @@ exit
|
|||
exact !elim_loop ⬝ !con.right_inv }
|
||||
end
|
||||
|
||||
definition smash_pcircle_of_psusp [unfold 2] (x : psusp A) : smash A S¹* :=
|
||||
definition smash_pcircle_of_susp [unfold 2] (x : susp A) : smash A S¹* :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact pt },
|
||||
|
|
@ -111,13 +111,13 @@ exit
|
|||
end
|
||||
|
||||
-- the definitions below compile, but take a long time to do so and have sorry's in them
|
||||
definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
|
||||
smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
|
||||
definition smash_pcircle_of_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
|
||||
smash_pcircle_of_susp (susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact gluel' pt a },
|
||||
{ exact abstract begin apply eq_pathover,
|
||||
refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
|
||||
refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _,
|
||||
refine ap02 _ (elim_loop north (merid a ⬝ (merid pt)⁻¹)) ⬝ph _,
|
||||
refine !ap_con ⬝ (!elim_merid ◾ (!ap_inv ⬝ !elim_merid⁻²)) ⬝ph _,
|
||||
-- make everything below this a lemma defined by path induction?
|
||||
|
|
@ -136,10 +136,10 @@ exit
|
|||
end end }
|
||||
end
|
||||
|
||||
-- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*)
|
||||
-- : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b)
|
||||
-- definition smash_pcircle_of_susp_of_smash_pcircle_gluer_base (b : S¹*)
|
||||
-- : square (smash_pcircle_of_susp_of_smash_pcircle_pt (Point A) b)
|
||||
-- (gluer pt)
|
||||
-- (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b)))
|
||||
-- (ap smash_pcircle_of_susp (ap (λ a, susp_of_smash_pcircle a) (gluer b)))
|
||||
-- (gluer b) :=
|
||||
-- begin
|
||||
-- refine ap02 _ !elim_gluer ⬝ph _,
|
||||
|
|
@ -149,36 +149,36 @@ exit
|
|||
-- end
|
||||
|
||||
exit
|
||||
definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A :=
|
||||
definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* susp A :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ fapply equiv.MK,
|
||||
{ exact psusp_of_smash_pcircle },
|
||||
{ exact smash_pcircle_of_psusp },
|
||||
{ exact susp_of_smash_pcircle },
|
||||
{ exact smash_pcircle_of_susp },
|
||||
{ exact abstract begin intro x, induction x,
|
||||
{ reflexivity },
|
||||
{ exact merid pt },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose psusp_of_smash_pcircle _ _ ⬝ph _,
|
||||
refine ap_compose susp_of_smash_pcircle _ _ ⬝ph _,
|
||||
refine ap02 _ !elim_merid ⬝ph _,
|
||||
rewrite [↑gluel', +ap_con, +ap_inv, -ap_compose'],
|
||||
refine (_ ◾ _⁻² ◾ _ ◾ (_ ◾ _⁻²)) ⬝ph _,
|
||||
rotate 5, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
|
||||
esimp, apply elim_loop, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
|
||||
rotate 5, do 2 (unfold [susp_of_smash_pcircle]; apply elim_gluel),
|
||||
esimp, apply elim_loop, do 2 (unfold [susp_of_smash_pcircle]; apply elim_gluel),
|
||||
refine idp_con (merid a ⬝ (merid (Point A))⁻¹) ⬝ph _,
|
||||
apply square_of_eq, refine !idp_con ⬝ _⁻¹, apply inv_con_cancel_right } end end },
|
||||
{ intro x, induction x using smash.rec,
|
||||
{ exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b },
|
||||
{ exact smash_pcircle_of_susp_of_smash_pcircle_pt a b },
|
||||
{ exact gluel pt },
|
||||
{ exact gluer pt },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
|
||||
unfold [psusp_of_smash_pcircle],
|
||||
refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _,
|
||||
unfold [susp_of_smash_pcircle],
|
||||
refine ap02 _ !elim_gluel ⬝ph _,
|
||||
esimp, apply whisker_rt, exact vrfl },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
|
||||
unfold [psusp_of_smash_pcircle],
|
||||
refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _,
|
||||
unfold [susp_of_smash_pcircle],
|
||||
refine ap02 _ !elim_gluer ⬝ph _,
|
||||
induction b,
|
||||
{ apply square_of_eq, exact whisker_right _ !con.right_inv },
|
||||
|
|
|
|||
|
|
@ -180,49 +180,49 @@ parametrized_cohomology_isomorphism_right
|
|||
|
||||
/- suspension axiom -/
|
||||
|
||||
definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
|
||||
definition cohomology_susp_2 (Y : spectrum) (n : ℤ) :
|
||||
Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) :=
|
||||
begin
|
||||
apply loopn_pequiv_loopn 2,
|
||||
exact loop_pequiv_loop (pequiv_of_eq (ap Y (add.right_comm n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ*
|
||||
end
|
||||
|
||||
definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
psusp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) :=
|
||||
definition cohomology_susp_1 (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
susp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) :=
|
||||
calc
|
||||
psusp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : psusp_adjoint_loop_unpointed
|
||||
susp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : susp_adjoint_loop_unpointed
|
||||
... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left
|
||||
(cohomology_psusp_2 Y n))
|
||||
(cohomology_susp_2 Y n))
|
||||
|
||||
definition cohomology_psusp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ}
|
||||
(f g : psusp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_psusp_1 X Y n (pmap_mul f g) ~*
|
||||
pmap_mul (cohomology_psusp_1 X Y n f) (cohomology_psusp_1 X Y n g) :=
|
||||
definition cohomology_susp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ}
|
||||
(f g : susp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_susp_1 X Y n (pmap_mul f g) ~*
|
||||
pmap_mul (cohomology_susp_1 X Y n f) (cohomology_susp_1 X Y n g) :=
|
||||
begin
|
||||
unfold [cohomology_psusp_1],
|
||||
refine pwhisker_left _ !loop_psusp_intro_pmap_mul ⬝* _,
|
||||
unfold [cohomology_susp_1],
|
||||
refine pwhisker_left _ !loop_susp_intro_pmap_mul ⬝* _,
|
||||
apply pcompose_pmap_mul
|
||||
end
|
||||
|
||||
definition cohomology_psusp_equiv (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
H^n+1[psusp X, Y] ≃ H^n[X, Y] :=
|
||||
trunc_equiv_trunc _ (cohomology_psusp_1 X Y n)
|
||||
definition cohomology_susp_equiv (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
H^n+1[susp X, Y] ≃ H^n[X, Y] :=
|
||||
trunc_equiv_trunc _ (cohomology_susp_1 X Y n)
|
||||
|
||||
definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
H^n+1[psusp X, Y] ≃g H^n[X, Y] :=
|
||||
isomorphism_of_equiv (cohomology_psusp_equiv X Y n)
|
||||
definition cohomology_susp (X : Type*) (Y : spectrum) (n : ℤ) :
|
||||
H^n+1[susp X, Y] ≃g H^n[X, Y] :=
|
||||
isomorphism_of_equiv (cohomology_susp_equiv X Y n)
|
||||
begin
|
||||
intro f₁ f₂, induction f₁ with f₁, induction f₂ with f₂,
|
||||
apply ap tr, apply eq_of_phomotopy, exact cohomology_psusp_1_pmap_mul f₁ f₂
|
||||
apply ap tr, apply eq_of_phomotopy, exact cohomology_susp_1_pmap_mul f₁ f₂
|
||||
end
|
||||
|
||||
definition cohomology_psusp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
|
||||
cohomology_psusp X Y n ∘ cohomology_functor (psusp_functor f) Y (n+1) ~
|
||||
cohomology_functor f Y n ∘ cohomology_psusp X' Y n :=
|
||||
definition cohomology_susp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
|
||||
cohomology_susp X Y n ∘ cohomology_functor (susp_functor f) Y (n+1) ~
|
||||
cohomology_functor f Y n ∘ cohomology_susp X' Y n :=
|
||||
begin
|
||||
refine (trunc_functor_compose _ _ _)⁻¹ʰᵗʸ ⬝hty _ ⬝hty trunc_functor_compose _ _ _,
|
||||
apply trunc_functor_homotopy, intro g,
|
||||
apply eq_of_phomotopy, refine _ ⬝* !passoc⁻¹*, apply pwhisker_left,
|
||||
apply loop_psusp_intro_natural
|
||||
apply loop_susp_intro_natural
|
||||
end
|
||||
|
||||
/- exactness -/
|
||||
|
|
@ -284,9 +284,9 @@ structure cohomology_theory.{u} : Type.{u+1} :=
|
|||
(Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
|
||||
(Hcompose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (z : HH n Z),
|
||||
Hh n (g ∘* f) z = Hh n f (Hh n g z))
|
||||
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
|
||||
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (susp X) ≃g HH n X)
|
||||
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y)
|
||||
Hsusp n X ∘ Hh (succ n) (susp_functor f) ~ Hh n f ∘ Hsusp n Y)
|
||||
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
|
||||
(Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
|
||||
is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
|
||||
|
|
@ -301,19 +301,19 @@ open cohomology_theory
|
|||
definition Hequiv (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X ≃* Y) : H n Y ≃ H n X :=
|
||||
equiv_of_isomorphism (Hiso H n f)
|
||||
|
||||
definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X :=
|
||||
definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (susp X) ≃g H (pred n) X :=
|
||||
isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X
|
||||
|
||||
definition Hsusp_neg_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
|
||||
Hsusp_neg H n X ∘ H ^→ n (psusp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y :=
|
||||
Hsusp_neg H n X ∘ H ^→ n (susp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y :=
|
||||
sorry
|
||||
|
||||
definition Hsusp_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
|
||||
H ^→ (succ n) (psusp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f :=
|
||||
H ^→ (succ n) (susp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f :=
|
||||
sorry
|
||||
|
||||
definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) :
|
||||
H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f :=
|
||||
H ^→ n (susp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f :=
|
||||
sorry
|
||||
|
||||
definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I → Type*) (H2 : has_choice 0 I)
|
||||
|
|
@ -346,7 +346,7 @@ end
|
|||
|
||||
-- definition Hwedge (H : cohomology_theory) (n : ℤ) (A B : Type*) : H n (A ∨ B) ≃g H n A ×ag H n B :=
|
||||
-- begin
|
||||
-- refine Hiso H n (pwedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _,
|
||||
-- refine Hiso H n (wedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _,
|
||||
-- refine Hadditive_equiv H n _ _ ⬝g _
|
||||
-- end
|
||||
|
||||
|
|
@ -360,8 +360,8 @@ cohomology_theory.mk
|
|||
(λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
|
||||
(λn A x, cohomology_functor_pid A Y n x)
|
||||
(λn A B C g f x, cohomology_functor_pcompose g f Y n x)
|
||||
(λn A, cohomology_psusp A Y n)
|
||||
(λn A B f, cohomology_psusp_natural f Y n)
|
||||
(λn A, cohomology_susp A Y n)
|
||||
(λn A B f, cohomology_susp_natural f Y n)
|
||||
(λn A B f, cohomology_exact f Y n)
|
||||
(λn I A H, spectrum_additive H A Y n)
|
||||
|
||||
|
|
|
|||
|
|
@ -20,15 +20,15 @@ namespace homology
|
|||
(Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
|
||||
(Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
|
||||
Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
|
||||
(Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
|
||||
(Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X)
|
||||
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (susp X) ≃g HH n X)
|
||||
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
|
||||
Hsusp n Y ∘ Hh (succ n) (susp_functor f) ~ Hh n f ∘ Hsusp n X)
|
||||
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
|
||||
(Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
|
||||
(dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
|
||||
|
||||
structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} :=
|
||||
(Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0))))
|
||||
(Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (sphere 0))))
|
||||
|
||||
section
|
||||
universe variable u
|
||||
|
|
@ -37,20 +37,20 @@ namespace homology
|
|||
|
||||
theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
|
||||
: HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
|
||||
calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ
|
||||
... ≃g HH theory n (pType.mk A b) : by exact Hpsusp theory n (pType.mk A b)
|
||||
calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (susp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
|
||||
... ≃g HH theory n (pType.mk A b) : by exact Hsusp theory n (pType.mk A b)
|
||||
|
||||
theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
|
||||
: Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
|
||||
calc Hh theory n (pmap.mk f p) x
|
||||
= Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x))
|
||||
: by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹
|
||||
... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x))
|
||||
: by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹
|
||||
... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x))
|
||||
: by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x)
|
||||
= Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x))
|
||||
: by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹
|
||||
... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp_functor' f) !refl) ((Hsusp theory n A)⁻¹ x))
|
||||
: by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹
|
||||
... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x))
|
||||
: by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x)
|
||||
... = Hh theory n (pmap.mk f q) x
|
||||
: by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)
|
||||
: by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
|
||||
|
||||
theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
|
||||
calc Hh theory n f x
|
||||
|
|
@ -122,8 +122,8 @@ namespace homology
|
|||
definition Hfwedge (n : ℤ) {I : Type} [is_set I] (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) :=
|
||||
(isomorphism.mk _ (Hadditive theory n X))⁻¹ᵍ
|
||||
|
||||
definition Hpwedge (n : ℤ) (A B : Type*) : HH theory n (pwedge A B) ≃g HH theory n A ×g HH theory n B :=
|
||||
calc HH theory n (A ∨ B) ≃g HH theory n (⋁ (bool.rec A B)) : by exact HH_isomorphism n (pwedge_pequiv_fwedge A B)
|
||||
definition Hwedge (n : ℤ) (A B : Type*) : HH theory n (wedge A B) ≃g HH theory n A ×g HH theory n B :=
|
||||
calc HH theory n (A ∨ B) ≃g HH theory n (⋁ (bool.rec A B)) : by exact HH_isomorphism n (wedge_pequiv_fwedge A B)
|
||||
... ≃g dirsum (λb, HH theory n (bool.rec A B b)) : by exact (Hadditive'_equiv n (bool.rec A B))⁻¹ᵍ
|
||||
... ≃g dirsum (bool.rec (HH theory n A) (HH theory n B)) : by exact dirsum_isomorphism (bool.rec !isomorphism.refl !isomorphism.refl)
|
||||
... ≃g HH theory n A ×g HH theory n B : by exact binary_dirsum (HH theory n A) (HH theory n B)
|
||||
|
|
@ -134,13 +134,13 @@ namespace homology
|
|||
parameter (theory : homology_theory.{max u v})
|
||||
open homology_theory
|
||||
|
||||
definition Hplift_psusp (n : ℤ) (A : Type*): HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory n (plift.{u v} A) :=
|
||||
calc HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory (n + 1) (psusp (plift.{u v} A)) : by exact HH_isomorphism theory (n + 1) (plift_psusp _)
|
||||
... ≃g HH theory n (plift.{u v} A) : by exact Hpsusp theory n (plift.{u v} A)
|
||||
definition Hplift_susp (n : ℤ) (A : Type*): HH theory (n + 1) (plift.{u v} (susp A)) ≃g HH theory n (plift.{u v} A) :=
|
||||
calc HH theory (n + 1) (plift.{u v} (susp A)) ≃g HH theory (n + 1) (susp (plift.{u v} A)) : by exact HH_isomorphism theory (n + 1) (plift_susp _)
|
||||
... ≃g HH theory n (plift.{u v} A) : by exact Hsusp theory n (plift.{u v} A)
|
||||
|
||||
definition Hplift_pwedge (n : ℤ) (A B : Type*): HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) :=
|
||||
calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_pwedge A B)
|
||||
... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hpwedge theory n (plift.{u v} A) (plift.{u v} B)
|
||||
definition Hplift_wedge (n : ℤ) (A B : Type*): HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) :=
|
||||
calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_wedge A B)
|
||||
... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hwedge theory n (plift.{u v} A) (plift.{u v} B)
|
||||
|
||||
definition Hplift_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B) : HH theory n (plift.{u v} A) ≃g HH theory n (plift.{u v} B) :=
|
||||
HH_isomorphism theory n (!pequiv_plift⁻¹ᵉ* ⬝e* e ⬝e* !pequiv_plift)
|
||||
|
|
@ -175,11 +175,12 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f :
|
|||
(g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
|
||||
pshomotopy_group_fun n (smash_prespectrum_fun f g)
|
||||
|
||||
print is_exact_g
|
||||
print is_exact
|
||||
definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) :
|
||||
is_exact_g (homology_functor f (sid (gen_spectrum.to_prespectrum E)) n)
|
||||
(homology_functor (pcod f) (sid (gen_spectrum.to_prespectrum E)) n) :=
|
||||
is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) :=
|
||||
begin
|
||||
esimp[is_exact_g],
|
||||
esimp [is_exact_g],
|
||||
-- fconstructor,
|
||||
-- { intro a, exact sorry },
|
||||
-- { intro a, exact sorry }
|
||||
|
|
@ -211,8 +212,8 @@ begin
|
|||
-- (λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
|
||||
-- (λn A x, cohomology_functor_pid A Y n x)
|
||||
-- (λn A B C g f x, cohomology_functor_pcompose g f Y n x)
|
||||
-- (λn A, cohomology_psusp A Y n)
|
||||
-- (λn A B f, cohomology_psusp_natural f Y n)
|
||||
-- (λn A, cohomology_susp A Y n)
|
||||
-- (λn A B f, cohomology_susp_natural f Y n)
|
||||
-- (λn A B f, cohomology_exact f Y n)
|
||||
-- (λn I A H, spectrum_additive H A Y n)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -17,18 +17,18 @@ section
|
|||
|
||||
open homology_theory
|
||||
|
||||
theorem Hpsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
|
||||
theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (sphere m)) ≃g HH theory (n - m) (plift (sphere 0)) :=
|
||||
begin
|
||||
intros n m, revert n, induction m with m,
|
||||
{ exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ },
|
||||
{ exact λ n, isomorphism_ap (λ n, HH theory n (plift (sphere 0))) (sub_zero n)⁻¹ },
|
||||
{ intro n, exact calc
|
||||
HH theory n (plift (psusp (psphere m)))
|
||||
≃g HH theory (succ (pred n)) (plift (psusp (psphere m)))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (plift (psusp (psphere m)))) (succ_pred n)⁻¹
|
||||
... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hplift_psusp theory (pred n) (psphere m)
|
||||
... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n)
|
||||
... ≃g HH theory (n - succ m) (plift (psphere 0))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))
|
||||
HH theory n (plift (susp (sphere m)))
|
||||
≃g HH theory (succ (pred n)) (plift (susp (sphere m)))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (plift (susp (sphere m)))) (succ_pred n)⁻¹
|
||||
... ≃g HH theory (pred n) (plift (sphere m)) : by exact Hplift_susp theory (pred n) (sphere m)
|
||||
... ≃g HH theory (pred n - m) (plift (sphere 0)) : by exact v_0 (pred n)
|
||||
... ≃g HH theory (n - succ m) (plift (sphere 0))
|
||||
: by exact isomorphism_ap (λ n, HH theory n (plift (sphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))
|
||||
}
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -17,23 +17,23 @@ section
|
|||
|
||||
open ordinary_homology_theory
|
||||
|
||||
theorem Hptorus : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m ×* psphere m)) ≃g
|
||||
HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))) := λ n m,
|
||||
calc HH theory n (plift (psphere m ×* psphere m))
|
||||
≃g HH theory (n + 1) (plift (⅀ (psphere m ×* psphere m))) : by exact (Hplift_psusp theory n (psphere m ×* psphere m))⁻¹ᵍ
|
||||
... ≃g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m) ∨ ⅀ (psphere m ∧ psphere m))))
|
||||
: by exact Hplift_isomorphism theory (n + 1) (susp_product (psphere m) (psphere m))
|
||||
... ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))))
|
||||
: by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m)))
|
||||
... ≃g HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m))))
|
||||
: by exact product_isomorphism (Hplift_psusp theory n (psphere m))
|
||||
theorem Hptorus : Π(n : ℤ)(m : ℕ), HH theory n (plift (sphere m ×* sphere m)) ≃g
|
||||
HH theory n (plift (sphere m)) ×g (HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m)))) := λ n m,
|
||||
calc HH theory n (plift (sphere m ×* sphere m))
|
||||
≃g HH theory (n + 1) (plift (⅀ (sphere m ×* sphere m))) : by exact (Hplift_susp theory n (sphere m ×* sphere m))⁻¹ᵍ
|
||||
... ≃g HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m) ∨ ⅀ (sphere m ∧ sphere m))))
|
||||
: by exact Hplift_isomorphism theory (n + 1) (susp_product (sphere m) (sphere m))
|
||||
... ≃g HH theory (n + 1) (plift (⅀ (sphere m))) ×g HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m))))
|
||||
: by exact Hplift_wedge theory (n + 1) (⅀ (sphere m)) (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m)))
|
||||
... ≃g HH theory n (plift (sphere m)) ×g (HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m))))
|
||||
: by exact product_isomorphism (Hplift_susp theory n (sphere m))
|
||||
(calc
|
||||
HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))))
|
||||
≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m ∧ psphere m)))
|
||||
: by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m ∧ psphere m))
|
||||
... ≃g HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))
|
||||
: by exact product_isomorphism (Hplift_psusp theory n (psphere m))
|
||||
(Hplift_psusp theory n (psphere m ∧ psphere m) ⬝g Hplift_isomorphism theory n (sphere_smash_sphere m m)))
|
||||
HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m))))
|
||||
≃g HH theory (n + 1) (plift (⅀ (sphere m))) ×g HH theory (n + 1) (plift (⅀ (sphere m ∧ sphere m)))
|
||||
: by exact Hplift_wedge theory (n + 1) (⅀ (sphere m)) (⅀ (sphere m ∧ sphere m))
|
||||
... ≃g HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m)))
|
||||
: by exact product_isomorphism (Hplift_susp theory n (sphere m))
|
||||
(Hplift_susp theory n (sphere m ∧ sphere m) ⬝g Hplift_isomorphism theory n (sphere_smash_sphere m m)))
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
-- Authors: Floris van Doorn
|
||||
|
||||
import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
|
||||
..move_to_lib .susp
|
||||
..move_to_lib .susp ..algebra.quotient_group
|
||||
|
||||
open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
|
||||
|
||||
|
|
@ -10,7 +10,7 @@ open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp func
|
|||
namespace EM
|
||||
|
||||
definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
|
||||
EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (psusp_functor (EMadd1_functor φ n)) :=
|
||||
EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (susp_functor (EMadd1_functor φ n)) :=
|
||||
by reflexivity
|
||||
|
||||
definition EM1_functor_gid (G : Group) : EM1_functor (gid G) ~* !pid :=
|
||||
|
|
@ -28,7 +28,7 @@ namespace EM
|
|||
induction n with n p,
|
||||
{ apply EM1_functor_gid },
|
||||
{ refine !EMadd1_functor_succ ⬝* _,
|
||||
refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pid) ⬝* _,
|
||||
refine ptrunc_functor_phomotopy _ (susp_functor_phomotopy p ⬝* !susp_functor_pid) ⬝* _,
|
||||
apply ptrunc_functor_pid }
|
||||
end
|
||||
|
||||
|
|
@ -58,7 +58,7 @@ namespace EM
|
|||
induction n with n p,
|
||||
{ apply EM1_functor_gcompose },
|
||||
{ refine !EMadd1_functor_succ ⬝* _,
|
||||
refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pcompose) ⬝* _,
|
||||
refine ptrunc_functor_phomotopy _ (susp_functor_phomotopy p ⬝* !susp_functor_pcompose) ⬝* _,
|
||||
apply ptrunc_functor_pcompose }
|
||||
end
|
||||
|
||||
|
|
@ -87,7 +87,7 @@ namespace EM
|
|||
begin
|
||||
induction n with n q,
|
||||
{ exact EM1_functor_phomotopy p },
|
||||
{ exact ptrunc_functor_phomotopy _ (psusp_functor_phomotopy q) }
|
||||
{ exact ptrunc_functor_phomotopy _ (susp_functor_phomotopy q) }
|
||||
end
|
||||
|
||||
definition EM_functor_phomotopy {G H : AbGroup} {φ ψ : G →g H} (p : φ ~ ψ) (n : ℕ) :
|
||||
|
|
@ -154,7 +154,7 @@ namespace EM
|
|||
-- is_trunc_EMadd1 G n
|
||||
|
||||
definition loop_EMadd1_succ (G : AbGroup) (n : ℕ) :
|
||||
loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (psusp (EMadd1 G (n+1))))⁻¹ᵉ* ∘*
|
||||
loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (susp (EMadd1 G (n+1))))⁻¹ᵉ* ∘*
|
||||
freudenthal_pequiv (EMadd1 G (n+1)) (add_mul_le_mul_add n 1 1) ∘*
|
||||
(ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* :=
|
||||
by reflexivity
|
||||
|
|
@ -166,7 +166,7 @@ namespace EM
|
|||
induction n with n IH,
|
||||
{ refine pwhisker_left _ !hopf.to_pmap_delooping_pinv ⬝* _ ⬝*
|
||||
pwhisker_right _ !hopf.to_pmap_delooping_pinv⁻¹*,
|
||||
refine !loop_psusp_unit_natural⁻¹* ⬝h* _,
|
||||
refine !loop_susp_unit_natural⁻¹* ⬝h* _,
|
||||
apply ap1_psquare,
|
||||
apply ptr_natural },
|
||||
{ refine pwhisker_left _ !loop_EMadd1_succ ⬝* _ ⬝* pwhisker_right _ !loop_EMadd1_succ⁻¹*,
|
||||
|
|
@ -175,7 +175,7 @@ namespace EM
|
|||
refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _ ⬝*
|
||||
pwhisker_right _ !to_pmap_freudenthal_pequiv⁻¹*,
|
||||
apply ptrunc_functor_psquare,
|
||||
exact !loop_psusp_unit_natural⁻¹* }
|
||||
exact !loop_susp_unit_natural⁻¹* }
|
||||
end
|
||||
|
||||
definition apn_EMadd1_pequiv_EM1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) :
|
||||
|
|
@ -264,10 +264,10 @@ namespace EM
|
|||
refine (ptrunc_elim_pcompose ((succ n).+1) _ _)⁻¹* ⬝* _ ⬝*
|
||||
(ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*,
|
||||
apply ptrunc_elim_phomotopy,
|
||||
refine _ ⬝* !psusp_elim_psusp_functor⁻¹*,
|
||||
refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1)
|
||||
refine _ ⬝* !susp_elim_susp_functor⁻¹*,
|
||||
refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1)
|
||||
(@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)),
|
||||
apply psusp_elim_natural }
|
||||
apply susp_elim_natural }
|
||||
end
|
||||
|
||||
definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G)
|
||||
|
|
@ -374,7 +374,7 @@ namespace EM
|
|||
-- { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) },
|
||||
-- rewrite [EMadd1_succ],
|
||||
-- exact ptrunc.elim ((succ n).+1)
|
||||
-- (psusp.elim (f _ (EM_up e) (is_mul_hom_EM_up e r) _ _)),
|
||||
-- (susp.elim (f _ (EM_up e) (is_mul_hom_EM_up e r) _ _)),
|
||||
-- end
|
||||
|
||||
-- definition is_set_pmap_ptruncconntype {n : ℕ₋₂} (X Y : (n.+1)-Type*[n]) : is_set (X →* Y) :=
|
||||
|
|
@ -550,7 +550,7 @@ namespace EM
|
|||
begin
|
||||
induction n with n IH,
|
||||
{ exact is_contr_EM1 H },
|
||||
{ have is_contr (ptrunc (n+2) (psusp (EMadd1 G n))), from _,
|
||||
{ have is_contr (ptrunc (n+2) (susp (EMadd1 G n))), from _,
|
||||
exact this }
|
||||
end
|
||||
|
||||
|
|
@ -640,6 +640,7 @@ namespace EM
|
|||
-- end
|
||||
|
||||
|
||||
open group algebra
|
||||
definition homotopy_group_fiber_EM1_functor {G H : Group} (φ : G →g H) :
|
||||
π₁ (pfiber (EM1_functor φ)) ≃g kernel φ :=
|
||||
sorry
|
||||
|
|
|
|||
|
|
@ -86,14 +86,14 @@ namespace sphere
|
|||
{ unfold [πnSn], exact sorry}
|
||||
end
|
||||
|
||||
definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ :=
|
||||
definition deg {n : ℕ} [H : is_succ n] (f : S n →* S n) : ℤ :=
|
||||
by induction H with n; exact πnSn n (π→g[n+1] f (tr surf))
|
||||
|
||||
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) :=
|
||||
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S n)) = (1 : ℤ) :=
|
||||
by induction H with n;
|
||||
exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n
|
||||
exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n
|
||||
|
||||
definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) :
|
||||
definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S n →* S n} (p : f ~* g) :
|
||||
deg f = deg g :=
|
||||
begin
|
||||
induction H with n,
|
||||
|
|
@ -115,7 +115,7 @@ namespace sphere
|
|||
{ symmetry, exact to_right_inv (equiv_of_isomorphism e) n}
|
||||
end
|
||||
|
||||
definition deg_compose {n : ℕ} [H : is_succ n] (f g : S* n →* S* n) :
|
||||
definition deg_compose {n : ℕ} [H : is_succ n] (f g : S n →* S n) :
|
||||
deg (g ∘* f) = deg g *[ℤ] deg f :=
|
||||
begin
|
||||
induction H with n,
|
||||
|
|
@ -123,7 +123,7 @@ namespace sphere
|
|||
apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g)
|
||||
end
|
||||
|
||||
definition deg_equiv {n : ℕ} [H : is_succ n] (f : S* n ≃* S* n) :
|
||||
definition deg_equiv {n : ℕ} [H : is_succ n] (f : S n ≃* S n) :
|
||||
deg f = 1 ⊎ deg f = -1 :=
|
||||
begin
|
||||
induction H with n,
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ attribute fwedge.il fwedge.inl [constructor]
|
|||
|
||||
namespace fwedge
|
||||
|
||||
definition fwedge_of_pwedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) :=
|
||||
definition fwedge_of_wedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) :=
|
||||
begin
|
||||
induction x with a b,
|
||||
{ exact inl ff a },
|
||||
|
|
@ -56,7 +56,7 @@ namespace fwedge
|
|||
{ exact glue ff ⬝ (glue tt)⁻¹ }
|
||||
end
|
||||
|
||||
definition pwedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B :=
|
||||
definition wedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B :=
|
||||
begin
|
||||
induction x with b x b,
|
||||
{ induction b, exact pushout.inl x, exact pushout.inr x },
|
||||
|
|
@ -64,24 +64,24 @@ namespace fwedge
|
|||
{ induction b, exact pushout.glue ⋆, reflexivity }
|
||||
end
|
||||
|
||||
definition pwedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) :=
|
||||
definition wedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ fapply equiv.MK,
|
||||
{ exact fwedge_of_pwedge },
|
||||
{ exact pwedge_of_fwedge },
|
||||
{ exact fwedge_of_wedge },
|
||||
{ exact wedge_of_fwedge },
|
||||
{ exact abstract begin intro x, induction x with b x b,
|
||||
{ induction b: reflexivity },
|
||||
{ exact glue tt },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose fwedge_of_pwedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
|
||||
refine ap_compose fwedge_of_wedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
|
||||
induction b, exact !elim_glue ⬝ph whisker_bl _ hrfl, apply square_of_eq idp }
|
||||
end end },
|
||||
{ exact abstract begin intro x, induction x with a b,
|
||||
{ reflexivity },
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose pwedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝
|
||||
refine ap_compose wedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝
|
||||
!elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) ⬝ph _, exact hrfl } end end}},
|
||||
{ exact glue ff }
|
||||
end
|
||||
|
|
@ -104,7 +104,7 @@ namespace fwedge
|
|||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition pwedge_pmap [constructor] {A B : Type*} {X : Type*} (f : A →* X) (g : B →* X) : (A ∨ B) →* X :=
|
||||
definition wedge_pmap [constructor] {A B : Type*} {X : Type*} (f : A →* X) (g : B →* X) : (A ∨ B) →* X :=
|
||||
begin
|
||||
fapply pmap.mk,
|
||||
{ intro x, induction x, exact (f a), exact (g a), exact (respect_pt (f) ⬝ (respect_pt g)⁻¹) },
|
||||
|
|
@ -149,9 +149,9 @@ namespace fwedge
|
|||
{ intro g, apply eq_of_phomotopy, exact fwedge_pmap_eta g }
|
||||
end
|
||||
|
||||
definition pwedge_pmap_equiv [constructor] (A B X : Type*) :
|
||||
definition wedge_pmap_equiv [constructor] (A B X : Type*) :
|
||||
((A ∨ B) →* X) ≃ ((A →* X) × (B →* X)) :=
|
||||
calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)⁻¹ᵉ*
|
||||
calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact pequiv_ppcompose_right (wedge_pequiv_fwedge A B)⁻¹ᵉ*
|
||||
... ≃ Πi, (bool.rec A B) i →* X : by exact fwedge_pmap_equiv (bool.rec A B) X
|
||||
... ≃ (A →* X) × (B →* X) : by exact pi_bool_left (λ i, bool.rec A B i →* X)
|
||||
|
||||
|
|
@ -211,16 +211,16 @@ namespace fwedge
|
|||
end
|
||||
|
||||
-- hsquare 3:
|
||||
definition fwedge_to_pwedge_nat_square {A B X Y : Type*} (f : X →* Y) :
|
||||
hsquare (pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)) (pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) :=
|
||||
definition fwedge_to_wedge_nat_square {A B X Y : Type*} (f : X →* Y) :
|
||||
hsquare (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) :=
|
||||
begin
|
||||
exact sorry
|
||||
end
|
||||
|
||||
definition pwedge_pmap_nat₂ (A B X Y : Type*) (f : X →* Y) (h : A →* X) (k : B →* X) : Π (w : A ∨ B),
|
||||
(f ∘* (pwedge_pmap h k)) w = pwedge_pmap (f ∘* h )(f ∘* k) w :=
|
||||
definition wedge_pmap_nat₂ (A B X Y : Type*) (f : X →* Y) (h : A →* X) (k : B →* X) : Π (w : A ∨ B),
|
||||
(f ∘* (wedge_pmap h k)) w = wedge_pmap (f ∘* h )(f ∘* k) w :=
|
||||
have H : _, from
|
||||
(@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_pwedge_nat_square f),
|
||||
(@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_wedge_nat_square f),
|
||||
sorry
|
||||
|
||||
-- SA to here 7/5
|
||||
|
|
|
|||
|
|
@ -501,7 +501,7 @@ namespace pushout
|
|||
|
||||
/- cofiber of pcod is suspension -/
|
||||
|
||||
definition pcofiber_pcod {A B : Type*} (f : A →* B) : pcofiber (pcod f) ≃* psusp A :=
|
||||
definition pcofiber_pcod {A B : Type*} (f : A →* B) : pcofiber (pcod f) ≃* susp A :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ refine !pushout.symm ⬝e _,
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
import homotopy.join
|
||||
|
||||
open eq nat susp pointed pmap sigma is_equiv equiv fiber is_trunc trunc
|
||||
trunc_index is_conn sphere_index bool unit join pushout
|
||||
trunc_index is_conn bool unit join pushout
|
||||
|
||||
definition of_is_contr (A : Type) : is_contr A → A := @center A
|
||||
|
||||
|
|
@ -23,7 +23,7 @@ definition sigma_eq_equiv' {A : Type} (B : A → Type)
|
|||
: (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) ≃ (Σ(p : a₁ = a₂), p ▸ b₁ = b₂) :=
|
||||
calc (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩)
|
||||
≃ Σ(p : a₁ = a₂), b₁ =[p] b₂ : sigma_eq_equiv
|
||||
... ≃ Σ(p : a₁ = a₂), p ▸ b₁ = b₂
|
||||
... ≃ Σ(p : a₁ = a₂), p ▸ b₁ = b₂
|
||||
: by apply sigma_equiv_sigma_right; intro e; apply pathover_equiv_tr_eq
|
||||
|
||||
definition dec_eq_is_prop [instance] (A : Type) : is_prop (decidable_eq A) :=
|
||||
|
|
@ -88,7 +88,7 @@ calc (A = B)
|
|||
... ≃ (BoolType.carrier A = BoolType.carrier B)
|
||||
: begin
|
||||
induction A with A p, induction B with B q,
|
||||
symmetry, esimp, apply equiv_subtype
|
||||
symmetry, esimp, apply equiv_subtype
|
||||
end
|
||||
... ≃ (A ≃ B) : eq_equiv_equiv A B
|
||||
|
||||
|
|
@ -134,7 +134,7 @@ begin
|
|||
induction f with f, induction f, induction x,
|
||||
{ apply is_contr.mk ⟨ equiv_bnot, idp ⟩,
|
||||
intro w, induction w with e p, symmetry,
|
||||
apply to_inv (lemma_II_4 tt ff e equiv_bnot p idp),
|
||||
apply to_inv (lemma_II_4 tt ff e equiv_bnot p idp),
|
||||
fapply sigma.mk,
|
||||
{ intro b, induction b,
|
||||
{ exact theorem_II_2_lemma_2 e p },
|
||||
|
|
@ -220,19 +220,19 @@ begin
|
|||
{ intro w, apply is_prop.elimo } }
|
||||
end
|
||||
|
||||
definition realprojective_two_cover : ℕ₋₁ → two_cover :=
|
||||
sphere_index.rec empty_two_cover (λ x, two_cover_step)
|
||||
definition realprojective_two_cover : ℕ → two_cover :=
|
||||
nat.rec (two_cover_step empty_two_cover) (λ x, two_cover_step)
|
||||
|
||||
definition realprojective : ℕ₋₁ → Type₀ :=
|
||||
definition realprojective : ℕ → Type₀ :=
|
||||
λ n, carrier (realprojective_two_cover n)
|
||||
|
||||
definition realprojective_cov [reducible] (n : ℕ₋₁)
|
||||
definition realprojective_cov [reducible] (n : ℕ)
|
||||
: realprojective n → BoolType :=
|
||||
λ x, BoolType.mk
|
||||
(cov (realprojective_two_cover n) x)
|
||||
(cov_eq (realprojective_two_cover n) x)
|
||||
|
||||
definition theorem_III_3_u [reducible] (n : ℕ₋₁)
|
||||
definition theorem_III_3_u [reducible] (n : ℕ)
|
||||
: (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
|
||||
≃ (Σ x, realprojective_cov n x) × bool :=
|
||||
calc (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
|
||||
|
|
@ -245,14 +245,14 @@ calc (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
|
|||
... ≃ (Σ x, realprojective_cov n x) × bool
|
||||
: equiv_prod
|
||||
|
||||
definition theorem_III_3 (n : ℕ₋₁)
|
||||
definition theorem_III_3 (n : ℕ)
|
||||
: sphere n ≃ sigma (realprojective_cov n) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ symmetry, apply sigma_empty_left },
|
||||
{ apply equiv.trans (join.bool (sphere n))⁻¹ᵉ,
|
||||
apply equiv.trans (join.equiv_closed erfl IH),
|
||||
symmetry, refine equiv.trans _ !join.symm,
|
||||
{ symmetry, apply sorry /-sigma_empty_left-/ },
|
||||
{ apply equiv.trans (join_bool (sphere n))⁻¹ᵉ,
|
||||
apply equiv.trans (join_equiv_join erfl IH),
|
||||
symmetry, refine equiv.trans _ !join_symm,
|
||||
apply equiv.trans !pushout.flattening, esimp,
|
||||
fapply pushout.equiv,
|
||||
{ unfold function.compose, exact theorem_III_3_u n},
|
||||
|
|
|
|||
|
|
@ -752,9 +752,9 @@ namespace smash
|
|||
definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
|
||||
smash_pequiv pequiv.rfl g
|
||||
|
||||
/- A ∧ B ≃* pcofiber (pprod_of_pwedge A B) -/
|
||||
/- A ∧ B ≃* pcofiber (pprod_of_wedge A B) -/
|
||||
|
||||
definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B :=
|
||||
definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B :=
|
||||
begin
|
||||
induction v with a b ,
|
||||
{ exact (a, pt) },
|
||||
|
|
@ -762,7 +762,7 @@ namespace smash
|
|||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition wedge_of_sum [unfold 3] (v : A + B) : pwedge A B :=
|
||||
definition wedge_of_sum [unfold 3] (v : A + B) : wedge A B :=
|
||||
begin
|
||||
induction v with a b,
|
||||
{ exact pushout.inl a },
|
||||
|
|
@ -780,7 +780,7 @@ end smash open smash
|
|||
|
||||
namespace pushout
|
||||
|
||||
definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : pwedge A B) :
|
||||
definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : wedge A B) :
|
||||
inl pt = inl v :> pushout wedge_of_sum bool_of_sum :=
|
||||
begin
|
||||
induction v with a b,
|
||||
|
|
@ -856,14 +856,14 @@ namespace smash
|
|||
refine !con.right_inv ⬝pv _, exact square_of_eq idp },
|
||||
end
|
||||
|
||||
definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
|
||||
definition pprod_of_wedge [constructor] : wedge A B →* A ×* B :=
|
||||
begin
|
||||
fconstructor,
|
||||
{ exact prod_of_wedge },
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
|
||||
definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_wedge A B) :=
|
||||
begin
|
||||
apply pequiv_of_equiv (smash_equiv_cofiber A B),
|
||||
exact cofiber.glue pt
|
||||
|
|
|
|||
|
|
@ -506,77 +506,78 @@ namespace smash
|
|||
end
|
||||
|
||||
/- Corollary 2: smashing with a suspension -/
|
||||
definition smash_psusp_elim_equiv (A B X : Type*) :
|
||||
ppmap (A ∧ psusp B) X ≃* ppmap (psusp (A ∧ B)) X :=
|
||||
definition smash_susp_elim_equiv (A B X : Type*) :
|
||||
ppmap (A ∧ susp B) X ≃* ppmap (susp (A ∧ B)) X :=
|
||||
calc
|
||||
ppmap (A ∧ psusp B) X ≃* ppmap (psusp B) (ppmap A X) : smash_adjoint_pmap A (psusp B) X
|
||||
... ≃* ppmap B (Ω (ppmap A X)) : psusp_adjoint_loop' B (ppmap A X)
|
||||
ppmap (A ∧ susp B) X ≃* ppmap (susp B) (ppmap A X) : smash_adjoint_pmap A (susp B) X
|
||||
... ≃* ppmap B (Ω (ppmap A X)) : susp_adjoint_loop' B (ppmap A X)
|
||||
... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute A X)
|
||||
... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
|
||||
... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X
|
||||
... ≃* ppmap (susp (A ∧ B)) X : susp_adjoint_loop' (A ∧ B) X
|
||||
|
||||
definition smash_psusp_elim_natural_right (A B : Type*) (f : X →* X') :
|
||||
psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A B X')
|
||||
definition smash_susp_elim_natural_right (A B : Type*) (f : X →* X') :
|
||||
psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A B X')
|
||||
(ppcompose_left f) (ppcompose_left f) :=
|
||||
smash_adjoint_pmap_natural_right f ⬝h*
|
||||
psusp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
|
||||
susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h*
|
||||
ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h*
|
||||
(smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h*
|
||||
(psusp_adjoint_loop_natural_right f)⁻¹ʰ*
|
||||
(susp_adjoint_loop_natural_right f)⁻¹ʰ*
|
||||
|
||||
definition smash_psusp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
|
||||
psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A' B' X)
|
||||
(ppcompose_right (f ∧→ psusp_functor g)) (ppcompose_right (psusp_functor (f ∧→ g))) :=
|
||||
definition smash_susp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) :
|
||||
psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A' B' X)
|
||||
(ppcompose_right (f ∧→ susp_functor g)) (ppcompose_right (susp_functor (f ∧→ g))) :=
|
||||
begin
|
||||
refine smash_adjoint_pmap_natural_lm X f (psusp_functor g) ⬝h*
|
||||
refine smash_adjoint_pmap_natural_lm X f (susp_functor g) ⬝h*
|
||||
_ ⬝h* _ ⬝h*
|
||||
(smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h*
|
||||
(psusp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*,
|
||||
(susp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*,
|
||||
rotate 2,
|
||||
exact !ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare (loop_pmap_commute_natural_left X f),
|
||||
exact psusp_adjoint_loop_natural_left g ⬝v* psusp_adjoint_loop_natural_right (ppcompose_right f)
|
||||
exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right (ppcompose_right f)
|
||||
end
|
||||
|
||||
definition smash_psusp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
|
||||
definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
|
||||
begin
|
||||
fapply pequiv.MK,
|
||||
{ exact !smash_psusp_elim_equiv⁻¹ᵉ* !pid },
|
||||
{ exact !smash_psusp_elim_equiv !pid },
|
||||
{ refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
|
||||
refine pap !smash_psusp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
|
||||
apply phomotopy_of_eq, apply to_left_inv !smash_psusp_elim_equiv },
|
||||
{ refine phomotopy_of_eq (!smash_psusp_elim_natural_right _) ⬝* _,
|
||||
refine pap !smash_psusp_elim_equiv !pcompose_pid ⬝* _,
|
||||
apply phomotopy_of_eq, apply to_right_inv !smash_psusp_elim_equiv }
|
||||
{ exact !smash_susp_elim_equiv⁻¹ᵉ* !pid },
|
||||
{ exact !smash_susp_elim_equiv !pid },
|
||||
{ refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _,
|
||||
refine pap !smash_susp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
|
||||
apply phomotopy_of_eq, apply to_left_inv !smash_susp_elim_equiv },
|
||||
{ refine phomotopy_of_eq (!smash_susp_elim_natural_right _) ⬝* _,
|
||||
refine pap !smash_susp_elim_equiv !pcompose_pid ⬝* _,
|
||||
apply phomotopy_of_eq, apply to_right_inv !smash_susp_elim_equiv }
|
||||
end
|
||||
|
||||
definition smash_psusp_natural (f : A →* A') (g : B →* B') :
|
||||
psquare (smash_psusp A B) (smash_psusp A' B') (f ∧→ (psusp_functor g)) (psusp_functor (f ∧→ g)) :=
|
||||
definition smash_susp_natural (f : A →* A') (g : B →* B') :
|
||||
psquare (smash_susp A B) (smash_susp A' B') (f ∧→ (susp_functor g)) (susp_functor (f ∧→ g)) :=
|
||||
begin
|
||||
refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
|
||||
refine pap !smash_psusp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
|
||||
rexact phomotopy_of_eq ((smash_psusp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹
|
||||
refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _,
|
||||
refine pap !smash_susp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
|
||||
rexact phomotopy_of_eq ((smash_susp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹
|
||||
end
|
||||
|
||||
definition smash_iterate_psusp (n : ℕ) (A B : Type*) : A ∧ iterate_psusp n B ≃* iterate_psusp n (A ∧ B) :=
|
||||
print axioms smash_susp_natural
|
||||
definition smash_iterate_susp (n : ℕ) (A B : Type*) : A ∧ iterate_susp n B ≃* iterate_susp n (A ∧ B) :=
|
||||
begin
|
||||
induction n with n e,
|
||||
{ reflexivity },
|
||||
{ exact smash_psusp A (iterate_psusp n B) ⬝e* psusp_pequiv e }
|
||||
{ exact smash_susp A (iterate_susp n B) ⬝e* susp_pequiv e }
|
||||
end
|
||||
|
||||
definition smash_sphere (A : Type*) (n : ℕ) : A ∧ psphere n ≃* iterate_psusp n A :=
|
||||
smash_pequiv pequiv.rfl (psphere_pequiv_iterate_psusp n) ⬝e*
|
||||
smash_iterate_psusp n A pbool ⬝e*
|
||||
iterate_psusp_pequiv n (smash_pbool_pequiv A)
|
||||
definition smash_sphere (A : Type*) (n : ℕ) : A ∧ sphere n ≃* iterate_susp n A :=
|
||||
smash_pequiv pequiv.rfl (sphere_pequiv_iterate_susp n) ⬝e*
|
||||
smash_iterate_susp n A pbool ⬝e*
|
||||
iterate_susp_pequiv n (smash_pbool_pequiv A)
|
||||
|
||||
definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* psusp A :=
|
||||
definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* susp A :=
|
||||
smash_sphere A 1
|
||||
|
||||
definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) :=
|
||||
smash_sphere (psphere n) m ⬝e*
|
||||
iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e*
|
||||
iterate_psusp_iterate_psusp_rev m n pbool ⬝e*
|
||||
(psphere_pequiv_iterate_psusp (n + m))⁻¹ᵉ*
|
||||
definition sphere_smash_sphere (n m : ℕ) : sphere n ∧ sphere m ≃* sphere (n+m) :=
|
||||
smash_sphere (sphere n) m ⬝e*
|
||||
iterate_susp_pequiv m (sphere_pequiv_iterate_susp n) ⬝e*
|
||||
iterate_susp_iterate_susp_rev m n pbool ⬝e*
|
||||
(sphere_pequiv_iterate_susp (n + m))⁻¹ᵉ*
|
||||
|
||||
end smash
|
||||
|
|
|
|||
|
|
@ -1,29 +1,29 @@
|
|||
import homotopy.join homotopy.smash
|
||||
import homotopy.join homotopy.smash types.nat.hott
|
||||
|
||||
open eq equiv trunc function bool join sphere sphere_index sphere.ops prod
|
||||
open pointed sigma smash is_trunc
|
||||
open eq equiv trunc function bool join sphere sphere.ops prod
|
||||
open pointed sigma smash is_trunc nat
|
||||
|
||||
namespace spherical_fibrations
|
||||
|
||||
/- classifying type of spherical fibrations -/
|
||||
definition BG (n : ℕ) : Type₁ :=
|
||||
Σ(X : Type₀), ∥ X ≃ S n..-1 ∥
|
||||
definition BG (n : ℕ) [is_succ n] : Type₁ :=
|
||||
Σ(X : Type₀), ∥ X ≃ S (pred n) ∥
|
||||
|
||||
definition pointed_BG [instance] [constructor] (n : ℕ) : pointed (BG n) :=
|
||||
pointed.mk ⟨ S n..-1 , tr erfl ⟩
|
||||
definition pointed_BG [instance] [constructor] (n : ℕ) [is_succ n] : pointed (BG n) :=
|
||||
pointed.mk ⟨ S (pred n) , tr erfl ⟩
|
||||
|
||||
definition pBG [constructor] (n : ℕ) : Type* := pointed.mk' (BG n)
|
||||
definition pBG [constructor] (n : ℕ) [is_succ n] : Type* := pointed.mk' (BG n)
|
||||
|
||||
definition G (n : ℕ) : Type₁ :=
|
||||
definition G (n : ℕ) [is_succ n] : Type₁ :=
|
||||
pt = pt :> BG n
|
||||
|
||||
definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) :=
|
||||
definition G_char (n : ℕ) [is_succ n] : G n ≃ (S (pred n) ≃ S (pred n)) :=
|
||||
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
|
||||
G n ≃ Σ(p : pType.carrier (S (pred n)) = pType.carrier (S (pred n))), _ : sigma_eq_equiv
|
||||
... ≃ (pType.carrier (S (pred n)) = pType.carrier (S (pred n))) : sigma_equiv_of_is_contr_right
|
||||
... ≃ (S (pred n) ≃ S (pred n)) : eq_equiv_equiv
|
||||
|
||||
definition mirror (n : ℕ) : S n..-1 → G n :=
|
||||
definition mirror (n : ℕ) [is_succ n] : S (pred n) → G n :=
|
||||
begin
|
||||
intro v, apply to_inv (G_char n),
|
||||
exact sorry
|
||||
|
|
@ -35,35 +35,38 @@ namespace spherical_fibrations
|
|||
|
||||
Yes, let eval : BG (n+1) → S n be the evaluation map
|
||||
-/
|
||||
definition is_succ_1 [instance] : is_succ 1 := is_succ.mk 0
|
||||
|
||||
definition S_of_BG (n : ℕ) : Ω(pBG (n+1)) → S n :=
|
||||
λ f, f..1 ▸ base
|
||||
λ f, f..1 ▸ pt
|
||||
|
||||
definition BG_succ (n : ℕ) : BG n → BG (n+1) :=
|
||||
definition BG_succ (n : ℕ) [H : is_succ n] : BG n → BG (n+1) :=
|
||||
begin
|
||||
induction H with n,
|
||||
intro X, cases X with X p,
|
||||
apply sigma.mk (susp X), induction p with f, apply tr,
|
||||
apply susp.equiv f
|
||||
refine sigma.mk (susp X) _, induction p with f, apply tr,
|
||||
exact susp.equiv f
|
||||
end
|
||||
|
||||
/- classifying type of pointed spherical fibrations -/
|
||||
definition BF (n : ℕ) : Type₁ :=
|
||||
Σ(X : Type*), ∥ X ≃* S* n ∥
|
||||
Σ(X : Type*), ∥ X ≃* S n ∥
|
||||
|
||||
definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) :=
|
||||
pointed.mk ⟨ S* n , tr pequiv.rfl ⟩
|
||||
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_pequiv f
|
||||
apply sigma.mk (susp X), induction p with f, apply tr,
|
||||
apply susp.susp_pequiv f
|
||||
end
|
||||
|
||||
definition BF_of_BG {n : ℕ} : BG n → BF n :=
|
||||
definition BF_of_BG {n : ℕ} [H : is_succ n] : BG n → BF n :=
|
||||
begin
|
||||
induction H with n,
|
||||
intro X, cases X with X p,
|
||||
apply sigma.mk (pointed.MK (susp X) susp.north),
|
||||
induction p with f, apply tr,
|
||||
|
|
@ -78,13 +81,15 @@ namespace spherical_fibrations
|
|||
apply tr, exact fX
|
||||
end
|
||||
|
||||
definition BG_mul {n m : ℕ} (X : BG n) (Y : BG m) : BG (n + m) :=
|
||||
definition BG_mul {n m : ℕ} [Hn : is_succ n] [Hm : is_succ m] (X : BG n) (Y : BG m) :
|
||||
BG (n + m) :=
|
||||
begin
|
||||
induction Hn with n, induction Hm with m,
|
||||
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)
|
||||
apply tr, rewrite [succ_add],
|
||||
exact join_equiv_join fX fY ⬝e join_sphere n m
|
||||
end
|
||||
|
||||
definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) :=
|
||||
|
|
@ -95,7 +100,7 @@ namespace spherical_fibrations
|
|||
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)
|
||||
definition BF_of_BG_mul (n m : ℕ) [is_succ n] [is_succ 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
|
||||
|
||||
|
|
|
|||
|
|
@ -5,13 +5,8 @@ open susp eq pointed function is_equiv lift equiv is_trunc nat
|
|||
namespace susp
|
||||
variables {X X' Y Y' Z : Type*}
|
||||
|
||||
/- TODO: remove susp and rename psusp to susp -/
|
||||
definition psuspn : ℕ → Type* → Type*
|
||||
| psuspn 0 X := X
|
||||
| psuspn (succ n) X := psusp (psuspn n X)
|
||||
|
||||
definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) :
|
||||
psusp_functor (pconst X Y) x = pt :=
|
||||
definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : susp X) :
|
||||
susp_functor (pconst X Y) x = pt :=
|
||||
begin
|
||||
induction x,
|
||||
{ reflexivity },
|
||||
|
|
@ -19,81 +14,81 @@ namespace susp
|
|||
{ apply eq_pathover, refine !elim_merid ⬝ph _ ⬝hp !ap_constant⁻¹, exact square_of_eq !con.right_inv⁻¹ }
|
||||
end
|
||||
|
||||
definition susp_functor_pconst [constructor] (X Y : Type*) : psusp_functor (pconst X Y) ~* pconst (psusp X) (psusp Y) :=
|
||||
definition susp_functor_pconst [constructor] (X Y : Type*) : susp_functor (pconst X Y) ~* pconst (susp X) (susp Y) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ exact susp_functor_pconst_homotopy },
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
definition psusp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (psusp X) (psusp Y) :=
|
||||
pmap.mk psusp_functor (eq_of_phomotopy !susp_functor_pconst)
|
||||
definition susp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (susp X) (susp Y) :=
|
||||
pmap.mk susp_functor (eq_of_phomotopy !susp_functor_pconst)
|
||||
|
||||
definition psusp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (psusp X) Y :=
|
||||
ppcompose_left (loop_psusp_counit Y) ∘* psusp_pfunctor X (Ω Y)
|
||||
definition susp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (susp X) Y :=
|
||||
ppcompose_left (loop_susp_counit Y) ∘* susp_pfunctor X (Ω Y)
|
||||
|
||||
definition loop_psusp_pintro [constructor] (X Y : Type*) : ppmap (psusp X) Y →* ppmap X (Ω Y) :=
|
||||
ppcompose_right (loop_psusp_unit X) ∘* pap1 (psusp X) Y
|
||||
definition loop_susp_pintro [constructor] (X Y : Type*) : ppmap (susp X) Y →* ppmap X (Ω Y) :=
|
||||
ppcompose_right (loop_susp_unit X) ∘* pap1 (susp X) Y
|
||||
|
||||
definition loop_psusp_pintro_natural_left (f : X' →* X) :
|
||||
psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X' Y)
|
||||
(ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
|
||||
!pap1_natural_left ⬝h* ppcompose_right_psquare (loop_psusp_unit_natural f)⁻¹*
|
||||
definition loop_susp_pintro_natural_left (f : X' →* X) :
|
||||
psquare (loop_susp_pintro X Y) (loop_susp_pintro X' Y)
|
||||
(ppcompose_right (susp_functor f)) (ppcompose_right f) :=
|
||||
!pap1_natural_left ⬝h* ppcompose_right_psquare (loop_susp_unit_natural f)⁻¹*
|
||||
|
||||
definition loop_psusp_pintro_natural_right (f : Y →* Y') :
|
||||
psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X Y')
|
||||
definition loop_susp_pintro_natural_right (f : Y →* Y') :
|
||||
psquare (loop_susp_pintro X Y) (loop_susp_pintro X Y')
|
||||
(ppcompose_left f) (ppcompose_left (Ω→ f)) :=
|
||||
!pap1_natural_right ⬝h* !ppcompose_left_ppcompose_right⁻¹*
|
||||
|
||||
definition is_equiv_loop_psusp_pintro [constructor] (X Y : Type*) :
|
||||
is_equiv (loop_psusp_pintro X Y) :=
|
||||
definition is_equiv_loop_susp_pintro [constructor] (X Y : Type*) :
|
||||
is_equiv (loop_susp_pintro X Y) :=
|
||||
begin
|
||||
fapply adjointify,
|
||||
{ exact psusp_pelim X Y },
|
||||
{ intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g },
|
||||
{ intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f }
|
||||
{ exact susp_pelim X Y },
|
||||
{ intro g, apply eq_of_phomotopy, exact susp_adjoint_loop_right_inv g },
|
||||
{ intro f, apply eq_of_phomotopy, exact susp_adjoint_loop_left_inv f }
|
||||
end
|
||||
|
||||
definition psusp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) :=
|
||||
pequiv_of_pmap (loop_psusp_pintro X Y) (is_equiv_loop_psusp_pintro X Y)
|
||||
definition susp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (susp X) Y ≃* ppmap X (Ω Y) :=
|
||||
pequiv_of_pmap (loop_susp_pintro X Y) (is_equiv_loop_susp_pintro X Y)
|
||||
|
||||
definition psusp_adjoint_loop_natural_right (f : Y →* Y') :
|
||||
psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X Y')
|
||||
definition susp_adjoint_loop_natural_right (f : Y →* Y') :
|
||||
psquare (susp_adjoint_loop' X Y) (susp_adjoint_loop' X Y')
|
||||
(ppcompose_left f) (ppcompose_left (Ω→ f)) :=
|
||||
loop_psusp_pintro_natural_right f
|
||||
loop_susp_pintro_natural_right f
|
||||
|
||||
definition psusp_adjoint_loop_natural_left (f : X' →* X) :
|
||||
psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X' Y)
|
||||
(ppcompose_right (psusp_functor f)) (ppcompose_right f) :=
|
||||
loop_psusp_pintro_natural_left f
|
||||
definition susp_adjoint_loop_natural_left (f : X' →* X) :
|
||||
psquare (susp_adjoint_loop' X Y) (susp_adjoint_loop' X' Y)
|
||||
(ppcompose_right (susp_functor f)) (ppcompose_right f) :=
|
||||
loop_susp_pintro_natural_left f
|
||||
|
||||
definition iterate_psusp_iterate_psusp_rev (n m : ℕ) (A : Type*) :
|
||||
iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (m + n) A :=
|
||||
definition iterate_susp_iterate_susp_rev (n m : ℕ) (A : Type*) :
|
||||
iterate_susp n (iterate_susp m A) ≃* iterate_susp (m + n) A :=
|
||||
begin
|
||||
induction n with n e,
|
||||
{ reflexivity },
|
||||
{ exact psusp_pequiv e }
|
||||
{ exact susp_pequiv e }
|
||||
end
|
||||
|
||||
definition iterate_psusp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) :
|
||||
iterate_psusp n X ≃* iterate_psusp n Y :=
|
||||
definition iterate_susp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) :
|
||||
iterate_susp n X ≃* iterate_susp n Y :=
|
||||
begin
|
||||
induction n with n e,
|
||||
{ exact f },
|
||||
{ exact psusp_pequiv e }
|
||||
{ exact susp_pequiv e }
|
||||
end
|
||||
|
||||
open algebra nat
|
||||
definition iterate_psusp_iterate_psusp (n m : ℕ) (A : Type*) :
|
||||
iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (n + m) A :=
|
||||
iterate_psusp_iterate_psusp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_psusp k A) (add.comm m n))
|
||||
definition iterate_susp_iterate_susp (n m : ℕ) (A : Type*) :
|
||||
iterate_susp n (iterate_susp m A) ≃* iterate_susp (n + m) A :=
|
||||
iterate_susp_iterate_susp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_susp k A) (add.comm m n))
|
||||
|
||||
definition plift_psusp.{u v} : Π(A : Type*), plift.{u v} (psusp A) ≃* psusp (plift.{u v} A) :=
|
||||
definition plift_susp.{u v} : Π(A : Type*), plift.{u v} (susp A) ≃* susp (plift.{u v} A) :=
|
||||
begin
|
||||
intro A,
|
||||
calc
|
||||
plift.{u v} (psusp A) ≃* psusp A : by exact (pequiv_plift (psusp A))⁻¹ᵉ*
|
||||
... ≃* psusp (plift.{u v} A) : by exact psusp_pequiv (pequiv_plift.{u v} A)
|
||||
plift.{u v} (susp A) ≃* susp A : by exact (pequiv_plift (susp A))⁻¹ᵉ*
|
||||
... ≃* susp (plift.{u v} A) : by exact susp_pequiv (pequiv_plift.{u v} A)
|
||||
end
|
||||
|
||||
definition is_contr_susp [instance] (A : Type) [H : is_contr A] : is_contr (susp A) :=
|
||||
|
|
@ -106,32 +101,30 @@ namespace susp
|
|||
exact whisker_left idp (ap merid !eq_of_is_contr)
|
||||
end
|
||||
|
||||
definition is_contr_psusp [instance] (A : Type) [H : is_contr A] : is_contr (psusp A) :=
|
||||
is_contr_susp A
|
||||
|
||||
definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
|
||||
pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
|
||||
definition loop_susp_pintro_phomotopy {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) :
|
||||
loop_susp_pintro X Y f ~* loop_susp_pintro X Y g :=
|
||||
pwhisker_right (loop_susp_unit X) (Ω⇒ p)
|
||||
|
||||
variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
|
||||
{f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
|
||||
{f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
|
||||
|
||||
-- rename: psusp_functor_psquare
|
||||
-- rename: susp_functor_psquare
|
||||
definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
|
||||
sorry
|
||||
|
||||
definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
|
||||
definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : susp A₀₀ →* A₀₂) (f₂₁ : susp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_susp_pintro A₀₀ A₀₂) f₀₁) ((loop_susp_pintro A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat _ (ap1_psquare p),
|
||||
exact loop_psusp_unit_natural f₁₀
|
||||
exact loop_susp_unit_natural f₁₀
|
||||
end
|
||||
|
||||
definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
|
||||
definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((susp_pelim A₀₀ A₀₂) f₀₁) ((susp_pelim A₂₀ A₂₂) f₂₁)) :=
|
||||
begin
|
||||
intro p,
|
||||
refine pvconcat (suspend_psquare p) _,
|
||||
exact psquare_transpose (loop_psusp_counit_natural f₁₂)
|
||||
exact psquare_transpose (loop_susp_counit_natural f₁₂)
|
||||
end
|
||||
|
||||
end susp
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ open wedge pushout eq prod sum pointed equiv is_equiv unit lift
|
|||
|
||||
namespace wedge
|
||||
|
||||
definition wedge_flip [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A :=
|
||||
definition wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact inr a },
|
||||
|
|
@ -15,26 +15,29 @@ namespace wedge
|
|||
end
|
||||
|
||||
-- TODO: fix precedences
|
||||
definition pwedge_flip [constructor] (A B : Type*) : (A ∨ B) →* (B ∨ A) :=
|
||||
pmap.mk wedge_flip (glue ⋆)⁻¹
|
||||
definition wedge_flip [constructor] (A B : Type*) : A ∨ B →* B ∨ A :=
|
||||
pmap.mk wedge_flip' (glue ⋆)⁻¹
|
||||
|
||||
definition wedge_flip_wedge_flip {A B : Type*} (x : A ∨ B) : wedge_flip (wedge_flip x) = x :=
|
||||
definition wedge_flip'_wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : wedge_flip' (wedge_flip' x) = x :=
|
||||
begin
|
||||
induction x,
|
||||
{ reflexivity },
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover_id_right,
|
||||
apply hdeg_square,
|
||||
exact ap_compose wedge_flip _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv }
|
||||
exact ap_compose wedge_flip' _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv }
|
||||
end
|
||||
|
||||
definition pwedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A :=
|
||||
definition wedge_flip_wedge_flip (A B : Type*) : wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) :=
|
||||
phomotopy.mk wedge_flip'_wedge_flip' (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹
|
||||
|
||||
definition wedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A :=
|
||||
begin
|
||||
fapply pequiv.MK',
|
||||
{ exact pwedge_flip A B },
|
||||
{ exact wedge_flip },
|
||||
{ exact wedge_flip_wedge_flip },
|
||||
{ exact wedge_flip_wedge_flip }
|
||||
fapply pequiv.MK,
|
||||
{ exact wedge_flip A B },
|
||||
{ exact wedge_flip B A },
|
||||
{ exact wedge_flip_wedge_flip A B },
|
||||
{ exact wedge_flip_wedge_flip B A }
|
||||
end
|
||||
|
||||
-- TODO: wedge is associative
|
||||
|
|
@ -53,15 +56,15 @@ namespace wedge
|
|||
end
|
||||
|
||||
|
||||
definition pwedge_pequiv [constructor] {A A' B B' : Type*} (a : A ≃* A') (b : B ≃* B') : A ∨ B ≃* A' ∨ B' :=
|
||||
definition wedge_pequiv [constructor] {A A' B B' : Type*} (a : A ≃* A') (b : B ≃* B') : A ∨ B ≃* A' ∨ B' :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
exact pushout.equiv !pconst !pconst !pconst !pconst !pequiv.refl a b (λdummy, respect_pt a) (λdummy, respect_pt b),
|
||||
exact ap pushout.inl (respect_pt a)
|
||||
end
|
||||
|
||||
definition plift_pwedge.{u v} (A B : Type*) : plift.{u v} (A ∨ B) ≃* plift.{u v} A ∨ plift.{u v} B :=
|
||||
definition plift_wedge.{u v} (A B : Type*) : plift.{u v} (A ∨ B) ≃* plift.{u v} A ∨ plift.{u v} B :=
|
||||
calc plift.{u v} (A ∨ B) ≃* A ∨ B : by exact !pequiv_plift⁻¹ᵉ*
|
||||
... ≃* plift.{u v} A ∨ plift.{u v} B : by exact pwedge_pequiv !pequiv_plift !pequiv_plift
|
||||
... ≃* plift.{u v} A ∨ plift.{u v} B : by exact wedge_pequiv !pequiv_plift !pequiv_plift
|
||||
|
||||
end wedge
|
||||
|
|
|
|||
|
|
@ -174,6 +174,10 @@ namespace eq
|
|||
phomotopy_rec_on_idp phomotopy.rfl H = H :=
|
||||
!phomotopy_rec_on_eq_phomotopy_of_eq
|
||||
|
||||
definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type}
|
||||
{a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) :
|
||||
eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp :=
|
||||
by induction q; reflexivity
|
||||
|
||||
end eq open eq
|
||||
|
||||
|
|
@ -477,6 +481,11 @@ namespace is_trunc
|
|||
|
||||
end is_trunc
|
||||
namespace sigma
|
||||
open sigma.ops
|
||||
|
||||
definition sigma_eq_equiv_of_is_prop_right [constructor] {A : Type} {B : A → Type} (u v : Σa, B a)
|
||||
[H : Π a, is_prop (B a)] : u = v ≃ u.1 = v.1 :=
|
||||
!sigma_eq_equiv ⬝e !sigma_equiv_of_is_contr_right
|
||||
|
||||
definition ap_sigma_pr1 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a))
|
||||
(p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..1 = ap f p :=
|
||||
|
|
@ -903,13 +912,13 @@ end category
|
|||
|
||||
namespace sphere
|
||||
|
||||
-- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
|
||||
-- f ~* pconst (S* n) (S* m) :=
|
||||
-- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S n →* S m) :
|
||||
-- f ~* pconst (S n) (S m) :=
|
||||
-- begin
|
||||
-- assert H : is_contr (Ω[n] (S* m)),
|
||||
-- assert H : is_contr (Ω[n] (S m)),
|
||||
-- { apply homotopy_group_sphere_le, },
|
||||
-- apply phomotopy_of_eq,
|
||||
-- apply eq_of_fn_eq_fn !psphere_pmap_pequiv,
|
||||
-- apply eq_of_fn_eq_fn !sphere_pmap_pequiv,
|
||||
-- apply @is_prop.elim
|
||||
-- end
|
||||
|
||||
|
|
@ -948,8 +957,8 @@ end injective_surjective
|
|||
|
||||
-- Yuri Sulyma's code from HoTT MRC
|
||||
|
||||
notation `⅀→`:(max+5) := psusp_functor
|
||||
notation `⅀⇒`:(max+5) := psusp_functor_phomotopy
|
||||
notation `⅀→`:(max+5) := susp_functor
|
||||
notation `⅀⇒`:(max+5) := susp_functor_phomotopy
|
||||
notation `Ω⇒`:(max+5) := ap1_phomotopy
|
||||
|
||||
definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) :=
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ namespace pointed
|
|||
pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
|
||||
ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
|
||||
|
||||
/- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/
|
||||
definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
|
||||
(loop_ppmap_commute X Y)⁻¹ᵉ*
|
||||
|
||||
|
|
|
|||
|
|
@ -1014,6 +1014,8 @@ namespace pointed
|
|||
ppmap A₊ B ≃* A →ᵘ* B :=
|
||||
pequiv_of_equiv (pmap_equiv_left A B) idp
|
||||
|
||||
/- There are some lemma's needed to prove the naturality of the equivalence
|
||||
Ω (Π*a, B a) ≃* Π*(a : A), Ω (B a) -/
|
||||
definition ppi_eq_equiv_natural_gen_lem {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
|
||||
{f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k : ppi_gen B b₀} {k' : ppi_gen C c₀}
|
||||
(p : pmap_compose_ppi_gen f f₀ k ~~* k') :
|
||||
|
|
@ -1086,6 +1088,7 @@ namespace pointed
|
|||
{ exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !ppi_eq_refl) }
|
||||
end
|
||||
|
||||
|
||||
/- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural,
|
||||
where we define loop_pppi_pequiv as composite of pointed equivalences, and proved the
|
||||
naturality individually. That turned out to be harder.
|
||||
|
|
|
|||
|
|
@ -779,7 +779,7 @@ namespace spectrum
|
|||
|
||||
-- Suspension prespectra are one that's naturally indexed on the natural numbers
|
||||
definition psp_susp (X : Type*) : gen_prespectrum +ℕ :=
|
||||
gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X))
|
||||
gen_prespectrum.mk (λn, iterate_susp n X) (λn, loop_susp_unit (iterate_susp n X))
|
||||
|
||||
-- The sphere prespectrum
|
||||
definition psp_sphere : gen_prespectrum +ℕ :=
|
||||
|
|
|
|||
|
|
@ -7,10 +7,10 @@ namespace spectrum
|
|||
|
||||
definition smash_prespectrum (X : Type*) (Y : prespectrum) : prespectrum :=
|
||||
prespectrum.mk (λ z, X ∧ Y z) begin
|
||||
intro n, refine loop_psusp_pintro (X ∧ Y n) (X ∧ Y (n + 1)) _,
|
||||
refine _ ∘* (smash_psusp X (Y n))⁻¹ᵉ*,
|
||||
intro n, refine loop_susp_pintro (X ∧ Y n) (X ∧ Y (n + 1)) _,
|
||||
refine _ ∘* (smash_susp X (Y n))⁻¹ᵉ*,
|
||||
refine smash_functor !pid _,
|
||||
refine psusp_pelim (Y n) (Y (n + 1)) _,
|
||||
refine susp_pelim (Y n) (Y (n + 1)) _,
|
||||
exact !glue
|
||||
end
|
||||
|
||||
|
|
@ -18,11 +18,11 @@ definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →*
|
|||
smap.mk (λn, smash_functor f (g n)) begin
|
||||
intro n,
|
||||
refine susp_to_loop_psquare _ _ _ _ _,
|
||||
refine pvconcat (psquare_transpose (phinverse (smash_psusp_natural f (g n)))) _,
|
||||
refine pvconcat (psquare_transpose (phinverse (smash_susp_natural f (g n)))) _,
|
||||
refine vconcat_phomotopy _ (smash_functor_split f (g (S n))),
|
||||
refine phomotopy_vconcat (smash_functor_split f (psusp_functor (g n))) _,
|
||||
refine phomotopy_vconcat (smash_functor_split f (susp_functor (g n))) _,
|
||||
refine phconcat _ _,
|
||||
let glue_adjoint := psusp_pelim (Y n) (Y (S n)) (glue Y n),
|
||||
let glue_adjoint := susp_pelim (Y n) (Y (S n)) (glue Y n),
|
||||
exact pid X' ∧→ glue_adjoint,
|
||||
exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint),
|
||||
refine smash_functor_psquare (phrefl (pid X')) _,
|
||||
|
|
|
|||
Loading…
Reference in a new issue