Ext.v

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

Instance is0bifunctor_ext `{Univalence}
  : Is0Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
  := is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses).

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)).H: Univalence
B, A: AbGroup
E: AbSES B A
merely
  {s : GroupHomomorphism B E &
  projection E $o s == idmap} <~>
tr E = point (Ext B A)
Proof.H: Univalence
B, A: AbGroup
E: AbSES B A
merely
  {s : GroupHomomorphism B E &
  projection E $o s == idmap} <~>
tr E = point (Ext B A)
  refine (equiv_path_Tr _ _ oE _).H: Univalence
B, A: AbGroup
E: AbSES B A
merely
  {s : GroupHomomorphism B E &
  projection E $o s == idmap} <~>
Tr (-1) (E = point (AbSES B A))
  srapply equiv_iff_hprop;
    apply Trunc_functor;
    apply iff_abses_trivial_split.
Defined.

Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).

Instance is0bifunctor_ext' `{Univalence}
  : Is0Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
  := is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses').

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.H: Univalence
B, A: AbGroup
Group
Proof.H: Univalence
B, A: AbGroup
Group
  snapply (Build_Group (Ext B A)).H: Univalence
B, A: AbGroup
SgOp (Ext B A)
H: Univalence
B, A: AbGroup
MonUnit (Ext B A)
H: Univalence
B, A: AbGroup
Inverse (Ext B A)
H: Univalence
B, A: AbGroup
IsGroup (Ext B A)
  -H: Univalence
B, A: AbGroup
SgOp (Ext B A) intros E F.H: Univalence
B, A: AbGroup
E, F: Ext B A
Ext B A
    strip_truncations.H: Univalence
B, A: AbGroup
F, E: AbSES B A
Ext B A
    exact (tr (abses_baer_sum E F)).
  -H: Univalence
B, A: AbGroup
MonUnit (Ext B A) exact (point (Ext B A)).
  -H: Univalence
B, A: AbGroup
Inverse (Ext B A) unfold Inverse.H: Univalence
B, A: AbGroup
Ext B A -> Ext B A
    exact (Trunc_functor _ (abses_pullback (- grp_homo_id))).
  -H: Univalence
B, A: AbGroup
IsGroup (Ext B A) repeat split.H: Univalence
B, A: AbGroup
IsHSet (Ext B A)
H: Univalence
B, A: AbGroup
Associative sg_op
H: Univalence
B, A: AbGroup
LeftIdentity sg_op 0
H: Univalence
B, A: AbGroup
RightIdentity sg_op 0
H: Univalence
B, A: AbGroup
LeftInverse sg_op inv 0
H: Univalence
B, A: AbGroup
RightInverse sg_op inv 0
    1: apply istrunc_truncation.H: Univalence
B, A: AbGroup
Associative sg_op
H: Univalence
B, A: AbGroup
LeftIdentity sg_op 0
H: Univalence
B, A: AbGroup
RightIdentity sg_op 0
H: Univalence
B, A: AbGroup
LeftInverse sg_op inv 0
H: Univalence
B, A: AbGroup
RightInverse sg_op inv 0
    all: intro E.H: Univalence
B, A: AbGroup
E: Ext B A
forall y z : Ext B A, E + (y + z) = E + y + z
H: Univalence
B, A: AbGroup
E: Ext B A
0 + E = E
H: Univalence
B, A: AbGroup
E: Ext B A
E + 0 = E
H: Univalence
B, A: AbGroup
E: Ext B A
- E + E = 0
H: Univalence
B, A: AbGroup
E: Ext B A
E - E = 0  1: intros F G.H: Univalence
B, A: AbGroup
E, F, G: Ext B A
E + (F + G) = E + F + G
H: Univalence
B, A: AbGroup
E: Ext B A
0 + E = E
H: Univalence
B, A: AbGroup
E: Ext B A
E + 0 = E
H: Univalence
B, A: AbGroup
E: Ext B A
- E + E = 0
H: Univalence
B, A: AbGroup
E: Ext B A
E - E = 0
    all: strip_truncations; unfold mon_unit, point; apply (ap tr).H: Univalence
