Library HoTT.Homotopy.WhiteheadsPrinciple
From HoTT Require Import Basics Types.
Require Import Pointed.
Require Import WildCat.Core HFiber.
Require Import Truncations.
Require Import Algebra.Groups.Group Algebra.Groups.ShortExactSequence.
Require Import Homotopy.HomotopyGroup Homotopy.ExactSequence.
Require Import Modalities.Identity.
Require Import Spaces.Nat.Core.
Local Open Scope pointed_scope.
Local Open Scope nat_scope.
Require Import Pointed.
Require Import WildCat.Core HFiber.
Require Import Truncations.
Require Import Algebra.Groups.Group Algebra.Groups.ShortExactSequence.
Require Import Homotopy.HomotopyGroup Homotopy.ExactSequence.
Require Import Modalities.Identity.
Require Import Spaces.Nat.Core.
Local Open Scope pointed_scope.
Local Open Scope nat_scope.
8.8.1
Definition isequiv_issurj_tr0_isequiv_ap
`{Univalence} {A B : Type} (f : A → B)
{i : IsSurjection (Trunc_functor 0 f)}
{ii : ∀ x y, IsEquiv (@ap _ _ f x y)}
: IsEquiv f.
Proof.
apply (equiv_isequiv_ap_isembedding f)^-1 in ii.
srapply isequiv_surj_emb.
srapply BuildIsSurjection.
cbn; intro b.
pose proof (@center _ (i (tr b))) as p.
revert p.
apply Trunc_functor.
apply sig_ind.
srapply Trunc_ind.
intros a p.
apply (equiv_path_Tr _ _)^-1 in p.
strip_truncations.
∃ a.
exact p.
Defined.
`{Univalence} {A B : Type} (f : A → B)
{i : IsSurjection (Trunc_functor 0 f)}
{ii : ∀ x y, IsEquiv (@ap _ _ f x y)}
: IsEquiv f.
Proof.
apply (equiv_isequiv_ap_isembedding f)^-1 in ii.
srapply isequiv_surj_emb.
srapply BuildIsSurjection.
cbn; intro b.
pose proof (@center _ (i (tr b))) as p.
revert p.
apply Trunc_functor.
apply sig_ind.
srapply Trunc_ind.
intros a p.
apply (equiv_path_Tr _ _)^-1 in p.
strip_truncations.
∃ a.
exact p.
Defined.
8.8.2
Definition isequiv_isbij_tr0_isequiv_loops
`{Univalence} {A B : Type} (f : A → B)
{i : IsEquiv (Trunc_functor 0 f)}
{ii : ∀ x, IsEquiv (fmap loops (pmap_from_point f x)) }
: IsEquiv f.
Proof.
srapply (isequiv_issurj_tr0_isequiv_ap f).
intros x y.
apply isequiv_inhab_codomain.
intro p.
apply (ap (@tr 0 _)) in p.
apply (@equiv_inj _ _ _ i (tr x) (tr y)) in p.
apply (equiv_path_Tr _ _)^-1 in p.
strip_truncations.
destruct p.
cbn in ii.
snapply (isequiv_homotopic _ (H:=ii x)).
exact (fun _ ⇒ concat_1p _ @ concat_p1 _).
Defined.
`{Univalence} {A B : Type} (f : A → B)
{i : IsEquiv (Trunc_functor 0 f)}
{ii : ∀ x, IsEquiv (fmap loops (pmap_from_point f x)) }
: IsEquiv f.
Proof.
srapply (isequiv_issurj_tr0_isequiv_ap f).
intros x y.
apply isequiv_inhab_codomain.
intro p.
apply (ap (@tr 0 _)) in p.
apply (@equiv_inj _ _ _ i (tr x) (tr y)) in p.
apply (equiv_path_Tr _ _)^-1 in p.
strip_truncations.
destruct p.
cbn in ii.
snapply (isequiv_homotopic _ (H:=ii x)).
exact (fun _ ⇒ concat_1p _ @ concat_p1 _).
Defined.
When the types are pointed and 0-connected, and the map is pointed, just one loops_functor needs to be checked.
Definition isequiv_is0connected_isequiv_loops
`{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B}
(f : A ->* B)
(e : IsEquiv (fmap loops f))
: IsEquiv f.
Proof.
apply isequiv_isbij_tr0_isequiv_loops.
`{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B}
(f : A ->* B)
(e : IsEquiv (fmap loops f))
: IsEquiv f.
Proof.
apply isequiv_isbij_tr0_isequiv_loops.
Since A is 0-connected, it's enough to check the loops_functor condition for the basepoint.
The loops_functor condition for pmap_from_point f _ is equivalent to the loops_functor condition for f with its given pointing.
srapply isequiv_homotopic'.
- exact (equiv_concat_lr (point_eq f) (point_eq f)^ oE (Build_Equiv _ _ _ e)).
- intro r.
simpl.
hott_simpl.
Defined.
- exact (equiv_concat_lr (point_eq f) (point_eq f)^ oE (Build_Equiv _ _ _ e)).
- intro r.
simpl.
hott_simpl.
Defined.
Truncated Whitehead's principle (8.8.3)
Definition whiteheads_principle
{ua : Univalence} {A B : Type} {f : A → B}
(n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
{i : IsEquiv (Trunc_functor 0 f)}
{ii : ∀ (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x)) }
: IsEquiv f.
Proof.
revert A B H0 H1 f i ii.
induction n as [|n IHn].
1: intros; apply isequiv_contr_contr.
intros A B H0 H1 f i ii.
nrefine (@isequiv_isbij_tr0_isequiv_loops ua _ _ f i _).
intro x.
nrefine (isequiv_homotopic (@ap _ _ f x x) _).
2:{intros p; cbn.
symmetry; exact (concat_1p _ @ concat_p1 _). }
pose proof (@istrunc_paths _ _ H0 x x) as h0.
pose proof (@istrunc_paths _ _ H1 (f x) (f x)) as h1.
nrefine (IHn (x=x) (f x=f x) h0 h1 (@ap _ _ f x x) _ _).
- pose proof (ii x 0) as h2.
unfold is0functor_pi in h2; cbn in h2.
refine (@isequiv_homotopic _ _ _ _ h2 _).
apply (O_functor_homotopy (Tr 0)); intros p.
exact (concat_1p _ @ concat_p1 _).
- intros p k; revert p.
assert (h3 : ∀ (y:A) (q:x=y),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (@ap _ _ f x y) q))).
2:exact (h3 x).
intros y q. destruct q.
snrefine (isequiv_homotopic _ _).
1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))).
2:{ tapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
- intros p; cbn.
exact (concat_1p _ @ concat_p1 _).
- reflexivity. }
nrefine (isequiv_commsq _ _ _ _ (fmap_pi_loops k.+1 (pmap_from_point f x))).
2-3:exact (equiv_isequiv (pi_loops _ _)).
exact (ii x k.+1).
Defined.
{ua : Univalence} {A B : Type} {f : A → B}
(n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
{i : IsEquiv (Trunc_functor 0 f)}
{ii : ∀ (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x)) }
: IsEquiv f.
Proof.
revert A B H0 H1 f i ii.
induction n as [|n IHn].
1: intros; apply isequiv_contr_contr.
intros A B H0 H1 f i ii.
nrefine (@isequiv_isbij_tr0_isequiv_loops ua _ _ f i _).
intro x.
nrefine (isequiv_homotopic (@ap _ _ f x x) _).
2:{intros p; cbn.
symmetry; exact (concat_1p _ @ concat_p1 _). }
pose proof (@istrunc_paths _ _ H0 x x) as h0.
pose proof (@istrunc_paths _ _ H1 (f x) (f x)) as h1.
nrefine (IHn (x=x) (f x=f x) h0 h1 (@ap _ _ f x x) _ _).
- pose proof (ii x 0) as h2.
unfold is0functor_pi in h2; cbn in h2.
refine (@isequiv_homotopic _ _ _ _ h2 _).
apply (O_functor_homotopy (Tr 0)); intros p.
exact (concat_1p _ @ concat_p1 _).
- intros p k; revert p.
assert (h3 : ∀ (y:A) (q:x=y),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (@ap _ _ f x y) q))).
2:exact (h3 x).
intros y q. destruct q.
snrefine (isequiv_homotopic _ _).
1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))).
2:{ tapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
- intros p; cbn.
exact (concat_1p _ @ concat_p1 _).
- reflexivity. }
nrefine (isequiv_commsq _ _ _ _ (fmap_pi_loops k.+1 (pmap_from_point f x))).
2-3:exact (equiv_isequiv (pi_loops _ _)).
exact (ii x k.+1).
Defined.
When the types are pointed and 0-connected, and the map is pointed, it's enough to check condition ii at the base point.
Definition whiteheads_principle_is0connected
{ua : Univalence} {A B : pType} {f : A ->* B}
(n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
{cA : IsConnected 0 A} {cB : IsConnected 0 B}
{ii : ∀ (k : nat), IsEquiv (fmap (Pi k.+1) f) }
: IsEquiv f.
Proof.
snapply (whiteheads_principle n).
1, 2: assumption.
1: apply isequiv_contr_contr.
(* We eliminate into IsEquiv for each k separately. Eliminating into ∀ k : nat, IsEquiv _ would use istrunc_forall with nat in an unconstrained universe, adding two universe variables to this result and to everything that uses it. *)
intros x k; revert x.
rapply conn_point_elim.
pointed_reduce_pmap f.
exact (ii k).
Defined.
{ua : Univalence} {A B : pType} {f : A ->* B}
(n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
{cA : IsConnected 0 A} {cB : IsConnected 0 B}
{ii : ∀ (k : nat), IsEquiv (fmap (Pi k.+1) f) }
: IsEquiv f.
Proof.
snapply (whiteheads_principle n).
1, 2: assumption.
1: apply isequiv_contr_contr.
(* We eliminate into IsEquiv for each k separately. Eliminating into ∀ k : nat, IsEquiv _ would use istrunc_forall with nat in an unconstrained universe, adding two universe variables to this result and to everything that uses it. *)
intros x k; revert x.
rapply conn_point_elim.
pointed_reduce_pmap f.
exact (ii k).
Defined.
A pointed map between n-1-connected, n-truncated pointed types which induces an equivalence on Pi n is an equivalence. Only the top homotopy group of such a type is non-trivial, so this is the only condition Whitehead's principle leaves to check.
Definition isequiv_isconnected_istrunc_isequiv_pi `{Univalence} (n : nat) {X Y : pType}
(f : X ->* Y)
{cX : IsConnected (nat_pred n) X} {tX : IsTrunc n X}
{cY : IsConnected (nat_pred n) Y} {tY : IsTrunc n Y}
{e : IsEquiv (fmap (pPi n) f)}
: IsEquiv f.
Proof.
snapply (whiteheads_principle_is0connected n).
1, 2: assumption.
1, 2: rapply is0connected_isconnected.
intro k.
destruct (nat_trichotomy k.+1 n) as [[kltn | keqn] | kgtn].
- napply isequiv_contr_contr.
all: rapply (contr_pi_isconnected (nat_pred n) (mlen:=leq_pred kltn)).
- destruct keqn; exact e.
- napply isequiv_contr_contr.
all: rapply (contr_pi_istrunc n (nltm:=kgtn)).
Defined.
(f : X ->* Y)
{cX : IsConnected (nat_pred n) X} {tX : IsTrunc n X}
{cY : IsConnected (nat_pred n) Y} {tY : IsTrunc n Y}
{e : IsEquiv (fmap (pPi n) f)}
: IsEquiv f.
Proof.
snapply (whiteheads_principle_is0connected n).
1, 2: assumption.
1, 2: rapply is0connected_isconnected.
intro k.
destruct (nat_trichotomy k.+1 n) as [[kltn | keqn] | kgtn].
- napply isequiv_contr_contr.
all: rapply (contr_pi_isconnected (nat_pred n) (mlen:=leq_pred kltn)).
- destruct keqn; exact e.
- napply isequiv_contr_contr.
all: rapply (contr_pi_istrunc n (nltm:=kgtn)).
Defined.
A complex F → X → Y of pointed types is a fiber sequence when F is n-connected and n.+1-truncated, X and Y are n.+1-truncated, f is an n-connected map, fmap (Pi n.+1) i is an embedding and the complex is exact on Pi n.+1. Indeed, F and the fiber of f are then both n-connected and n.+1-truncated, and on Pi n.+1 both are the kernel of fmap (Pi n.+1) f, so cxfib is an equivalence by the previous result.
Definition isexact_purely_isexact_pi `{Univalence} (n : nat) {F X Y : pType}
{i : F ->* X} {f : X ->* Y} (cx : IsComplex i f)
`{IsConnected n F} `{IsTrunc n.+1 F} `{IsTrunc n.+1 X} `{IsTrunc n.+1 Y}
`{!IsConnMap n f} `{!IsEmbedding (fmap (pPi n.+1) i)}
(ex : IsExact (Tr (-1)) (fmap (pPi n.+1) i) (fmap (pPi n.+1) f))
: IsExact purely i f.
Proof.
∃ cx.
napply conn_map_isequiv.
napply (isequiv_isconnected_istrunc_isequiv_pi n.+1).
1-4: exact _.
pose (j := fmap (Pi n.+1) (pfib f)). (* To make the goals readable. *)
napply (isequiv_isexact_factor (j:=j) _ _ ex).
- intro x.
exact ((fmap_comp (Pi n.+1) (cxfib cx) (pfib f) x)^
@ fmap2 (Pi n.+1) (pfib_cxfib cx) x).
- exact _.
- exact (isembedding_fmap_pi_isexact _ _ n (c := contr_pi_istrunc n.+1 _)).
- exact (isexact_pi_total _ _ n.+1).
Defined.
{i : F ->* X} {f : X ->* Y} (cx : IsComplex i f)
`{IsConnected n F} `{IsTrunc n.+1 F} `{IsTrunc n.+1 X} `{IsTrunc n.+1 Y}
`{!IsConnMap n f} `{!IsEmbedding (fmap (pPi n.+1) i)}
(ex : IsExact (Tr (-1)) (fmap (pPi n.+1) i) (fmap (pPi n.+1) f))
: IsExact purely i f.
Proof.
∃ cx.
napply conn_map_isequiv.
napply (isequiv_isconnected_istrunc_isequiv_pi n.+1).
1-4: exact _.
pose (j := fmap (Pi n.+1) (pfib f)). (* To make the goals readable. *)
napply (isequiv_isexact_factor (j:=j) _ _ ex).
- intro x.
exact ((fmap_comp (Pi n.+1) (cxfib cx) (pfib f) x)^
@ fmap2 (Pi n.+1) (pfib_cxfib cx) x).
- exact _.
- exact (isembedding_fmap_pi_isexact _ _ n (c := contr_pi_istrunc n.+1 _)).
- exact (isexact_pi_total _ _ n.+1).
Defined.