From HoTT Require Import Basics Types AbelianGroup AbPullbackFrom HoTT Require Import Basics Types AbelianGroup AbPullback
  WildCat.Core Limits.Pullback ReflectiveSubuniverse Truncations.Core.

(** * Projective abelian groups *)

(** We define projective abelian groups and show that [P] is projective if and only if every epimorphism [A -> P] merely splits. *)

(** An abelian group [P] is projective if for any map [P -> B] and epimorphism [A -> B], there merely exists a lift [P -> A] making the following triangle commute:

              A
            ^ |
         l /  |
              | e
         /    |
              V
       P ---> B
          f
*)
Class IsAbProjective@{u +} (P : AbGroup@{u}) : Type :=
  isabprojective : forall (A B : AbGroup@{u}), forall (e : A $-> B),
    forall (f : P $-> B), IsSurjection e -> merely (exists l : P $-> A, e $o l == f).

(** An abelian group is projective iff epis into it merely split. *)
Proposition iff_isabprojective_surjections_split (P : AbGroup)
  : IsAbProjective P
    <-> (forall A, forall p : A $-> P, IsSurjection p ->
                           merely (exists s : P $-> A, p $o s == grp_homo_id)).
P: AbGroup
IsAbProjective P <->
(forall (A : AbGroup) (p : A $-> P),
 IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id})
Proof.
P: AbGroup
IsAbProjective P <->
(forall (A : AbGroup) (p : A $-> P),
 IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id})
  split.
P: AbGroup
IsAbProjective P ->
forall (A : AbGroup) (p : A $-> P),
IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id}
P: AbGroup
(forall (A : AbGroup) (p : A $-> P),
 IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id}) ->
IsAbProjective P
  -
P: AbGroup
IsAbProjective P ->
forall (A : AbGroup) (p : A $-> P),
IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id} intros H A B.
P: AbGroup
H: IsAbProjective P
A: AbGroup
B: A $-> P
IsConnMap (Tr (-1)) B -> merely {s : P $-> A & B $o s == grp_homo_id}
    apply H.
  -
P: AbGroup
(forall (A : AbGroup) (p : A $-> P),
 IsConnMap (Tr (-1)) p -> merely {s : P $-> A & p $o s == grp_homo_id}) ->
IsAbProjective P intros H A B e f H1.
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s : P $-> A0 & p $o s == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
merely {l : P $-> A & e $o l == f}
    pose proof (s := H (ab_pullback f e) (grp_pullback_pr1 f e)
                       (conn_map_pullback _ f e)).
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s0 : P $-> A0 & p $o s0 == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
s: merely
  {s0 : P $-> ab_pullback f e & grp_pullback_pr1 f e $o s0 == grp_homo_id}
merely {l : P $-> A & e $o l == f}
    strip_truncations.
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s0 : P $-> A0 & p $o s0 == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
s: {s0 : P $-> ab_pullback f e & grp_pullback_pr1 f e $o s0 == grp_homo_id}
merely {l : P $-> A & e $o l == f}
    destruct s as [s h].
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s0 : P $-> A0 & p $o s0 == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
s: P $-> ab_pullback f e
h: grp_pullback_pr1 f e $o s == grp_homo_id
merely {l : P $-> A & e $o l == f}
    refine (tr ((grp_pullback_pr2 f e) $o s; _)); intro x.
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s0 : P $-> A0 & p $o s0 == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
s: P $-> ab_pullback f e
h: grp_pullback_pr1 f e $o s == grp_homo_id
x: P
(e $o (grp_pullback_pr2 f e $o s)) x = f x
    refine ((pullback_commsq f e _)^ @ _).
P: AbGroup
H: forall (A0 : AbGroup) (p : A0 $-> P),
IsConnMap (Tr (-1)) p -> merely {s0 : P $-> A0 & p $o s0 == grp_homo_id}
A, B: AbGroup
e: A $-> B
f: P $-> B
H1: IsConnMap (Tr (-1)) e
s: P $-> ab_pullback f e
h: grp_pullback_pr1 f e $o s == grp_homo_id
x: P
f (pullback_pr1 (s x)) = f x
    exact (ap f (h x)).
Defined.