(** * Some general constructions *) (** ** Contensts - Pair of morphisms - Short exact sequence data *) Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Local Open Scope cat. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp. (** * 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) : C⟦Source 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) : C⟦Ob1 MP, Ob2 MP⟧ := dirprod_pr1 (pr2 (pr2 (pr2 MP))). Definition Mor2 (MP : MorphismPair) : C⟦Ob2 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 (inv_from_z_iso j)) (!l)) @ _); unfold precomp_with, postcomp_with. refine (maponpaths _ (! assoc _ _ _) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (postcomp_with (g · inv_from_z_iso 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. exists (z_iso_inv (pr1 f)). exists (z_iso_inv (pr12 f)). exists (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} : (M⟶N) -> @MorphismPair M -> @MorphismPair N := λ F P, make_MorphismPair (# F (Mor1 P)) (# F (Mor2 P)). Definition applyFunctorToPairIsomorphism {M N:precategory} (F : M⟶N) (P Q : @MorphismPair M) : MorphismPairIsomorphism P Q -> MorphismPairIsomorphism (applyFunctorToPair F P) (applyFunctorToPair F Q). Proof. intros [i1 [i2 [i3 [[d d'][e e']]]]]. exists (functor_on_z_iso F i1). exists (functor_on_z_iso F i2). exists (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 : category. Let hs : has_homsets C := homset_property 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 *) Definition ShortShortExactData_MorphismPair (SSED : ShortShortExactData) : MorphismPair C := pr1 SSED. Coercion ShortShortExactData_MorphismPair : ShortShortExactData >-> MorphismPair. Definition ShortShortExactData_Eq (SSED : ShortShortExactData) : (Mor1 SSED) · (Mor2 SSED) = ZeroArrow Z _ _ := pr2 SSED. End def_shortshortexactdata. Arguments make_ShortShortExactData [C] _ _ _. Arguments ShortShortExactData_Eq [C] _ _. (** * ShortShortExactData and opposite categories *) Section shortshortexactdata_opp. Lemma opp_ShortShortExactData_Eq {C : category} {Z : Zero C} (SSED : ShortShortExactData (op_category 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 (op_category C) (Zero_opp C Z) SSED)). rewrite <- ZeroArrow_opp. apply idpath. Qed. Definition opp_ShortShortExactData {C : category} {Z : Zero C} (SSED : ShortShortExactData (op_category 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 : category} {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 : category} {Z : Zero C} (SSED : ShortShortExactData C Z) : ShortShortExactData (op_category C) (Zero_opp C Z). Proof. use make_ShortShortExactData. - exact (MorphismPair_opp SSED). - exact (ShortShortExactData_opp_Eq SSED). Defined. End shortshortexactdata_opp.