B, A: AbGroup
G, F, E: AbSES B A
abses_baer_sum E (abses_baer_sum F G) =
abses_baer_sum (abses_baer_sum E F) G
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (point (AbSES B A)) E = E
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback (- grp_homo_id) E) E =
point (AbSES B A)
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) =
point (AbSES B A)
    +H: Univalence
B, A: AbGroup
G, F, E: AbSES B A
abses_baer_sum E (abses_baer_sum F G) =
abses_baer_sum (abses_baer_sum E F) G symmetry; apply baer_sum_associative.
    +H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (point (AbSES B A)) E = E apply baer_sum_unit_l.
    +H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E apply baer_sum_unit_r.
    +H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback (- grp_homo_id) E) E =
point (AbSES B A) apply baer_sum_inverse_r.
    +H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) =
point (AbSES B A) 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}.H: Univalence
B: AbGroup^op
A: AbGroup
AbGroup
Proof.H: Univalence
B: AbGroup^op
A: AbGroup
AbGroup
  snapply (Build_AbGroup (grp_ext@{u v} B A)).H: Univalence
B: AbGroup^op
A: AbGroup
Commutative sg_op
  intros E F.H: Univalence
B: AbGroup^op
A: AbGroup
E, F: grp_ext B A
E + F = F + E
  strip_truncations; cbn.H: Univalence
B: AbGroup^op
A: AbGroup
F, E: AbSES B A
tr (abses_baer_sum E F) = tr (abses_baer_sum F E)
  apply ap.H: Univalence
B: AbGroup^op
A: AbGroup
F, E: AbSES B A
abses_baer_sum E F = abses_baer_sum F E
  apply baer_sum_commutative.
Defined.

Instance is0functor_abext01 `{Univalence} (B : AbGroup^op)
  : Is0Functor (ab_ext B).H: Univalence
B: AbGroup^op
Is0Functor (ab_ext B)
Proof.H: Univalence
B: AbGroup^op
Is0Functor (ab_ext B)
  srapply Build_Is0Functor; intros ? ? f.H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
ab_ext B a $-> ab_ext B b
  snapply Build_GroupHomomorphism.H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
ab_ext B a -> ab_ext B b
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fmap (Ext B) f).H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
IsSemiGroupPreserving (fmap (pTr 0 o AbSES B) f)
  rapply Trunc_ind; intro E0.H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0: AbSES B a
forall y : ab_ext B a,
fmap (pTr 0 o AbSES B) f (tr E0 + y) =
fmap (pTr 0 o AbSES B) f (tr E0) +
fmap (pTr 0 o AbSES B) f y
  rapply Trunc_ind; intro E1.H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0, E1: AbSES B a
fmap (pTr 0 o AbSES B) f (tr E0 + tr E1) =
fmap (pTr 0 o AbSES B) f (tr E0) +
fmap (pTr 0 o AbSES B) f (tr E1)
  apply (ap tr); cbn.H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0, E1: AbSES B a
abses_pushout f (abses_baer_sum E0 E1) =
abses_baer_sum (abses_pushout f E0)
  (abses_pushout f E1)
  apply baer_sum_pushout.
Defined.

Instance is0functor_abext10 `{Univalence} (A : AbGroup)
  : Is0Functor (fun B : AbGroup^op => ab_ext B A).H: Univalence
A: AbGroup
Is0Functor (fun B : AbGroup^op => ab_ext B A)
Proof.H: Univalence
A: AbGroup
Is0Functor (fun B : AbGroup^op => ab_ext B A)
  srapply Build_Is0Functor; intros ? ? f; cbn.H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
GroupHomomorphism (grp_ext a A) (grp_ext b A)
  snapply Build_GroupHomomorphism.H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
grp_ext a A -> grp_ext b A
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fmap (fun (B : AbGroup^op) => Ext B A) f).H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
IsSemiGroupPreserving
  (fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f)
  rapply Trunc_ind; intro E0.H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0: AbSES a A
forall y : grp_ext a A,
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f
  (tr E0 + y) =
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f
  (tr E0) +
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f y
  rapply Trunc_ind; intro E1.H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0, E1: AbSES a A
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f
  (tr E0 + tr E1) =
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f
  (tr E0) +
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f
  (tr E1)
  apply (ap tr); cbn.H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0, E1: AbSES a A
