Timings for Ext.v
Require Import Basics Types Truncations.Core.
Require Import Pointed WildCat.
Require Import Truncations.SeparatedTrunc.
Require Import AbelianGroup AbHom AbProjective.
Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.
Local Open Scope mc_scope.
Local Open Scope mc_add_scope.
(** * The set [Ext B A] of abelian group extensions *)
Definition Ext (B A : AbGroup@{u}) := pTr 0 (AbSES B A).
Global Instance is0bifunctor_ext `{Univalence}
: Is0Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
:= is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses).
Global Instance is1bifunctor_ext `{Univalence}
: Is1Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
:= is1bifunctor_postcompose _ _ (bf:=is1bifunctor_abses).
(** An extension [E : AbSES B A] is trivial in [Ext B A] if and only if [E] merely splits. *)
Proposition iff_ab_ext_trivial_split `{Univalence} {B A : AbGroup} (E : AbSES B A)
: merely {s : GroupHomomorphism B E & (projection _) $o s == idmap}
<~> (tr E = point (Ext B A)).
refine (equiv_path_Tr _ _ oE _).
srapply equiv_iff_hprop;
apply Trunc_functor;
apply iff_abses_trivial_split.
Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
Global Instance is0bifunctor_ext' `{Univalence}
: Is0Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
:= is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses').
Global Instance is1bifunctor_ext' `{Univalence}
: Is1Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
:= is1bifunctor_postcompose _ _ (bf:=is1bifunctor_abses').
(** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
snrapply (Build_Group (Ext B A)).
exact (tr (abses_baer_sum E F)).
exact (Trunc_functor _ (abses_pullback (- grp_homo_id))).
1: apply istrunc_truncation.
all: strip_truncations; unfold mon_unit, point; apply (ap tr).
symmetry; apply baer_sum_associative.
apply baer_sum_inverse_r.
apply baer_sum_inverse_l.
(** ** The bifunctor [ab_ext] *)
Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}.
snrapply (Build_AbGroup (grp_ext@{u v} B A)).
apply baer_sum_commutative.
Global Instance is0functor_abext01 `{Univalence} (B : AbGroup^op)
: Is0Functor (ab_ext B).
srapply Build_Is0Functor; intros ? ? f.
snrapply Build_GroupHomomorphism.
1: exact (fmap (Ext B) f).
rapply Trunc_ind; intro E0.
rapply Trunc_ind; intro E1.
Global Instance is0functor_abext10 `{Univalence} (A : AbGroup)
: Is0Functor (fun B : AbGroup^op => ab_ext B A).
srapply Build_Is0Functor; intros ? ? f; cbn.
snrapply Build_GroupHomomorphism.
1: exact (fmap (fun (B : AbGroup^op) => Ext B A) f).
rapply Trunc_ind; intro E0.
rapply Trunc_ind; intro E1.
Global Instance is1functor_abext01 `{Univalence} (B : AbGroup^op)
: Is1Functor (ab_ext B).
snrapply Build_Is1Functor.
exact (fmap_comp (Ext B)).
Global Instance is1functor_abext10 `{Univalence} (A : AbGroup)
: Is1Functor (fun B : AbGroup^op => ab_ext B A).
snrapply Build_Is1Functor.
exact (fmap2 (fun B : AbGroup^op => Ext B A)).
exact (fmap_id (fun B : AbGroup^op => Ext B A)).
exact (fmap_comp (fun B : AbGroup^op => Ext B A)).
Global Instance is0bifunctor_abext `{Univalence}
: Is0Bifunctor (A:=AbGroup^op) ab_ext.
rapply Build_Is0Bifunctor''.
Global Instance is1bifunctor_abext `{Univalence}
: Is1Bifunctor (A:=AbGroup^op) ab_ext.
snrapply Build_Is1Bifunctor''.
exact (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType)).
(** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
Definition abses_pushout_ext `{Univalence}
{B A G : AbGroup@{u}} (E : AbSES B A)
: GroupHomomorphism (ab_hom A G) (ab_ext B G).
snrapply Build_GroupHomomorphism.
1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
exact (baer_sum_distributive_pushouts f g).
(** ** Extensions ending in a projective are trivial *)
Proposition abext_trivial_projective `{Univalence}
(P : AbGroup) `{IsAbProjective P}
: forall A, forall E : AbSES P A, tr E = point (Ext P A).
apply iff_ab_ext_trivial_split.
exact (fst (iff_isabprojective_surjections_split P) _ _ _ _).
(** It follows that when [P] is projective, [Ext P A] is contractible. *)
Global Instance contr_abext_projective `{Univalence}
(P : AbGroup) `{IsAbProjective P} {A : AbGroup}
: Contr (Ext P A).
apply (Build_Contr _ (point _)); intro E.
symmetry; by apply abext_trivial_projective.
(* Converely, if all extensions ending in [P] are trivial, then [P] is projective. *)
Proposition abext_projective_trivial `{Univalence} (P : AbGroup)
(ext_triv : forall A, forall E : AbSES P A, tr E = point (Ext P A))
: IsAbProjective P.
apply iff_isabprojective_surjections_split.
apply (iff_ab_ext_trivial_split (abses_from_surjection p))^-1.