52dd6cf90b
This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
99 lines
3.6 KiB
Text
99 lines
3.6 KiB
Text
/-
|
|
Copyright (c) 2016 Jakob von Raumer. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Jakob von Raumer
|
|
|
|
The Cofiber Type
|
|
-/
|
|
import hit.pointed_pushout function .susp types.unit
|
|
|
|
open eq pushout unit pointed is_trunc is_equiv susp unit
|
|
|
|
definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
|
|
|
|
namespace cofiber
|
|
section
|
|
parameters {A B : Type} (f : A → B)
|
|
|
|
protected definition base [constructor] : cofiber f := inl ⋆
|
|
|
|
protected definition cod [constructor] : B → cofiber f := inr
|
|
|
|
protected definition contr_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
|
|
begin
|
|
fapply is_contr.mk, exact base,
|
|
intro a, induction a with [u, b],
|
|
{ cases u, reflexivity },
|
|
{ exact !glue ⬝ ap inr (right_inv f b) },
|
|
{ apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _,
|
|
apply move_bot_of_left, refine !idp_con ⬝ph _, apply transpose, esimp,
|
|
refine _ ⬝hp (ap (ap inr) !adj⁻¹), refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
|
|
end
|
|
|
|
protected definition rec {A : Type} {B : Type} {f : A → B} {P : cofiber f → Type}
|
|
(Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (glue x) (Pinr (f x))) :
|
|
(Π y, P y) :=
|
|
begin
|
|
intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
|
|
end
|
|
|
|
protected definition rec_on {A : Type} {B : Type} {f : A → B} {P : cofiber f → Type}
|
|
(y : cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (glue x) (Pinr (f x))) : P y :=
|
|
begin
|
|
induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
|
|
end
|
|
|
|
end
|
|
end cofiber
|
|
|
|
-- pointed version
|
|
|
|
definition pcofiber {A B : Type*} (f : A →* B) : Type* := ppushout (pconst A punit) f
|
|
|
|
namespace cofiber
|
|
|
|
protected definition prec {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
|
|
(Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) :
|
|
(Π (y : pcofiber f), P y) :=
|
|
begin
|
|
intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
|
|
end
|
|
|
|
protected definition prec_on {A B : Type*} {f : A →* B} {P : pcofiber f → Type}
|
|
(y : pcofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
|
|
(Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : P y :=
|
|
begin
|
|
induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
|
|
end
|
|
|
|
protected definition pelim_on {A B C : Type*} {f : A →* B} (y : pcofiber f)
|
|
(c : C) (g : B → C) (p : Π x, c = g (f x)) : C :=
|
|
begin
|
|
fapply pushout.elim_on y, exact (λ x, c), exact g, exact p
|
|
end
|
|
|
|
--TODO more pointed recursors
|
|
|
|
variables (A : Type*)
|
|
|
|
definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A :=
|
|
begin
|
|
fapply pequiv_of_pmap,
|
|
{ fconstructor, intro x, induction x, exact north, exact south, exact merid x,
|
|
reflexivity },
|
|
{ esimp, fapply adjointify,
|
|
intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a,
|
|
intro s, induction s, do 2 reflexivity, esimp,
|
|
apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square,
|
|
refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
|
|
refine ap _ !elim_merid ⬝ _, apply elim_glue,
|
|
intro c, induction c with [n, s], induction n, reflexivity,
|
|
induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
|
|
refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
|
|
refine ap _ !elim_glue ⬝ _, apply elim_merid },
|
|
end
|
|
|
|
end cofiber
|