Library HoTT.Algebra.Groups.ShortExactSequence

Require Import Basics Types.
Require Import Truncations.Core.
Require Import WildCat.Core Pointed.
Require Import Groups.Group Groups.Subgroup Groups.Kernel.
Require Import Homotopy.ExactSequence Modalities.Identity.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.
Local Open Scope path_scope.

Complexes of groups

This is the same proof as for equiv_cxfib_beta, but giving the proof is easier than specializing the general result.

Proposition grp_iso_cxfib_beta {A B C : Group} {i : A $-> B} {f : B $-> C}
            `{IsEmbedding i} (ex : IsExact (Tr (-1)) i f)
  : i $o (grp_iso_inverse (grp_iso_cxfib ex)) $== subgroup_incl (grp_kernel f).
Proof.
  rapply equiv_ind.
  1: exact (isequiv_cxfib ex).
  intro x.
  exact (ap (fun y ⇒ i y) (eissect _ x)).
Defined.

Definition grp_iscomplex_trivial {X Y : Group} (f : X $-> Y)
  : IsComplex (grp_trivial_rec X) f.
Proof.
  srapply phomotopy_homotopy_hset.
  intro x; cbn.
  exact (grp_homo_unit f).
Defined.

A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding.

Lemma iff_grp_isexact_isembedding {A B : Group} (f : A $-> B)
  : IsExact purely (grp_trivial_rec A) f ↔ IsEmbedding f.
Proof.
  split.
  - intros ex b.
    apply hprop_inhabited_contr; intro a.
    rapply (contr_equiv' grp_trivial).
    exact ((equiv_grp_hfiber f b a)^-1 oE pequiv_cxfib).
  - intro isemb_f.
    ∃ (grp_iscomplex_trivial f).
    intros y; rapply contr_inhabited_hprop.
    ∃ tt; apply path_ishprop.
Defined.

A complex 0 -> A -> B is purely exact if and only if the kernel of the map A -> B is trivial.