abses_pullback f (abses_baer_sum E0 E1) =
abses_baer_sum (abses_pullback f E0)
  (abses_pullback f E1)
  apply baer_sum_pullback.
Defined.

Instance is1functor_abext01 `{Univalence} (B : AbGroup^op)
  : Is1Functor (ab_ext B).H: Univalence
B: AbGroup^op
Is1Functor (ab_ext B)
Proof.H: Univalence
B: AbGroup^op
Is1Functor (ab_ext B)
  snapply Build_Is1Functor.H: Univalence
B: AbGroup^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g
H: Univalence
B: AbGroup^op
forall a : AbGroup,
fmap (ab_ext B) (Id a) $== Id (ab_ext B a)
H: Univalence
B: AbGroup^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_ext B) (g $o f) $==
fmap (ab_ext B) g $o fmap (ab_ext B) f
  -H: Univalence
B: AbGroup^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g intros A C f g.H: Univalence
B: AbGroup^op
A, C: AbGroup
f, g: A $-> C
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g
    exact (fmap2 (Ext B)).
  -H: Univalence
B: AbGroup^op
forall a : AbGroup,
fmap (ab_ext B) (Id a) $== Id (ab_ext B a) exact (fmap_id (Ext B)).
  -H: Univalence
B: AbGroup^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_ext B) (g $o f) $==
fmap (ab_ext B) g $o fmap (ab_ext B) f intros A C D.H: Univalence
B: AbGroup^op
A, C, D: AbGroup
forall (f : A $-> C) (g : C $-> D),
fmap (ab_ext B) (g $o f) $==
fmap (ab_ext B) g $o fmap (ab_ext B) f
    exact (fmap_comp (Ext B)).
Defined.

Instance is1functor_abext10 `{Univalence} (A : AbGroup)
  : Is1Functor (fun B : AbGroup^op => ab_ext B A).H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => ab_ext B A)
Proof.H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => ab_ext B A)
  snapply Build_Is1Functor.H: Univalence
A: AbGroup
forall (a b : AbGroup^op) (f g : a $-> b),
f $== g ->
fmap (fun B : AbGroup^op => ab_ext B A) f $==
fmap (fun B : AbGroup^op => ab_ext B A) g
H: Univalence
A: AbGroup
forall a : AbGroup^op,
fmap (fun B : AbGroup^op => ab_ext B A) (Id a) $==
Id ((fun B : AbGroup^op => ab_ext B A) a)
H: Univalence
A: AbGroup
forall (a b c : AbGroup^op) (f : a $-> b)
(g : b $-> c),
fmap (fun B : AbGroup^op => ab_ext B A) (g $o f) $==
fmap (fun B : AbGroup^op => ab_ext B A) g $o
fmap (fun B : AbGroup^op => ab_ext B A) f
  -H: Univalence
A: AbGroup
forall (a b : AbGroup^op) (f g : a $-> b),
f $== g ->
fmap (fun B : AbGroup^op => ab_ext B A) f $==
fmap (fun B : AbGroup^op => ab_ext B A) g intros B C f g.H: Univalence
A: AbGroup
B, C: AbGroup^op
f, g: B $-> C
f $== g ->
fmap (fun B : AbGroup^op => ab_ext B A) f $==
fmap (fun B : AbGroup^op => ab_ext B A) g
    exact (fmap2 (fun B : AbGroup^op => Ext B A)).
  -H: Univalence
A: AbGroup
forall a : AbGroup^op,
fmap (fun B : AbGroup^op => ab_ext B A) (Id a) $==
Id ((fun B : AbGroup^op => ab_ext B A) a) exact (fmap_id (fun B : AbGroup^op => Ext B A)).
  -H: Univalence
A: AbGroup
forall (a b c : AbGroup^op) (f : a $-> b)
(g : b $-> c),
fmap (fun B : AbGroup^op => ab_ext B A) (g $o f) $==
fmap (fun B : AbGroup^op => ab_ext B A) g $o
fmap (fun B : AbGroup^op => ab_ext B A) f intros B C D.H: Univalence
A: AbGroup
B, C, D: AbGroup^op
forall (f : B $-> C) (g : C $-> D),
fmap (fun B : AbGroup^op => ab_ext B A) (g $o f) $==
fmap (fun B : AbGroup^op => ab_ext B A) g $o
fmap (fun B : AbGroup^op => ab_ext B A) f
    exact (fmap_comp (fun B : AbGroup^op => Ext B A)).
