Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 *)

Definition grp_cxfib {A B C : Group} {i : A $-> B} {f : B $-> C} (cx : IsComplex i f)
  : GroupHomomorphism A (grp_kernel f)
  := grp_kernel_corec _ cx.

Definition grp_iso_cxfib {A B C : Group} {i : A $-> B} {f : B $-> C}
           `{IsEmbedding i} (ex : IsExact (Tr (-1)) i f)
  : GroupIsomorphism A (grp_kernel f)
  := Build_GroupIsomorphism _ _ (grp_cxfib cx_isexact) (isequiv_cxfib ex).

(** 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).
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
i $o grp_iso_inverse (grp_iso_cxfib ex) $==
subgroup_incl (grp_kernel f)
Proof.
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
i $o grp_iso_inverse (grp_iso_cxfib ex) $==
subgroup_incl (grp_kernel f)
  rapply equiv_ind.
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
IsEquiv ?Goal0
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
forall x : ?Goal,
(i $o grp_iso_inverse (grp_iso_cxfib ex)) (?Goal0 x) =
subgroup_incl (grp_kernel f) (?Goal0 x)
  1: exact (isequiv_cxfib ex).
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
forall x : A,
(i $o grp_iso_inverse (grp_iso_cxfib ex))
  (cxfib cx_isexact x) =
subgroup_incl (grp_kernel f) (cxfib cx_isexact x)
  intro x.
A, B, C: Group
i: A $-> B
f: B $-> C
IsEmbedding0: IsEmbedding i
ex: IsExact (Tr (-1)) i f
x: A
(i $o grp_iso_inverse (grp_iso_cxfib ex))
  (cxfib cx_isexact x) =
subgroup_incl (grp_kernel f) (cxfib cx_isexact 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.
X, Y: Group
f: X $-> Y
IsComplex (grp_trivial_rec X) f
Proof.
X, Y: Group
f: X $-> Y
IsComplex (grp_trivial_rec X) f
  srapply phomotopy_homotopy_hset.
X, Y: Group
f: X $-> Y
f o* grp_trivial_rec X == pconst
  intro x; cbn.
X, Y: Group
f: X $-> Y
x: grp_trivial
f group_unit = ispointed_group Y
  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.
A, B: Group
f: A $-> B
IsExact purely (grp_trivial_rec A) f <-> IsEmbedding f
Proof.
A, B: Group
f: A $-> B
IsExact purely (grp_trivial_rec A) f <-> IsEmbedding f
  split.
A, B: Group
f: A $-> B
IsExact purely (grp_trivial_rec A) f -> IsEmbedding f
A, B: Group
f: A $-> B
IsEmbedding f -> IsExact purely (grp_trivial_rec A) f
  -
A, B: Group
f: A $-> B
IsExact purely (grp_trivial_rec A) f -> IsEmbedding f intros ex b.
A, B: Group
f: A $-> B
ex: IsExact purely (grp_trivial_rec A) f
b: B
IsHProp (hfiber f b)
    apply hprop_inhabited_contr; intro a.
A, B: Group
f: A $-> B
ex: IsExact purely (grp_trivial_rec A) f
b: B
a: hfiber f b
Contr (hfiber f b)
    rapply (contr_equiv' grp_trivial).
A, B: Group
f: A $-> B
ex: IsExact purely (grp_trivial_rec A) f
b: B
a: hfiber f b
grp_trivial <~> hfiber f b
    exact ((equiv_grp_hfiber f b a)^-1 oE pequiv_cxfib).
  -
A, B: Group
f: A $-> B
IsEmbedding f -> IsExact purely (grp_trivial_rec A) f intro isemb_f.
A, B: Group
f: A $-> B
isemb_f: IsEmbedding f
IsExact purely (grp_trivial_rec A) f
    exists (grp_iscomplex_trivial f).
A, B: Group
f: A $-> B
isemb_f: IsEmbedding f
ReflectiveSubuniverse.IsConnMap purely
  (cxfib (grp_iscomplex_trivial f))
    intros y; rapply contr_inhabited_hprop.
A, B: Group
f: A $-> B
isemb_f: IsEmbedding f
y: pfiber f
purely (hfiber (cxfib (grp_iscomplex_trivial f)) y)
    exists 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. *)
Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
  : IsExact purely (grp_trivial_rec A) f
      <~> (grp_kernel f = trivial_subgroup :> Subgroup _)
  := (equiv_kernel_isembedding f)^-1%equiv
       oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).