# Some general constructions

## Contensts

• Pair of morphisms
• Short exact sequence data

# Pair of morphisms

Section def_morphismpair.

Context {C : precategory}.

## Morphism

Definition Morphism : UU := (a b : C), a --> b.

Definition make_Morphism {a b : C} (f : a --> b) : Morphism := (a,,(b,,f)).

Definition Source (M : Morphism) : ob C := pr1 M.

Definition Target (M : Morphism) : ob C := pr1 (pr2 M).

Definition MorphismMor (M : Morphism) : CSource M, Target M := pr2 (pr2 M).
Coercion MorphismMor : Morphism >-> precategory_morphisms.

## MorphismPair

Definition MorphismPair : UU := (a b c : C), (a --> b × b --> c).

Definition make_MorphismPair {a b c : C} (f : a --> b) (g : b --> c) : MorphismPair.
Proof.
use tpair.
- exact a.
- use tpair.
+ exact b.
+ use tpair.
× exact c.
× use make_dirprod.
-- exact f.
-- exact g.
Defined.

Accessor function
Definition Ob1 (MP : MorphismPair) : ob C := pr1 MP.

Definition Ob2 (MP : MorphismPair) : ob C := pr1 (pr2 MP).

Definition Ob3 (MP : MorphismPair) : ob C := pr1 (pr2 (pr2 MP)).

Definition Mor1 (MP : MorphismPair) : COb1 MP, Ob2 MP := dirprod_pr1 (pr2 (pr2 (pr2 MP))).

Definition Mor2 (MP : MorphismPair) : COb2 MP, Ob3 MP := dirprod_pr2 (pr2 (pr2 (pr2 MP))).

Morphism of morphism pairs
Definition MPMorMors (MP1 MP2 : MorphismPair) : UU :=
(Ob1 MP1 --> Ob1 MP2) × (Ob2 MP1 --> Ob2 MP2) × (Ob3 MP1 --> Ob3 MP2).

Definition make_MPMorMors {MP1 MP2 : MorphismPair} (f1 : Ob1 MP1 --> Ob1 MP2)
(f2 : Ob2 MP1 --> Ob2 MP2) (f3 : Ob3 MP1 --> Ob3 MP2) : MPMorMors MP1 MP2 :=
(f1,,(f2,,f3)).

Definition MPMor1 {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2) : Ob1 MP1 --> Ob1 MP2 :=
dirprod_pr1 MPM.

Definition MPMor2 {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2) : Ob2 MP1 --> Ob2 MP2 :=
dirprod_pr1 (dirprod_pr2 MPM).

Definition MPMor3 {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2) : Ob3 MP1 --> Ob3 MP2 :=
dirprod_pr2 (dirprod_pr2 MPM).

Definition MPMorComms {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2) : UU :=
(MPMor1 MPM · Mor1 MP2 = Mor1 MP1 · MPMor2 MPM)
× (MPMor2 MPM · Mor2 MP2 = Mor2 MP1 · MPMor3 MPM).

Definition make_MPMorComms {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2)
(H1 : MPMor1 MPM · Mor1 MP2 = Mor1 MP1 · MPMor2 MPM)
(H2 : MPMor2 MPM · Mor2 MP2 = Mor2 MP1 · MPMor3 MPM) : MPMorComms MPM := (H1,,H2).

Definition MPComm1 {MP1 MP2 : MorphismPair} {MPM : MPMorMors MP1 MP2} (MPMC : MPMorComms MPM) :
MPMor1 MPM · Mor1 MP2 = Mor1 MP1 · MPMor2 MPM := dirprod_pr1 MPMC.

Definition MPComm2 {MP1 MP2 : MorphismPair} {MPM : MPMorMors MP1 MP2} (MPMC : MPMorComms MPM) :
MPMor2 MPM · Mor2 MP2 = Mor2 MP1 · MPMor3 MPM := dirprod_pr2 MPMC.

Definition MPMor (MP1 MP2 : MorphismPair) : UU := MPM : MPMorMors MP1 MP2, MPMorComms MPM.

Definition make_MPMor {MP1 MP2 : MorphismPair} (MPM : MPMorMors MP1 MP2) (MPMC : MPMorComms MPM) :
MPMor MP1 MP2 := (MPM,,MPMC).

Definition MPMor_MPMorMors {MP1 MP2 : MorphismPair} (MPM : MPMor MP1 MP2) :
MPMorMors MP1 MP2 := pr1 MPM.
Coercion MPMor_MPMorMors : MPMor >-> MPMorMors.

