Remove some old files
This commit is contained in:
Floris van Doorn
parent
47532e4315
commit
b9ed007161
7 changed files with 192 additions and 409 deletions
|
|
@ -1,7 +1,7 @@
|
|||
-- Authors: Floris van Doorn
|
||||
-- In collaboration with Stefano, Robin
|
||||
|
||||
import .smash
|
||||
import ..homotopy.smash
|
||||
|
||||
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
|
||||
function red_susp unit sigma
|
||||
190
archive/smash_old.hlean
Normal file
190
archive/smash_old.hlean
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
/- below are some old tries to compute (A ∧ S¹) directly -/
|
||||
|
||||
exit
|
||||
|
||||
/- smash A S¹ = red_susp A -/
|
||||
|
||||
definition red_susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : red_susp A :=
|
||||
begin
|
||||
induction x using smash.elim,
|
||||
{ induction b, exact base, exact equator a },
|
||||
{ exact base },
|
||||
{ exact base },
|
||||
{ reflexivity },
|
||||
{ exact circle_elim_constant equator_pt b }
|
||||
end
|
||||
|
||||
definition smash_pcircle_of_red_susp [unfold 2] (x : red_susp A) : smash A S¹* :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact pt },
|
||||
{ exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
|
||||
{ refine !con.right_inv ◾ _ ◾ !con.right_inv,
|
||||
exact ap_is_constant gluer loop ⬝ !con.right_inv }
|
||||
end
|
||||
|
||||
definition smash_pcircle_of_red_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
|
||||
smash_pcircle_of_red_susp (red_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_red_susp _ _ ⬝ph _,
|
||||
refine ap02 _ (elim_loop pt (equator a)) ⬝ !elim_equator ⬝ph _,
|
||||
-- make everything below this a lemma defined by path induction?
|
||||
refine !con_idp⁻¹ ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb,
|
||||
apply whisker_tl, apply hrfl end end }
|
||||
end
|
||||
|
||||
definition concat2o [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
|
||||
{p : a = a'} (s : q a =[p] q a') (t : r a =[p] r a') : q a ⬝ r a =[p] q a' ⬝ r a' :=
|
||||
by induction p; exact idpo
|
||||
|
||||
definition apd_con_fn [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
|
||||
(p : a = a') : apd (λa, q a ⬝ r a) p = concat2o (apd q p) (apd r p) :=
|
||||
by induction p; reflexivity
|
||||
|
||||
-- definition apd_con_fn_constant [unfold 10] {A B : Type} {f : A → B} {b b' : B} {q : Πa, f a = b}
|
||||
-- {r : b = b'} {a a' : A} (p : a = a') :
|
||||
-- apd (λa, q a ⬝ r) p = concat2o (apd q p) (pathover_of_eq _ idp) :=
|
||||
-- by induction p; reflexivity
|
||||
|
||||
|
||||
definition smash_pcircle_pequiv_red [constructor] (A : Type*) : smash A S¹* ≃* red_susp A :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ fapply equiv.MK,
|
||||
{ exact red_susp_of_smash_pcircle },
|
||||
{ exact smash_pcircle_of_red_susp },
|
||||
{ exact abstract begin intro x, induction x,
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover, apply hdeg_square,
|
||||
refine ap_compose red_susp_of_smash_pcircle _ _ ⬝ ap02 _ !elim_equator ⬝ _ ⬝ !ap_id⁻¹,
|
||||
refine !ap_con ⬝ (!ap_con ⬝ !elim_gluel' ◾ !ap_compose'⁻¹) ◾ !elim_gluel' ⬝ _,
|
||||
esimp, exact !idp_con ⬝ !elim_loop },
|
||||
{ exact sorry } end end },
|
||||
{ intro x, induction x,
|
||||
{ exact smash_pcircle_of_red_susp_of_smash_pcircle_pt a b },
|
||||
{ exact gluel pt },
|
||||
{ exact gluer pt },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
|
||||
unfold [red_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_red_susp _ _ ⬝ph _,
|
||||
unfold [red_susp_of_smash_pcircle],
|
||||
-- not sure why so many implicit arguments are needed here...
|
||||
refine ap02 _ (@smash.elim_gluer A S¹* _ (λa, circle.elim red_susp.base (equator a)) red_susp.base red_susp.base (λa, refl red_susp.base) (circle_elim_constant equator_pt) b) ⬝ph _,
|
||||
apply square_of_eq, induction b,
|
||||
{ exact whisker_right _ !con.right_inv },
|
||||
{ apply eq_pathover_dep, refine !apd_con_fn ⬝pho _ ⬝hop !apd_con_fn⁻¹,
|
||||
refine ap (λx, concat2o x _) !rec_loop ⬝pho _ ⬝hop (ap011 concat2o (apd_compose1 (λa b, ap smash_pcircle_of_red_susp b) (circle_elim_constant equator_pt) loop) !apd_constant')⁻¹,
|
||||
exact sorry }
|
||||
|
||||
}}},
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
/- smash A S¹ = susp A -/
|
||||
open susp
|
||||
|
||||
|
||||
definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A :=
|
||||
begin
|
||||
induction x using smash.elim,
|
||||
{ induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ },
|
||||
{ exact pt },
|
||||
{ exact pt },
|
||||
{ reflexivity },
|
||||
{ induction b, reflexivity, apply eq_pathover_constant_right, apply hdeg_square,
|
||||
exact !elim_loop ⬝ !con.right_inv }
|
||||
end
|
||||
|
||||
definition smash_pcircle_of_psusp [unfold 2] (x : psusp A) : smash A S¹* :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact pt },
|
||||
{ exact pt },
|
||||
{ exact gluel' pt a ⬝ (ap (smash.mk a) loop ⬝ gluel' a pt) },
|
||||
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 :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact gluel' pt a },
|
||||
{ exact abstract begin apply eq_pathover,
|
||||
refine ap_compose smash_pcircle_of_psusp _ _ ⬝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?
|
||||
exact sorry,
|
||||
-- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, refine !con.assoc⁻¹ ⬝ph _,
|
||||
-- apply whisker_bl, apply whisker_lb,
|
||||
-- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl
|
||||
-- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl,
|
||||
-- refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl
|
||||
-- apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
|
||||
-- symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
|
||||
-- refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,
|
||||
-- refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹,
|
||||
-- refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv,
|
||||
-- refine !ap_mk_right ⬝ !con.right_inv
|
||||
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)
|
||||
-- (gluer pt)
|
||||
-- (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b)))
|
||||
-- (gluer b) :=
|
||||
-- begin
|
||||
-- refine ap02 _ !elim_gluer ⬝ph _,
|
||||
-- induction b,
|
||||
-- { apply square_of_eq, exact whisker_right _ !con.right_inv },
|
||||
-- { apply square_pathover', exact sorry }
|
||||
-- end
|
||||
|
||||
exit
|
||||
definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A :=
|
||||
begin
|
||||
fapply pequiv_of_equiv,
|
||||
{ fapply equiv.MK,
|
||||
{ exact psusp_of_smash_pcircle },
|
||||
{ exact smash_pcircle_of_psusp },
|
||||
{ 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 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),
|
||||
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 gluel pt },
|
||||
{ exact gluer pt },
|
||||
{ apply eq_pathover_id_right,
|
||||
refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
|
||||
unfold [psusp_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 ap02 _ !elim_gluer ⬝ph _,
|
||||
induction b,
|
||||
{ apply square_of_eq, exact whisker_right _ !con.right_inv },
|
||||
{ exact sorry}
|
||||
}}},
|
||||
{ reflexivity }
|
||||
end
|
||||
|
||||
end smash
|
||||
|
|
@ -1,194 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Ulrik Buchholtz
|
||||
-/
|
||||
import types.trunc types.arrow_2 types.fiber homotopy.susp
|
||||
|
||||
open eq is_trunc is_equiv nat equiv trunc function fiber
|
||||
|
||||
namespace homotopy
|
||||
|
||||
definition is_conn [reducible] (n : trunc_index) (A : Type) : Type :=
|
||||
is_contr (trunc n A)
|
||||
|
||||
definition is_conn_equiv_closed (n : trunc_index) {A B : Type}
|
||||
: A ≃ B → is_conn n A → is_conn n B :=
|
||||
begin
|
||||
intros H C,
|
||||
fapply @is_contr_equiv_closed (trunc n A) _,
|
||||
apply trunc_equiv_trunc,
|
||||
assumption
|
||||
end
|
||||
|
||||
definition is_conn_fun (n : trunc_index) {A B : Type} (f : A → B) : Type :=
|
||||
Πb : B, is_conn n (fiber f b)
|
||||
|
||||
namespace is_conn_fun
|
||||
section
|
||||
parameters {n : trunc_index} {A B : Type} {h : A → B}
|
||||
(H : is_conn_fun n h) (P : B → n -Type)
|
||||
|
||||
private definition helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b :=
|
||||
λt b, trunc.rec (λx, point_eq x ▸ t (point x))
|
||||
|
||||
private definition g : (Πa : A, P (h a)) → (Πb : B, P b) :=
|
||||
λt b, helper t b (@center (trunc n (fiber h b)) (H b))
|
||||
|
||||
-- induction principle for n-connected maps (Lemma 7.5.7)
|
||||
definition rec : is_equiv (λs : Πb : B, P b, λa : A, s (h a)) :=
|
||||
adjointify (λs a, s (h a)) g
|
||||
begin
|
||||
intro t, apply eq_of_homotopy, intro a, unfold g, unfold helper,
|
||||
rewrite [@center_eq _ (H (h a)) (tr (fiber.mk a idp))],
|
||||
end
|
||||
begin
|
||||
intro k, apply eq_of_homotopy, intro b, unfold g,
|
||||
generalize (@center _ (H b)), apply trunc.rec, apply fiber.rec,
|
||||
intros a p, induction p, reflexivity
|
||||
end
|
||||
|
||||
definition elim : (Πa : A, P (h a)) → (Πb : B, P b) :=
|
||||
@is_equiv.inv _ _ (λs a, s (h a)) rec
|
||||
|
||||
definition elim_β : Πf : (Πa : A, P (h a)), Πa : A, elim f (h a) = f a :=
|
||||
λf, apd10 (@is_equiv.right_inv _ _ (λs a, s (h a)) rec f)
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
universe variables u v
|
||||
parameters {n : trunc_index} {A : Type.{u}} {B : Type.{v}} {h : A → B}
|
||||
parameter sec : ΠP : B → trunctype.{max u v} n,
|
||||
is_retraction (λs : (Πb : B, P b), λ a, s (h a))
|
||||
|
||||
private definition s := sec (λb, trunctype.mk' n (trunc n (fiber h b)))
|
||||
|
||||
include sec
|
||||
|
||||
-- the other half of Lemma 7.5.7
|
||||
definition intro : is_conn_fun n h :=
|
||||
begin
|
||||
intro b,
|
||||
apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b),
|
||||
esimp, apply trunc.rec, apply fiber.rec, intros a p,
|
||||
apply transport
|
||||
(λz : (Σy, h a = y), @sect _ _ _ s (λa, tr (mk a idp)) (sigma.pr1 z) =
|
||||
tr (fiber.mk a (sigma.pr2 z)))
|
||||
(@center_eq _ (is_contr_sigma_eq (h a)) (sigma.mk b p)),
|
||||
exact apd10 (@right_inverse _ _ _ s (λa, tr (fiber.mk a idp))) a
|
||||
end
|
||||
end
|
||||
end is_conn_fun
|
||||
|
||||
-- Connectedness is related to maps to and from the unit type, first to
|
||||
section
|
||||
parameters (n : trunc_index) (A : Type)
|
||||
|
||||
definition is_conn_of_map_to_unit
|
||||
: is_conn_fun n (λx : A, unit.star) → is_conn n A :=
|
||||
begin
|
||||
intro H, unfold is_conn_fun at H,
|
||||
rewrite [-(ua (fiber.fiber_star_equiv A))],
|
||||
exact (H unit.star)
|
||||
end
|
||||
|
||||
-- now maps from unit
|
||||
definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_fun n (const unit a₀))
|
||||
: is_conn n .+1 A :=
|
||||
is_contr.mk (tr a₀)
|
||||
begin
|
||||
apply trunc.rec, intro a,
|
||||
exact trunc.elim (λz : fiber (const unit a₀) a, ap tr (point_eq z))
|
||||
(@center _ (H a))
|
||||
end
|
||||
|
||||
definition is_conn_fun_from_unit (a₀ : A) [H : is_conn n .+1 A]
|
||||
: is_conn_fun n (const unit a₀) :=
|
||||
begin
|
||||
intro a,
|
||||
apply is_conn_equiv_closed n (equiv.symm (fiber_const_equiv A a₀ a)),
|
||||
apply @is_contr_equiv_closed _ _ (tr_eq_tr_equiv n a₀ a),
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
-- Lemma 7.5.2
|
||||
definition minus_one_conn_of_surjective {A B : Type} (f : A → B)
|
||||
: is_surjective f → is_conn_fun -1 f :=
|
||||
begin
|
||||
intro H, intro b,
|
||||
exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
|
||||
end
|
||||
|
||||
definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B)
|
||||
: is_conn_fun -1 f → is_surjective f :=
|
||||
begin
|
||||
intro H, intro b,
|
||||
exact @center (∥fiber f b∥) (H b),
|
||||
end
|
||||
|
||||
definition merely_of_minus_one_conn {A : Type} : is_conn -1 A → ∥A∥ :=
|
||||
λH, @center (∥A∥) H
|
||||
|
||||
definition minus_one_conn_of_merely {A : Type} : ∥A∥ → is_conn -1 A :=
|
||||
@is_contr_of_inhabited_prop (∥A∥) (is_trunc_trunc -1 A)
|
||||
|
||||
section
|
||||
open arrow
|
||||
|
||||
variables {f g : arrow}
|
||||
|
||||
-- Lemma 7.5.4
|
||||
definition retract_of_conn_is_conn [instance] (r : arrow_hom f g) [H : is_retraction r]
|
||||
(n : trunc_index) [K : is_conn_fun n f] : is_conn_fun n g :=
|
||||
begin
|
||||
intro b, unfold is_conn,
|
||||
apply is_contr_retract (trunc_functor n (retraction_on_fiber r b)),
|
||||
exact K (on_cod (arrow.is_retraction.sect r) b)
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
-- Corollary 7.5.5
|
||||
definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
|
||||
(p : f ~ g) (H : is_conn_fun n f) : is_conn_fun n g :=
|
||||
@retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
|
||||
|
||||
-- all types are -2-connected
|
||||
definition minus_two_conn [instance] (A : Type) : is_conn -2 A :=
|
||||
_
|
||||
|
||||
-- Theorem 8.2.1
|
||||
open susp
|
||||
|
||||
definition is_conn_susp [instance] (n : trunc_index) (A : Type)
|
||||
[H : is_conn n A] : is_conn (n .+1) (susp A) :=
|
||||
is_contr.mk (tr north)
|
||||
begin
|
||||
apply trunc.rec,
|
||||
fapply susp.rec,
|
||||
{ reflexivity },
|
||||
{ exact (trunc.rec (λa, ap tr (merid a)) (center (trunc n A))) },
|
||||
{ intro a,
|
||||
generalize (center (trunc n A)),
|
||||
apply trunc.rec,
|
||||
intro a',
|
||||
apply pathover_of_tr_eq,
|
||||
rewrite [eq_transport_Fr,idp_con],
|
||||
revert H, induction n with [n, IH],
|
||||
{ intro H, apply is_prop.elim },
|
||||
{ intros H,
|
||||
change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'),
|
||||
generalize a',
|
||||
apply is_conn_fun.elim
|
||||
(is_conn_fun_from_unit n A a)
|
||||
(λx : A, trunctype.mk' n (ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid x))),
|
||||
intros,
|
||||
change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a),
|
||||
reflexivity
|
||||
}
|
||||
}
|
||||
end
|
||||
|
||||
end homotopy
|
||||
|
|
@ -548,5 +548,4 @@ namespace smash
|
|||
rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
|
||||
end
|
||||
|
||||
|
||||
end smash
|
||||
|
|
|
|||
|
|
@ -1,123 +0,0 @@
|
|||
|
||||
import .smash_adjoint
|
||||
|
||||
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
|
||||
function red_susp unit smash
|
||||
|
||||
variables {A A' B B' C C' D E F X X' : Type*}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- definition concat2o {A B : Type} {f g h : A → B} {a₁ a₂ : A} {p₁ : f a₁ = g a₁} {p₂ : f a₂ = g a₂}
|
||||
-- {q₁ : g a₁ = h a₁} {q₂ : g a₂ = h a₂} {r : a₁ = a₂} (s₁ : p₁ =[r] p₂) (s₂ : q₁ =[r] q₂) :
|
||||
-- p₁ ⬝ q₁ =[r] p₂ ⬝ q₂ :=
|
||||
-- apo011 (λx, concat) s₁ s₂
|
||||
|
||||
-- infixl ` ◾o' `:75 := concat2o
|
||||
|
||||
-- definition apd_con_fn {A B : Type} {f g h : A → B} {a₁ a₂ : A} (p : f ~ g) (q : g ~ h) (r : a₁ = a₂)
|
||||
-- : apd (λa, p a ⬝ q a) r = apd p r ◾o' apd q r :=
|
||||
-- begin
|
||||
-- induction r, reflexivity
|
||||
-- end
|
||||
|
||||
-- definition ap02o {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) {a₁ a₂ : A} {p₁ : g a₁ = h a₁}
|
||||
-- {p₂ : g a₂ = h a₂} {q : a₁ = a₂} (r : p₁ =[q] p₂) : ap (f a₁) p₁ =[q] ap (f a₂) p₂ :=
|
||||
-- apo (λx, ap (f x)) r
|
||||
|
||||
-- definition apo_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
|
||||
-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
|
||||
-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
|
||||
-- apo h (eq_pathover s) = eq_pathover _ :=
|
||||
-- sorry
|
||||
|
||||
-- definition ap02o_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
|
||||
-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
|
||||
-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
|
||||
-- apo h (eq_pathover s) = eq_pathover _ :=
|
||||
-- sorry
|
||||
|
||||
-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
|
||||
-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=
|
||||
-- begin
|
||||
-- induction r; reflexivity
|
||||
-- end
|
||||
|
||||
-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
|
||||
-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=
|
||||
|
|
@ -1,80 +0,0 @@
|
|||
import homotopy.torus
|
||||
|
||||
open eq circle prod prod.ops function
|
||||
|
||||
namespace torus
|
||||
|
||||
definition S1xS1_of_torus [unfold 1] (x : T²) : S¹ × S¹ :=
|
||||
begin
|
||||
induction x,
|
||||
{ exact (circle.base, circle.base) },
|
||||
{ exact prod_eq loop idp },
|
||||
{ exact prod_eq idp loop },
|
||||
{ apply square_of_eq,
|
||||
exact !prod_eq_concat ⬝ ap011 prod_eq !idp_con⁻¹ !idp_con ⬝ !prod_eq_concat⁻¹ }
|
||||
end
|
||||
|
||||
definition torus_of_S1xS1 [unfold 1] (x : S¹ × S¹) : T² :=
|
||||
begin
|
||||
induction x with x y, induction x,
|
||||
{ induction y,
|
||||
{ exact base },
|
||||
{ exact loop2 }},
|
||||
{ induction y,
|
||||
{ exact loop1 },
|
||||
{ apply eq_pathover, refine !elim_loop ⬝ph surf ⬝hp !elim_loop⁻¹ }}
|
||||
end
|
||||
|
||||
definition to_from_base_left [unfold 1] (y : S¹) :
|
||||
S1xS1_of_torus (torus_of_S1xS1 (circle.base, y)) = (circle.base, y) :=
|
||||
begin
|
||||
induction y,
|
||||
{ reflexivity },
|
||||
{ apply eq_pathover, apply hdeg_square,
|
||||
refine ap_compose S1xS1_of_torus _ _ ⬝ ap02 _ !elim_loop ⬝ _ ⬝ !ap_prod_mk_right⁻¹,
|
||||
apply elim_loop2 }
|
||||
end
|
||||
|
||||
definition from_to_loop1
|
||||
: pathover (λa, torus_of_S1xS1 (S1xS1_of_torus a) = a) proof idp qed loop1 proof idp qed :=
|
||||
begin
|
||||
apply eq_pathover, apply hdeg_square,
|
||||
refine ap_compose torus_of_S1xS1 _ _ ⬝ ap02 _ !elim_loop1 ⬝ _ ⬝ !ap_id⁻¹,
|
||||
refine !ap_prod_elim ⬝ !idp_con ⬝ !elim_loop
|
||||
end
|
||||
|
||||
definition from_to_loop2
|
||||
: pathover (λa, torus_of_S1xS1 (S1xS1_of_torus a) = a) proof idp qed loop2 proof idp qed :=
|
||||
begin
|
||||
apply eq_pathover, apply hdeg_square,
|
||||
refine ap_compose torus_of_S1xS1 _ _ ⬝ ap02 _ !elim_loop2 ⬝ _ ⬝ !ap_id⁻¹,
|
||||
refine !ap_prod_elim ⬝ !elim_loop
|
||||
end
|
||||
|
||||
definition torus_equiv_S1xS1 : T² ≃ S¹ × S¹ :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ exact S1xS1_of_torus },
|
||||
{ exact torus_of_S1xS1 },
|
||||
{ intro x, induction x with x y, induction x,
|
||||
{ exact to_from_base_left y },
|
||||
{ apply eq_pathover,
|
||||
refine ap_compose (S1xS1_of_torus ∘ torus_of_S1xS1) _ _ ⬝ph _,
|
||||
refine ap02 _ !ap_prod_mk_left ⬝ph _ ⬝hp !ap_prod_mk_left⁻¹,
|
||||
refine !ap_compose ⬝ ap02 _ (!ap_prod_elim ⬝ !idp_con) ⬝ph _,
|
||||
refine ap02 _ !elim_loop ⬝ph _,
|
||||
induction y,
|
||||
{ apply hdeg_square, apply elim_loop1 },
|
||||
{ apply square_pathover, exact sorry }
|
||||
-- apply square_of_eq, induction y,
|
||||
-- { refine !idp_con ⬝ !elim_loop1⁻¹ },
|
||||
-- { apply eq_pathover_dep, }
|
||||
}},
|
||||
{ intro x, induction x,
|
||||
{ reflexivity },
|
||||
{ exact from_to_loop1 },
|
||||
{ exact from_to_loop2 },
|
||||
{ exact sorry }}
|
||||
end
|
||||
|
||||
end torus
|
||||
|
|
@ -5,14 +5,6 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge
|
|||
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
|
||||
is_trunc function sphere unit sum prod
|
||||
|
||||
attribute equiv_unit_of_is_contr [constructor]
|
||||
attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructor]
|
||||
attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor]
|
||||
attribute pushout.functor [unfold 16]
|
||||
attribute pushout.transpose [unfold 6]
|
||||
attribute ap_eq_apd10 [unfold 5]
|
||||
attribute eq_equiv_eq_symm [constructor]
|
||||
|
||||
definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
|
||||
!add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
|
||||
|
||||
|
|
@ -96,7 +88,6 @@ section -- squares
|
|||
|
||||
end
|
||||
|
||||
infix ` ⬝p2 `:75 := eq_concat2
|
||||
section -- cubes
|
||||
|
||||
variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A}
|
||||
|
|
@ -216,7 +207,7 @@ end
|
|||
definition id_compose {A B : Type} (f : A → B) : id ∘ f ~ f :=
|
||||
by reflexivity
|
||||
|
||||
-- move
|
||||
-- move to eq2
|
||||
definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X}
|
||||
(p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) :=
|
||||
by induction p; reflexivity
|
||||
|
|
|
|||
Loading…
Reference in a new issue