Defined.

Instance is0bifunctor_abext `{Univalence}
  : Is0Bifunctor (A:=AbGroup^op) ab_ext
  := Build_Is0Bifunctor'' _.

Instance is1bifunctor_abext `{Univalence}
  : Is1Bifunctor (A:=AbGroup^op) ab_ext.H: Univalence
Is1Bifunctor ab_ext
Proof.H: Univalence
Is1Bifunctor ab_ext
  snapply Build_Is1Bifunctor''.H: Univalence
forall a : AbGroup^op, Is1Functor (ab_ext a)
H: Univalence
forall b : AbGroup, Is1Functor (flip ab_ext b)
H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_ext a1 g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext a0 g
  1,2: exact _.H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_ext a1 g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext a0 g
  intros A B.H: Univalence
A, B: AbGroup^op
forall (f : A $-> B) (b0 b1 : AbGroup)
(g : b0 $-> b1),
fmap01 ab_ext B g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext A g
  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).H: Univalence
B, A, G: AbGroup
E: AbSES B A
GroupHomomorphism (ab_hom A G) (ab_ext B G)
Proof.H: Univalence
B, A, G: AbGroup
E: AbSES B A
GroupHomomorphism (ab_hom A G) (ab_ext B G)
  snapply Build_GroupHomomorphism.H: Univalence
B, A, G: AbGroup
E: AbSES B A
ab_hom A G -> ab_ext B G
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsSemiGroupPreserving
  (fun f : ab_hom A G => fmap01 Ext' B f (tr E))
  intros f g; cbn.H: Univalence
B, A, G: AbGroup
E: AbSES B A
f, g: ab_hom A G
tr (abses_pushout (sgop_hom f g) E) =
tr
  (abses_baer_sum (abses_pushout f E)
     (abses_pushout g E))
  napply (ap tr).H: Univalence
B, A, G: AbGroup
E: AbSES B A
f, g: ab_hom A G
abses_pushout (sgop_hom f g) E =
abses_baer_sum (abses_pushout f E) (abses_pushout g E)
  exact (baer_sum_distributive_pushouts f g).
Defined.

(** ** 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).H: Univalence
P: AbGroup
H0: IsAbProjective P
forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
Proof.H: Univalence
P: AbGroup
H0: IsAbProjective P
forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
  intros A E.H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
tr E = point (Ext P A)
  apply iff_ab_ext_trivial_split.H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
merely
  {s : GroupHomomorphism P E &
  projection E $o s == idmap}
  exact (fst (iff_isabprojective_surjections_split P) _ _ _ _).
Defined.

(** It follows that when [P] is projective, [Ext P A] is contractible. *)
Instance contr_abext_projective `{Univalence}
  (P : AbGroup) `{IsAbProjective P} {A : AbGroup}
  : Contr (Ext P A).H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
Contr (Ext P A)
Proof.H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
Contr (Ext P A)
  apply (Build_Contr _ (point _)); intro E.H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: Ext P A
point (Ext P A) = E
  strip_truncations.H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
point (Ext P A) = tr E
  symmetry; by apply abext_trivial_projective.
Defined.

(* Conversely, 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.H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
IsAbProjective P
Proof.H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
IsAbProjective P
  apply iff_isabprojective_surjections_split.H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
forall (A : AbGroup) (p : A $-> P),
ReflectiveSubuniverse.IsConnMap (Tr (-1)) p ->
merely {s : P $-> A & p $o s == grp_homo_id}
  intros E p issurj_p.H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
E: AbGroup
p: E $-> P
issurj_p: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
merely {s : P $-> E & p $o s == grp_homo_id}
  apply (iff_ab_ext_trivial_split (abses_from_surjection p))^-1.H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A),
tr E = point (Ext P A)
E: AbGroup
p: E $-> P
issurj_p: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
tr (abses_from_surjection p) =
point (Ext P (ab_kernel p))
  apply ext_triv.
Defined.