Finish proof of pfiber_equiv_of_square
This commit is contained in:
parent
22e75da53e
commit
f8f7f69bcd
1 changed files with 26 additions and 7 deletions
|
@ -5,13 +5,16 @@ Authors: Michael Shulman
|
||||||
|
|
||||||
-/
|
-/
|
||||||
|
|
||||||
import types.int types.pointed2 types.trunc homotopy.susp algebra.homotopy_group .chain_complex
|
import types.int types.pointed2 types.trunc homotopy.susp algebra.homotopy_group .chain_complex cubical
|
||||||
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index
|
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index
|
||||||
|
|
||||||
/-----------------------------------------
|
/-----------------------------------------
|
||||||
Stuff that should go in other files
|
Stuff that should go in other files
|
||||||
-----------------------------------------/
|
-----------------------------------------/
|
||||||
|
|
||||||
|
attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap [constructor]
|
||||||
|
attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
|
||||||
|
|
||||||
namespace sigma
|
namespace sigma
|
||||||
|
|
||||||
definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') :=
|
definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') :=
|
||||||
|
@ -20,6 +23,13 @@ namespace sigma
|
||||||
end sigma
|
end sigma
|
||||||
open sigma
|
open sigma
|
||||||
|
|
||||||
|
namespace eq
|
||||||
|
|
||||||
|
definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q :=
|
||||||
|
by induction p; induction q; exact idpo
|
||||||
|
|
||||||
|
end eq open eq
|
||||||
|
|
||||||
namespace pointed
|
namespace pointed
|
||||||
|
|
||||||
definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C :=
|
definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C :=
|
||||||
|
@ -119,7 +129,7 @@ namespace pointed
|
||||||
rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) }
|
rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) }
|
||||||
end
|
end
|
||||||
|
|
||||||
definition transport_fiber_equiv {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) : fiber f b1 ≃ fiber f b2 :=
|
definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) : fiber f b1 ≃ fiber f b2 :=
|
||||||
calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char
|
calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char
|
||||||
... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p)
|
... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p)
|
||||||
... ≃ fiber f b2 : fiber.sigma_char
|
... ≃ fiber f b2 : fiber.sigma_char
|
||||||
|
@ -128,15 +138,24 @@ namespace pointed
|
||||||
begin
|
begin
|
||||||
fapply pequiv_of_equiv, esimp,
|
fapply pequiv_of_equiv, esimp,
|
||||||
refine ((transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹) ⬝e (@fiber.equiv_postcompose A B f (Point B) B' g _)),
|
refine ((transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹) ⬝e (@fiber.equiv_postcompose A B f (Point B) B' g _)),
|
||||||
-- change (eq_equiv_fn_eq g _ _)⁻¹ ((ap g (respect_pt f) ⬝ respect_pt g) ⬝ (respect_pt g)⁻¹) = respect_pt f,
|
esimp, apply (ap (fiber.mk (Point A))), rewrite con.assoc, apply inv_con_eq_of_eq_con,
|
||||||
exact sorry
|
rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
|
||||||
end
|
end
|
||||||
|
|
||||||
|
definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f :=
|
||||||
|
begin
|
||||||
|
fapply pequiv_of_equiv, esimp,
|
||||||
|
refine (@fiber.equiv_precompose A B f (Point B) A' g _),
|
||||||
|
esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
|
||||||
|
{ apply respect_pt g },
|
||||||
|
{ apply pathover_eq_Fl' }
|
||||||
|
end
|
||||||
|
|
||||||
definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D} (s : k ∘* f ~* g ∘* h)
|
definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D} (s : k ∘* f ~* g ∘* h)
|
||||||
: pfiber f ≃* pfiber g :=
|
: pfiber f ≃* pfiber g :=
|
||||||
calc pfiber f ≃* pfiber (k ∘* f) : /- fiber.equiv_postcompose; need a pointed version (WIP above) -/ sorry
|
calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose
|
||||||
... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
|
... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
|
||||||
... ≃* pfiber g : /- fiber.equiv_precompose -/ sorry
|
... ≃* pfiber g : pequiv_precompose
|
||||||
|
|
||||||
end pointed
|
end pointed
|
||||||
open pointed
|
open pointed
|
||||||
|
|
Loading…
Add table
Reference in a new issue