Library HoTT.Algebra.AbSES.Ext

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)).
Proof.
  refine (equiv_path_Tr _ _ oE _).
  srapply equiv_iff_hprop;
    apply Trunc_functor;
    apply iff_abses_trivial_split.
Defined.

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.
Proof.
  snrapply (Build_Group (Ext B A)).
  - intros E F.
    strip_truncations.
    exact (tr (abses_baer_sum E F)).
  - exact (point (Ext B A)).
  - unfold Negate.
    exact (Trunc_functor _ (abses_pullback (- grp_homo_id))).
  - repeat split.
    1: apply istrunc_truncation.
    all: intro E. 1: intros F G.
    all: strip_truncations; unfold mon_unit, point; apply (ap tr).
    + symmetry; apply baer_sum_associative.
    + apply baer_sum_unit_l.
    + apply baer_sum_unit_r.
    + apply baer_sum_inverse_r.
    + apply baer_sum_inverse_l.
Defined.

The bifunctor ab_ext

Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u }^op) (A : AbGroup@{u }) : AbGroup@{v }.
Proof.
  snrapply (Build_AbGroup (grp_ext@{u v } B A)).
  intros E F.
  strip_truncations; cbn.
  apply ap.
  apply baer_sum_commutative.
Defined.

Global Instance is0functor_abext01 `{Univalence} (B : AbGroup ^op)
  : Is0Functor (ab_ext B).
Proof.
  srapply Build_Is0Functor; intros ? ? f.
  snrapply Build_GroupHomomorphism.
  1: exact (fmap (Ext B) f).
  rapply Trunc_ind; intro E0.
  rapply Trunc_ind; intro E1.
  apply (ap tr); cbn.
  apply baer_sum_pushout.
Defined.

Global Instance is0functor_abext10 `{Univalence} (A : AbGroup)
  : Is0Functor (fun B : AbGroup ^op ⇒ ab_ext B A).
Proof.
  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.
  apply (ap tr); cbn.
  apply baer_sum_pullback.
Defined.

Global Instance is1functor_abext01 `{Univalence} (B : AbGroup ^op)
  : Is1Functor (ab_ext B).
Proof.
  snrapply Build_Is1Functor.
  - intros A C f g.
    exact (fmap2 (Ext B)).
  - exact (fmap_id (Ext B)).
  - intros A C D.
    exact (fmap_comp (Ext B)).
Defined.

Global Instance is1functor_abext10 `{Univalence} (A : AbGroup)
  : Is1Functor (fun B : AbGroup ^op ⇒ ab_ext B A).
Proof.
  snrapply Build_Is1Functor.
  - intros B C f g.
    exact (fmap2 (fun B : AbGroup ^op ⇒ Ext B A)).
  - exact (fmap_id (fun B : AbGroup ^op ⇒ Ext B A)).
  - intros B C D.
    exact (fmap_comp (fun B : AbGroup ^op ⇒ Ext B A)).
Defined.

Global Instance is0bifunctor_abext `{Univalence}
  : Is0Bifunctor (A:=AbGroup ^op) ab_ext.
Proof.
  rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_abext `{Univalence}
  : Is1Bifunctor (A:=AbGroup ^op) ab_ext.
Proof.
  snrapply Build_Is1Bifunctor''.
  1,2: exact _.
  intros A B.
  exact (bifunctor_coh (Ext : AbGroup ^op → AbGroup → pType)).
Defined.

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).
Proof.
  snrapply Build_GroupHomomorphism.
  1: exact (fun f ⇒ fmap01 (A:=AbGroup ^op) Ext' _ f (tr E)).
  intros f g; cbn.
  nrapply (ap tr).
  exact (baer_sum_distributive_pushouts f g).
Defined.

Extensions ending in a projective are trivial

Proposition abext_trivial_projective `{Univalence}
  (P : AbGroup) `{IsAbProjective P}
  : ∀ A , ∀ E : AbSES P A , tr E = point (Ext P A).
Proof.
  intros A E.
  apply iff_ab_ext_trivial_split.
  exact (fst (iff_isabprojective_surjections_split P) _ _ _ _).
Defined.

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).
Proof.
  apply (Build_Contr _ (point _)); intro E.
  strip_truncations.
  symmetry; by apply abext_trivial_projective.
Defined.

(* Converely, if all extensions ending in P are trivial, then P is projective. *)
Proposition abext_projective_trivial `{Univalence} (P : AbGroup)
  (ext_triv : ∀ A , ∀ E : AbSES P A , tr E = point (Ext P A))
  : IsAbProjective P.
Proof.
  apply iff_isabprojective_surjections_split.
  intros E p issurj_p.
  apply (iff_ab_ext_trivial_split (abses_from_surjection p))^-1.
  apply ext_triv.
Defined.