Library HoTT.Algebra.Groups.ShortExactSequence
From HoTT Require Import Basics Types.
Require Import Truncations.Core.
Require Import WildCat.Core Pointed.Core.
Require Import Groups.Group Groups.Subgroup.
Require Import Homotopy.ExactSequence Modalities.Identity.
Require Import Truncations.Core.
Require Import WildCat.Core Pointed.Core.
Require Import Groups.Group Groups.Subgroup.
Require Import Homotopy.ExactSequence Modalities.Identity.
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).
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.
`{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.
If A → B → C is exact at B with A contractible, then B → C is an embedding. Only B and C need to be groups; A can be any pointed type. Note also that (-1)-exactness suffices, which is what one gets from a fiber sequence after truncating.
Definition isembedding_isexact {A : pType} {B C : Group} {i : A ->* B} {f : B $-> C}
`{Contr A} (ex : IsExact (Tr (-1)) i f)
: IsEmbedding f.
Proof.
(* Since A is contractible and B is a set, i is an embedding, which upgrades exactness to an equivalence between A and the fiber of f over the identity. This is needed by equiv_cxfib. *)
assert (IsEmbedding i) by (intro b; rapply istrunc_sigma).
intro c.
apply hprop_inhabited_contr; intro b.
rapply (contr_equiv' A).
exact ((equiv_grp_hfiber f c b)^-1 oE equiv_cxfib ex).
Defined.
`{Contr A} (ex : IsExact (Tr (-1)) i f)
: IsEmbedding f.
Proof.
(* Since A is contractible and B is a set, i is an embedding, which upgrades exactness to an equivalence between A and the fiber of f over the identity. This is needed by equiv_cxfib. *)
assert (IsEmbedding i) by (intro b; rapply istrunc_sigma).
intro c.
apply hprop_inhabited_contr; intro b.
rapply (contr_equiv' A).
exact ((equiv_grp_hfiber f c b)^-1 oE equiv_cxfib ex).
Defined.
A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding. (This is also true with purely replaced by Tr (-1).)
Lemma iff_grp_isexact_isembedding {A B : Group} (f : A $-> B)
: IsExact purely (grp_trivial_rec A) f ↔ IsEmbedding f.
Proof.
split.
- intro ex.
exact (isembedding_isexact (isexact_purely_O _ _ (H:=ex))).
- intro isemb_f.
∃ (grp_iscomplex_trivial f).
intros y; rapply contr_inhabited_hprop.
∃ tt; apply path_ishprop.
Defined.
: IsExact purely (grp_trivial_rec A) f ↔ IsEmbedding f.
Proof.
split.
- intro ex.
exact (isembedding_isexact (isexact_purely_O _ _ (H:=ex))).
- 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.
Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
: IsExact purely (grp_trivial_rec A) f <~> IsTrivialGroup (grp_kernel f)
:= (equiv_istrivial_kernel_isembedding f)^-1%equiv
oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).
: IsExact purely (grp_trivial_rec A) f <~> IsTrivialGroup (grp_kernel f)
:= (equiv_istrivial_kernel_isembedding f)^-1%equiv
oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).
If A → B → C → D is exact at B and C, with A and D contractible, then the middle map is an isomorphism. Only B and C need to be groups.
Definition grp_iso_isexact {A : pType} {B C : Group} {D : pType}
{h : A ->* B} {f : B $-> C} {g : C ->* D} `{Contr A} `{Contr D}
(exl : IsExact (Tr (-1)) h f) (exr : IsExact (Tr (-1)) f g)
: GroupIsomorphism B C.
Proof.
snapply (Build_GroupIsomorphism _ _ f).
napply isequiv_surj_emb.
- exact (isconnmap_O_isexact_base_contr _ f g).
- exact (isembedding_isexact exl).
Defined.
{h : A ->* B} {f : B $-> C} {g : C ->* D} `{Contr A} `{Contr D}
(exl : IsExact (Tr (-1)) h f) (exr : IsExact (Tr (-1)) f g)
: GroupIsomorphism B C.
Proof.
snapply (Build_GroupIsomorphism _ _ f).
napply isequiv_surj_emb.
- exact (isconnmap_O_isexact_base_contr _ f g).
- exact (isembedding_isexact exl).
Defined.