From HoTT Require Import Basics Types WildCat Pointed Truncations
ExactSequence AbGroups AbSES AbSES.SixTerm.
Require Import Lemmas EquivalenceRelation Ext ES HigherExt XII_5.
Local Open Scope pointed_scope.
Local Open Scope type_scope.
(** * The long exact sequence of Ext groups *)
(** Currently [Ext n] is only a pointed set, but the notion of exactness abelian groups is the same. *)
(** Exactness at the domain of the connecting map, for all n. *)
Global Instance isexact_extn_inclusion_splice `{Univalence} {n : nat}
{B A G : AbGroup} (E : ES 1 B A)
: IsExact (Tr (-1))
(ext_pullback (n:=n) (A:=G) (inclusion E))
(abses_ext_splice E).
Proof.
destruct n as [|n].
(* The case [n=0] follows from [isexact_ext_contra_sixterm_iii]. *)
{ rapply isexact_homotopic_f.
by apply phomotopy_homotopy_hset. }
unshelve econstructor.
{ hnf.
refine (splice_pullback_to_pushout_phomotopy _ _ @* _).
rewrite abses_pushout_inclusion.
apply abses_ext_splice_pt. }
intros [S p]; revert dependent S.
(** TODO make a tactic for the following. *)
destruct n.
1: rapply Trunc_ind; intros S p;
rapply contr_inhabited_hprop;
pose proof (K := snd (ext_XII_5_5 (S : ES 1 A G) E) p^).
2: rapply Quotient_ind_hprop; intros S p;
rapply contr_inhabited_hprop;
pose proof (K := snd (ext_XII_5_5 S E) p^).
all: strip_truncations; destruct K as [K q];
refine (tr (K; _));
apply path_sigma_hprop;
exact q.
Defined.
(** Exactness at the domain of the connecting map, for all n. *)
(** The proof writes out the first part of Lemma XII.5.2. *)
Global Instance isexact_extn_splice_pullback `{Univalence} {n : nat}
{B A G : AbGroup} (E : AbSES B A)
: IsExact (Tr (-1))
(abses_ext_splice (n:=n) (M:=G) E)
(ext_pullback (projection E)).
Proof.
destruct n as [|n].
{ rapply isexact_homotopic_if.
all: by apply phomotopy_homotopy_hset. }
srapply Build_IsExact.
{ refine (splice_pullback_commute _ _ @* _).
rewrite <- abses_pullback_projection.
apply abses_ext_splice_pt. }
hnf.
intros [S p]; revert dependent S.
rapply Quotient_ind_hprop; intros [C [T F]] p.
rapply contr_inhabited_hprop.
pose (Fs := abses_pullback (projection E) F).
assert (U : merely (hfiber (ext_pullback (inclusion Fs)) (es_in T))).
{ rapply isexact_preimage.
1: apply isexact_extn_inclusion_splice.
refine ((splice_pullback_commute _ _ _)^ @ _).
destruct n; exact p. }
strip_truncations; destruct U as [U q].
pose (F' := abses_pushout (inclusion Fs) F).
assert (alpha : merely (hfiber (abses_pushout_ext E)
(es_in (F' : ES 1 B Fs)))).
{ rapply (isexact_preimage _ (abses_pushout_ext E)).
(* TODO Why do we have to specify the map above? *)
apply (ap tr).
refine ((abses_pushout_pullback_reorder _ _ _)^ @ _).
apply abses_pushout_inclusion. }
strip_truncations; destruct alpha as [alpha r].
pose proof (r' := (equiv_path_Tr _ _)^-1 r);
strip_truncations.
refine (tr (ext_pullback alpha U; _)).
apply path_sigma_hprop.
unfold cxfib, Build_pMap, pointed_fun, pr1.
refine (splice_pullback_to_pushout _ _ _ @ _).
refine (ap (ext_abses_splice U) r' @ _); clear r'.
unfold F'.
refine ((splice_pullback_to_pushout _ _ _)^ @ _).
rewrite q.
destruct n; reflexivity.
Defined.
(** Exactness at the middle term, for n > 0. The zeroth level is covered by [isexact_ext_sixterm_ii]. *)
Global Instance isexact_extn_pullback_pullback `{Univalence} {n : nat}
{B A G : AbGroup} (E : AbSES B A)
: IsExact (Tr (-1))
(ext_pullback (n:=n.+1) (A:=G) (projection E))
(ext_pullback (inclusion E)).
Proof.
destruct n.
{ rapply isexact_homotopic_if.
all: by apply phomotopy_homotopy_hset. }
srapply Build_IsExact.
{ apply phomotopy_homotopy_hset.
rapply Quotient_ind_hprop; intro F.
apply qglue.
refine (transport (fun X => es_meqrel X pt) _^ _).
{ refine (es_pullback_compose _ _ _ @ _).
refine (es_pullback_homotopic _ _ (f':=grp_homo_const)).
intro; apply isexact_inclusion_projection. }
apply zag_to_meqrel.
apply es_pullback_const_zig. }
hnf.
intros [S p]; revert dependent S.
rapply Quotient_ind_hprop; intros [C [T F]] p.
rapply contr_inhabited_hprop.
pose (Fs := abses_pullback (inclusion E) F).
assert (U : merely (hfiber (ext_pullback (inclusion Fs)) (es_in T))).
{ rapply isexact_preimage.
1: apply isexact_extn_inclusion_splice.
refine ((splice_pullback_commute _ _ _)^ @ _).
destruct n; exact p. }
strip_truncations; destruct U as [U q].
pose (iF := abses_pushout (inclusion Fs) F).
assert (F' : (hfiber
(abses_pullback_pmap (projection E))
iF)).
{ (* Uses [isexact_abses_pullback]. *)
rapply (isexact_preimage _ (abses_pullback_pmap (projection E))).
refine ((abses_pushout_pullback_reorder _ _ _)^ @ _).
exact (abses_pushout_inclusion Fs). }
destruct F' as [F' r].
refine (tr (ext_abses_splice U F'; _)).
apply path_sigma_hprop.
unfold cxfib, Build_pMap, pointed_fun, pr1.
refine (splice_pullback_commute F' (projection E) U @ _).
refine (ap (fun X => abses_ext_splice X U) r @ _).
refine ((splice_pullback_to_pushout _ _ _)^ @ _).
refine (ap (abses_ext_splice F) q @ _).
destruct n; reflexivity.
Defined.