Definition MPMor_MPMorComms {MP1 MP2 : MorphismPair} (MPM : MPMor MP1 MP2) :
MPMorComms MPM := pr2 MPM.
Coercion MPMor_MPMorComms : MPMor >-> MPMorComms.

Lemma reverseCommIsoSquare {M : precategory} {P Q P' Q':M} (f:P'-->P) (g:Q'-->Q) (i:z_iso P' Q') (j:z_iso P Q) :
i · g = f · j z_iso_inv i · f = g · z_iso_inv j.
Proof.
intros l.
refine (! id_right _ @ _).
refine (maponpaths _ (! is_inverse_in_precat1 (z_iso_is_inverse_in_precat j)) @ _).
refine (! assoc (z_iso_inv i) _ _ @ _).
refine (maponpaths _ (assoc f _ _) @ _).
refine (maponpaths (precomp_with (z_iso_inv i)) (maponpaths (postcomp_with (z_iso_inv_mor j)) (!l)) @ _);
unfold precomp_with, postcomp_with.
refine (maponpaths _ (! assoc _ _ _) @ _).
refine (assoc _ _ _ @ _).
refine (maponpaths (postcomp_with (g · z_iso_inv_mor j)) (is_inverse_in_precat2 (z_iso_is_inverse_in_precat i)) @ _);
unfold postcomp_with.
exact (id_left _).
Qed.
Lemma reverseCommIsoSquare' {M : precategory} {P Q P' Q':M} (f:P'-->P) (g:Q'-->Q) (i:z_iso P' Q') (j:z_iso P Q) :
f · j = i · g g · z_iso_inv j = z_iso_inv i · f.
Proof.
intros l. refine (! _). apply reverseCommIsoSquare. refine (! _). exact l.
Qed.
Definition MorphismPairMap (P Q : MorphismPair) :=
(f : Ob1 P --> Ob1 Q) (g : Ob2 P --> Ob2 Q) (h : Ob3 P --> Ob3 Q),
f · Mor1 Q = Mor1 P · g × g · Mor2 Q = Mor2 P · h.
Definition Map1 {P Q : MorphismPair} (f : MorphismPairMap P Q) : Ob1 P --> Ob1 Q := pr1 f.
Definition Map2 {P Q : MorphismPair} (f : MorphismPairMap P Q) : Ob2 P --> Ob2 Q := pr1 (pr2 f).
Definition Map3 {P Q : MorphismPair} (f : MorphismPairMap P Q) : Ob3 P --> Ob3 Q := pr1 (pr2 (pr2 f)).
Definition MorphismPairIsomorphism (P Q : MorphismPair) :=
(f : z_iso (Ob1 P) (Ob1 Q)) (g : z_iso (Ob2 P) (Ob2 Q)) (h : z_iso (Ob3 P) (Ob3 Q)),
( f · Mor1 Q = Mor1 P · g
×
Mor1 P · g = f · Mor1 Q )
×
( g · Mor2 Q = Mor2 P · h
×
Mor2 P · h = g · Mor2 Q ).
Definition InverseMorphismPairIsomorphism {P Q : MorphismPair} :
MorphismPairIsomorphism P Q MorphismPairIsomorphism Q P.
Proof.
intros f.
(z_iso_inv (pr1 f)). (z_iso_inv (pr12 f)). (z_iso_inv (pr122 f)).
split.
- split.
+ apply reverseCommIsoSquare. exact (pr11 (pr222 f)).
+ apply reverseCommIsoSquare'. exact (pr21 (pr222 f)).
- split.
+ apply reverseCommIsoSquare. exact (pr12 (pr222 f)).
+ apply reverseCommIsoSquare'. exact (pr22 (pr222 f)).
Defined.
Definition make_MorphismPairIsomorphism
(P Q : MorphismPair)
(f : z_iso (Ob1 P) (Ob1 Q))
(g : z_iso (Ob2 P) (Ob2 Q))
(h : z_iso (Ob3 P) (Ob3 Q)) :
f · Mor1 Q = Mor1 P · g
g · Mor2 Q = Mor2 P · h MorphismPairIsomorphism P Q
:= λ r s, (f,,g,,h,,(r,,!r),,(s,,!s)).
End def_morphismpair.
Arguments MorphismPair : clear implicits.

# MorphismPair and opposite categories

Section MorphismPair_opp.

Definition MorphismPair_opp {C : precategory} (MP : @MorphismPair C) :
@MorphismPair (opp_precat C).
Proof.
use make_MorphismPair.
- exact (Ob3 MP).
- exact (Ob2 MP).
- exact (Ob1 MP).
- exact (Mor2 MP).
- exact (Mor1 MP).
Defined.

Definition opp_MorphismPair {C : precategory} (MP : @MorphismPair (opp_precat C)) :
@MorphismPair C.
Proof.
exact (MorphismPair_opp MP).
Defined.

Definition applyFunctorToPair {M N:precategory} :
(MN) @MorphismPair M @MorphismPair N
:= λ F P, make_MorphismPair (# F (Mor1 P)) (# F (Mor2 P)).
Definition applyFunctorToPairIsomorphism {M N:precategory}
(F : MN) (P Q : @MorphismPair M) :
MorphismPairIsomorphism P Q
MorphismPairIsomorphism (applyFunctorToPair F P) (applyFunctorToPair F Q).
Proof.
intros [i1 [i2 [i3 [[d d'][e e']]]]].
(functor_on_z_iso F i1).
(functor_on_z_iso F i2).
(functor_on_z_iso F i3).
repeat split.
- refine (! _ @ (maponpaths (# F) d ) @ _);apply functor_comp.
- refine (! _ @ (maponpaths (# F) d') @ _);apply functor_comp.
- refine (! _ @ (maponpaths (# F) e ) @ _);apply functor_comp.
- refine (! _ @ (maponpaths (# F) e') @ _);apply functor_comp.
Defined.
Definition opp_MorphismPairIsomorphism {M:precategory} {P Q: @MorphismPair M} :
MorphismPairIsomorphism P Q MorphismPairIsomorphism (MorphismPair_opp Q) (MorphismPair_opp P)
:= λ f, opp_z_iso (pr122 f),,
opp_z_iso (pr12 f),,
opp_z_iso (pr1 f),,
(pr22 (pr222 f),,pr12 (pr222 f)),,
(pr21 (pr222 f),,pr11 (pr222 f)).

End MorphismPair_opp.

# ShortShortExactData

Section def_shortshortexactdata.

Variable C : precategory.
Hypothesis hs : has_homsets C.
Variable Z : Zero C.

## Data for ShortShortExact

A pair of morphism such that composition of the morphisms is the zero morphism.

Definition ShortShortExactData : UU :=
MP : MorphismPair C, Mor1 MP · Mor2 MP = ZeroArrow Z _ _.

Definition make_ShortShortExactData (MP : MorphismPair C)
(H : Mor1 MP · Mor2 MP = ZeroArrow Z _ _) : ShortShortExactData := tpair _ MP H.

Accessor functions

# ShortShortExactData and opposite categories

Section shortshortexactdata_opp.

Lemma opp_ShortShortExactData_Eq {C : precategory} {Z : Zero C}
(SSED : ShortShortExactData (opp_precat C) (Zero_opp C Z)) :
Mor1 (opp_MorphismPair SSED) · Mor2 (opp_MorphismPair SSED) =
ZeroArrow Z (Ob1 (opp_MorphismPair SSED)) (Ob3 (opp_MorphismPair SSED)).
Proof.
use (pathscomp0 (@ShortShortExactData_Eq (opp_precat C) (Zero_opp C Z) SSED)).
rewrite <- ZeroArrow_opp. apply idpath.
Qed.

Definition opp_ShortShortExactData {C : precategory} {Z : Zero C}
(SSED : ShortShortExactData (opp_precat C) (Zero_opp C Z)) : ShortShortExactData C Z.
Proof.
use make_ShortShortExactData.
- exact (opp_MorphismPair SSED).
- exact (opp_ShortShortExactData_Eq SSED).
Defined.

Lemma ShortShortExactData_opp_Eq {C : precategory} {Z : Zero C}
(SSED : ShortShortExactData C Z) :
Mor1 (MorphismPair_opp SSED) · Mor2 (MorphismPair_opp SSED) =
ZeroArrow (Zero_opp C Z) (Ob1 (MorphismPair_opp SSED)) (Ob3 (MorphismPair_opp SSED)).
Proof.
use (pathscomp0 (@ShortShortExactData_Eq C Z SSED)).
rewrite <- ZeroArrow_opp. apply idpath.
Qed.

Definition ShortShortExactData_opp {C : precategory} {Z : Zero C}
(SSED : ShortShortExactData C Z) : ShortShortExactData (opp_precat C) (Zero_opp C Z).
Proof.
use make_ShortShortExactData.
- exact (MorphismPair_opp SSED).
- exact (ShortShortExactData_opp_Eq SSED).
Defined.

End shortshortexactdata_opp.