Library UniMath.CategoryTheory.ExactCategories.ExactCategories
Exact categories
Contents
- Preliminaries
- Diagram chasing lemmas
- Diagram chasing lemmas
- The definition of exact category
- Equivalence with Quillen's definition
- The exact category structure induced on X by a function X -> ob M, where M is an exact category.
Require Export UniMath.Foundations.All.
Require Export UniMath.MoreFoundations.Notations.
Require Export UniMath.MoreFoundations.PartA.
Require Export UniMath.Algebra.BinaryOperations.
Require Export UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Export UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Export UniMath.CategoryTheory.Core.Functors.
Require Export UniMath.CategoryTheory.Core.NaturalTransformations.
Require Export UniMath.CategoryTheory.Monics.
Require Export UniMath.CategoryTheory.Epis.
Require Export UniMath.CategoryTheory.limits.zero.
Require Export UniMath.CategoryTheory.limits.kernels.
Require Export UniMath.CategoryTheory.limits.cokernels.
Require Export UniMath.CategoryTheory.limits.binproducts.
Require Export UniMath.CategoryTheory.limits.bincoproducts.
Require Export UniMath.CategoryTheory.limits.pullbacks.
Require Export UniMath.CategoryTheory.limits.pushouts.
Require Export UniMath.CategoryTheory.limits.BinDirectSums.
Require Export UniMath.CategoryTheory.limits.Opp.
Require Export UniMath.CategoryTheory.CategoriesWithBinOps.
Require Export UniMath.CategoryTheory.opp_precat.
Require Export UniMath.CategoryTheory.PrecategoriesWithAbgrops.
Require Export UniMath.CategoryTheory.PreAdditive.
Require Export UniMath.CategoryTheory.Morphisms.
Require Export UniMath.CategoryTheory.Additive.
Require Export UniMath.CategoryTheory.Subcategory.Full.
Require Export UniMath.MoreFoundations.Propositions.
Local Arguments grinv {_}.
Local Open Scope logic.
Local Open Scope cat.
Local Definition hom (C:precategory_data) : ob C → ob C → UU := λ c c', precategory_morphisms c c'.
Local Definition Hom (C : category) : ob C → ob C → hSet := λ c c', make_hSet _ (homset_property C c c').
Local Definition Hom_add (C : PreAdditive) : ob C → ob C → abgr := λ c c', (@to_abgr C c c').
Section InvestigateNotations.
Context (M : PreAdditive) (x y z:M) (f g : hom M x y) (h k : Hom_add M y z).
Local Open Scope abgrcat.
Goal empty.
set (Q := h+k).
set (r := -g).
set (t := f-g).
set (p := f·h + (h∘f) · 1).
set (o := (h + h) · 1 = h).
set (s := f+g).
set (u := f·1).
set (v := f·0·h).
Abort.
End InvestigateNotations.
Section Categories.
Definition isPushout' {M:category} {a b c d : M} (f : a --> b) (g : a --> c)
(in1 : b --> d) (in2 : c --> d) : hProp.
Proof.
∃ (∑ (H : f · in1 = g · in2), isPushout f g in1 in2 H).
abstract (
apply isaproptotal2 ;
[ intros H; apply isaprop_isPushout
| intros H H' po po'; apply homset_property ]) using _P_.
Defined.
Definition isPullback' {M:category} {a b c d : M} (f : b --> a) (g : c --> a)
(p1 : d --> b) (p2 : d --> c) : hProp.
Proof.
∃ (∑ (H : p1 · f = p2· g), isPullback f g p1 p2 H).
exact (_P_ (oppositeCategory M) a b c d f g p1 p2).
Defined.
Lemma isPullback'_up_to_z_iso {M:category} {a b c d d' : M}
(f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c)
(i : z_iso d' d) :
isPullback' f g p1 p2 → isPullback' f g (i·p1) (i·p2).
Proof.
intros [e pb]. use tpair.
- abstract (rewrite 2 assoc'; apply maponpaths; exact e) using _P_.
- cbn beta. intros T r s eq.
assert (Q := pb T r s eq).
use (iscontrweqf _ Q); clear Q.
use weqtotal2.
{ apply z_iso_comp_left_weq. exact (z_iso_inv i). }
{ intros h. cbn beta. apply weqiff.
{ cbn.
rewrite 2 (assoc' h). rewrite 2 (assoc _ i).
rewrite z_iso_after_z_iso_inv. rewrite 2 id_left.
apply isrefl_logeq. }
{ apply isapropdirprod; apply homset_property. }
{ apply isapropdirprod; apply homset_property. }
}
Defined.
Lemma isPushout'_up_to_z_iso {M:category} {a b c d d' : M}
(f : a --> b) (g : a --> c) (in1 : b --> d) (in2 : c --> d)
(i : z_iso d d') :
isPushout' f g in1 in2 → isPushout' f g (i∘in1) (i∘in2).
Proof.
exact (isPullback'_up_to_z_iso (M:=oppositeCategory M) f g in1 in2 (opp_z_iso i)).
Qed.
Lemma Pushout_to_isPushout' {M:category} {a b c : M} (f : a --> b) (g : a --> c)
(po : Pushout f g) :
isPushout' f g (PushoutIn1 po) (PushoutIn2 po).
Proof.
use tpair.
- apply PushoutSqrCommutes.
- cbn beta. apply isPushout_Pushout.
Qed.
Lemma Pullback_to_isPullback' {M:category} {a b c : M} (f : b --> a) (g : c --> a)
(pb : Pullback f g) :
isPullback' f g (PullbackPr1 pb) (PullbackPr2 pb).
Proof.
use tpair.
- apply PullbackSqrCommutes.
- cbn beta. apply isPullback_Pullback.
Qed.
End Categories.
Section MorphismPairs.
Goal ∏ (M : precategory) (P Q : MorphismPair M) (f:MorphismPairIsomorphism P Q),
InverseMorphismPairIsomorphism (InverseMorphismPairIsomorphism f) = f.
Proof.
Fail reflexivity.
Abort.
End MorphismPairs.
Section Pullbacks. Definition IsoArrowTo {M : precategory} {A A' B:M} (g : A --> B) (g' : A' --> B) := ∑ i : z_iso A A', i · g' = g .
Coercion IsoArrowTo_pr1 {M : precategory} {A A' B:M} (g : A --> B) (g' : A' --> B) : IsoArrowTo g g' → z_iso A A' := pr1.
Definition IsoArrowFrom {M : precategory} {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i = g'.
Coercion IsoArrowFrom_pr1 {M : precategory} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' → z_iso B B' := pr1.
Definition IsoArrow {M : precategory} {A A' B B':M} (g : A --> B) (g' : A' --> B') := ∑ (i : z_iso A A') (j : z_iso B B'), i · g' = g · j.
Definition pullbackiso1 {M : precategory} {A B C:M} {f : A --> C} {g : B --> C}
(pb : Pullback f g) (pb' : Pullback f g)
: IsoArrowTo (PullbackPr1 pb) (PullbackPr1 pb')
:= pr1 (pullbackiso pb pb'),,pr12 (pullbackiso pb pb').
Definition pullbackiso2 {M : precategory} {A B C:M} {f : A --> C} {g : B --> C}
(pb : Pullback f g) (pb' : Pullback f g)
: IsoArrowTo (PullbackPr2 pb) (PullbackPr2 pb')
:= pr1 (pullbackiso pb pb'),,pr22 (pullbackiso pb pb').
Section OppositeIsoArrows.
Definition opposite_IsoArrowTo {M:precategory} {A A' B:M} {g : A --> B} {g' : A' --> B} :
IsoArrowTo g g' → IsoArrowFrom (M:=M^op) g' g.
Proof.
intros i.
Fail exact i.
use tpair.
- exact (opp_z_iso (pr1 i)).
- cbn. exact (pr2 i).
Defined.
Definition opposite_IsoArrowFrom {M:precategory} {A B B':M} {g : A --> B} {g' : A --> B'} :
IsoArrowFrom g g' → IsoArrowTo (M:=M^op) g' g.
Proof.
intros i. use tpair.
- exact (opp_z_iso (pr1 i)).
- cbn. exact (pr2 i).
Defined.
Definition opposite_IsoArrow {M:precategory} {A A' B B':M} (g : A --> B) (g' : A' --> B') :
IsoArrow g g' → IsoArrow (M:=M^op) (opp_mor g') (opp_mor g).
Proof.
intros i.
∃ (opp_z_iso (pr12 i)).
∃ (opp_z_iso (pr1 i)).
exact (! pr22 i).
Defined.
End OppositeIsoArrows.
Lemma IsoArrowTo_isaprop (M : category) {A A' B:M} (g : A --> B) (g' : A' --> B) :
isMonic g' → isaprop (IsoArrowTo g g').
Proof.
intros i. apply invproofirrelevance; intros k k'. apply subtypePath.
- intro. apply homset_property.
- induction k as [[k K] e], k' as [[k' K'] e']; cbn; cbn in e, e'.
induction (i A k k' (e @ !e')). apply maponpaths. apply isaprop_is_z_isomorphism.
apply homset_property.
Qed.
Lemma IsoArrowFrom_isaprop (M : category) {A B B':M} (g : A --> B) (g' : A --> B') :
isEpi g → isaprop (IsoArrowFrom g g').
Proof.
intros i. apply invproofirrelevance; intros k k'. apply subtypePath.
{ intros j. apply homset_property. }
induction k as [[k K] e], k' as [[k' K'] e']; cbn; cbn in e, e'.
apply subtypePath; cbn.
{ intros f. apply isaprop_is_z_isomorphism. apply homset_property. }
use i. exact (e @ !e').
Qed.
End Pullbacks.
Local Open Scope abgrcat.
Local Notation "0" := (unel (grtomonoid (abgrtogr _))) : abgrcat.
Local Notation "0" := (unel (grtomonoid (abgrtogr (to_abgr _ _)))) : abgrcat.
Local Notation "f + g" := (@op (pr1monoid (grtomonoid (abgrtogr _))) f g) : abgrcat.
Local Notation "f + g" := (@op (pr1monoid (grtomonoid (abgrtogr (to_abgr _ _)))) f g) : abgrcat.
Local Notation " - g" := (@grinv (abgrtogr _) g) : abgrcat.
Local Notation " - g" := (@grinv (abgrtogr (to_abgr _ _)) g) : abgrcat.
Local Notation "f - g" := (@op (pr1monoid (grtomonoid (abgrtogr _))) f (@grinv (abgrtogr (to_abgr _ _)) g)) : abgrcat.
Local Notation "f - g" := (@op (pr1monoid (grtomonoid (abgrtogr (to_abgr _ _)))) f (@grinv (abgrtogr (to_abgr _ _)) g)) : abgrcat.
Section PreAdditive.
Reprove some standard facts in additive categories with the 0 map (the zero element of the
group) replacing the zero map (defined by composing maps to and from the zero object).
Lemma ThroughZeroIsZero {M:PreAdditive} (a b:M) (Z : Zero M) (f : a --> Z) (g : Z --> b) : f · g = 0.
Proof.
intermediate_path ((0:a-->Z) · g).
- apply (maponpaths (postcomp_with g)). apply ArrowsToZero.
- apply to_postmor_unel'.
Qed.
Definition elem21 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : AB-->AB := 1 + π₁·f·ι₂.
Section Foo. Definition elem21_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : is_z_isomorphism (elem21 AB f).
Proof.
∃ (1 - π₁·f·ι₂).
unfold elem21. split.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
rewrite grinvunel. reflexivity.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
rewrite grinvunel. reflexivity.
Defined.
End Foo.
Definition elem12 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : AB-->AB := 1 + π₂·f·ι₁.
Definition elem12_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : is_z_isomorphism (elem12 AB f).
Proof.
∃ (1 - π₂·f·ι₁). unfold elem12. split.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
rewrite 2 (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite zeroLeft. rewrite zeroLeft.
rewrite 2 zeroRight.
use grinvunel.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
rewrite (assoc ι₁). rewrite (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite 2 zeroLeft.
rewrite 2 zeroRight. use grinvunel.
Defined.
Definition isKernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
f · g = 0 ∧ ∀ (w : M) (h : w --> y), h · g = 0 ⇒ ∃! φ : w --> x, φ · f = h.
Definition hasKernel {M:PreAdditive} {y z : M} (g : y --> z) : hProp :=
∃ x (f:x-->y), isKernel' f g.
Lemma isKernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x --> y) (g : y --> z) :
isKernel' f g ↔ ∑ e : f · g = ZeroArrow Z x z, isKernel Z f g e.
Proof.
split.
{ intros [e' ik].
use tpair.
{ refine (e' @ _). apply PreAdditive_unel_zero. }
intros T h e.
exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
{ intros [e ik]. use tpair.
{ refine (e @ ! _). apply PreAdditive_unel_zero. }
cbn beta. intros T h e'.
exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
Qed.
Definition isKernel'_to_Kernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
isKernel' f g → Kernel Z g.
Proof.
intros co. ∃ (x,,f). now apply isKernel_iff.
Defined.
Definition isCokernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
f · g = 0 ∧ ∀ (w : M) (h : y --> w), f · h = 0 ⇒ ∃! φ : z --> w, g · φ = h.
Definition hasCokernel {M:PreAdditive} {x y : M} (f : x --> y) : hProp :=
∃ z (g:y-->z), isCokernel' f g.
Lemma isCokernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x <-- y) (g : y <-- z) :
isCokernel' g f ↔ ∑ e : f ∘ g = ZeroArrow Z z x, isCokernel Z g f e.
Proof.
split.
{ intros [e' ik].
use tpair.
{ refine (e' @ _). apply PreAdditive_unel_zero. }
intros T h e.
exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
{ intros [e ik]. use tpair.
{ refine (e @ ! _). apply PreAdditive_unel_zero. }
cbn beta. intros T h e'.
exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
Qed.
Definition isCokernel'_to_Cokernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
isCokernel' f g → Cokernel Z f.
Proof.
intros co. ∃ (z,,g). now apply isCokernel_iff.
Defined.
Section Tmp.
Lemma PushoutCokernel {M:PreAdditive} {A B C D E:M} (i:A-->B) (p:B-->C)
(j:B-->D) (p':D-->E) (j':C-->E) :
isCokernel' i p → isPushout' (M:=M) j p p' j' → isCokernel' (i·j) p'.
Proof.
intros [b co] [e po].
split.
- rewrite assoc'.
Fail rewrite e.
unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e.
rewrite e.
rewrite assoc. rewrite b. apply zeroLeft.
- intros T h v. rewrite assoc' in v.
assert (Q := co T (j·h) v); cbn in Q. generalize Q; clear Q.
apply iscontrweqb. use make_weq.
+ intros [k w]; ∃ (j'·k); abstract (rewrite assoc; unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e; rewrite <- e; rewrite assoc';
rewrite w; reflexivity) using _L_.
+ cbn beta. intros [l w]; unfold hfiber. assert (PO := po T h l (!w)); clear po.
generalize PO; clear PO. apply iscontrweqb.
refine (weqcomp (weqtotal2asstor _ _) _). apply weqfibtototal; intros m. cbn.
apply weqiff.
{ split.
- intros [x y]. split.
+ exact x.
+ exact (maponpaths pr1 y).
- intros [x y]. ∃ x. induction y. apply maponpaths, to_has_homsets.
}
{ apply isofhleveltotal2.
- apply to_has_homsets.
- intros u. refine ((_:isofhlevel 2 _) _ _). apply isofhleveltotal2.
+ apply to_has_homsets.
+ intros n. apply hlevelntosn. apply to_has_homsets. }
{ apply isapropdirprod; apply to_has_homsets. }
Qed.
End Tmp.
Lemma PullbackKernel {M:PreAdditive} {A B C D E:M} (i:A<--B) (p:B<--C)
(j:B<--D) (p':D<--E) (j':C<--E) :
isKernel' p i → isPullback' (M:=M) j p p' j' → isKernel' p' (i∘j).
Proof.
exact (@PushoutCokernel (oppositePreAdditive M) A B C D E i p j p' j').
Defined.
Lemma KernelIsMonic {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isKernel' f g → isMonic f.
Proof.
intros [t i] w p q e.
set (T := ∑ r : w --> x, r · f = q · f). assert (ic : isProofIrrelevant T).
{ apply proofirrelevance, isapropifcontr.
use i. rewrite assoc'. rewrite t. apply zeroRight. }
set (t1 := (p,,e) : T). set (t2 := (q,,idpath _) : T).
assert (Q := ic t1 t2). exact (maponpaths pr1 Q).
Qed.
Lemma CokernelIsEpi {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isCokernel' f g → isEpi g.
Proof.
exact (KernelIsMonic (M:=oppositePreAdditive M) g f).
Qed.
Definition makeMonicKernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
isMonic f → f · g = 0 →
(∏ (w : M) (h : w --> y), h · g = 0 → ∑ φ : w --> x, φ · f = h) →
isKernel' f g.
Proof.
intros im eq ex. ∃ eq. intros w h e.
apply iscontraprop1.
- apply invproofirrelevance; intros [r R] [s S].
apply subtypePath_prop; simpl. apply im. exact (R@!S).
- apply ex. exact e.
Qed.
Definition makeEpiCokernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
isEpi g → f · g = 0 →
(∏ (w : M) (h : y --> w), f · h = 0 → ∑ φ : z --> w, g · φ = h) →
isCokernel' f g.
Proof.
exact (makeMonicKernel (M:=oppositePreAdditive M) g f).
Qed.
Lemma IsoWithKernel {M:PreAdditive} {x y z z':M} (f : x --> y) (g : y --> z) (h : z --> z') :
isKernel' f g → is_z_isomorphism h → isKernel' f (g·h).
Proof.
intros i j.
apply makeMonicKernel.
- exact (KernelIsMonic _ _ i).
- exact (assoc _ _ _ @ maponpaths (postcomp_with _) (pr1 i) @ zeroLeft h).
- intros w k e. apply (pr2 i).
refine (post_comp_with_iso_is_inj _ _ _ h (is_iso_from_is_z_iso h j) _ _ _ _).
refine (! assoc _ _ _ @ e @ ! zeroLeft _).
Qed.
Lemma IsoWithCokernel {M:PreAdditive} {x x' y z:M} (f : x --> y) (g : y --> z) (h : x' --> x) :
isCokernel' f g → is_z_isomorphism h → isCokernel' (h·f) g.
Proof.
exact (λ c i, IsoWithKernel (M:=oppositePreAdditive M) g f h c (opp_is_z_isomorphism h i)).
Qed.
Lemma KernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : x --> y) : isKernel' g (0 : y --> z) → is_z_isomorphism g.
Proof.
intros [_ ke]. use (is_z_iso_from_is_iso' M). intros T h. exact (ke _ _ (zeroRight _)).
Defined.
Lemma CokernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : y --> z) : isCokernel' (0 : x --> y) g → is_z_isomorphism g.
Proof.
intros [_ co]. use is_z_iso_from_is_iso. intros T h. exact (co _ _ (zeroLeft _)).
Defined.
Lemma KernelUniqueness {M:PreAdditive} {x x' y z : M} {f : x --> y} {f' : x' --> y} {g : y --> z} :
isKernel' f g → isKernel' f' g → iscontr (IsoArrowTo f f').
Proof.
intros i j. apply iscontraprop1.
- exact (IsoArrowTo_isaprop M f f' (KernelIsMonic f' g j)).
- induction (iscontrpr1 (pr2 j _ f (pr1 i))) as [p P].
induction (iscontrpr1 (pr2 i _ f' (pr1 j))) as [q Q].
use tpair.
+ ∃ p. ∃ q. split.
× apply (KernelIsMonic _ _ i). rewrite assoc'. rewrite Q. rewrite P. rewrite id_left. reflexivity.
× apply (KernelIsMonic _ _ j). rewrite assoc'. rewrite P. rewrite Q. rewrite id_left. reflexivity.
+ cbn. exact P.
Defined.
Lemma CokernelUniqueness {M:PreAdditive} {x y z z' : M} {f : x --> y} {g : y --> z} {g' : y --> z'} :
isCokernel' f g → isCokernel' f g' → iscontr (IsoArrowFrom g g').
Proof.
intros i j.
apply iscontraprop1.
- exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)).
- induction (iscontrpr1 (pr2 j _ g (pr1 i))) as [p P].
induction (iscontrpr1 (pr2 i _ g' (pr1 j))) as [q Q].
use tpair.
+ ∃ q. ∃ p. split.
× apply (CokernelIsEpi _ _ i). rewrite assoc. rewrite Q. rewrite P. rewrite id_right. reflexivity.
× apply (CokernelIsEpi _ _ j). rewrite assoc. rewrite P. rewrite Q. rewrite id_right. reflexivity.
+ cbn. exact Q.
Defined.
Lemma DirectSumToPullback {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
Pullback (0 : A --> Z) (0 : B --> Z).
Proof.
use tpair.
- ∃ S. exact (to_Pr1 S,, to_Pr2 S).
- cbn. use tpair.
+ apply ArrowsToZero.
+ cbn. intros T f g e. exact (to_isBinProduct M S T f g).
Defined.
Lemma DirectSumToPushout {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
Pushout (0 : Z --> A) (0 : Z --> B).
Proof.
use tpair.
- ∃ S. exact (to_In1 S,, to_In2 S).
- cbn. use tpair.
+ apply ArrowsFromZero.
+ cbn. intros T f g e. exact (to_isBinCoproduct M S T f g).
Defined.
Definition directSumMap {M:PreAdditive} {a b c d:M} (ac : BinDirectSum a c) (bd : BinDirectSum b d) (f : a --> b) (g : c --> d) : ac --> bd
:= BinDirectSumIndAr f g _ _.
Lemma directSumMapEqPr1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
directSumMap ac bd f g · π₁ = π₁ · f.
Proof.
apply BinDirectSumPr1Commutes.
Qed.
Lemma directSumMapEqPr2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
directSumMap ac bd f g · π₂ = π₂ · g.
Proof.
apply BinDirectSumPr2Commutes.
Qed.
Lemma directSumMapEqIn1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
ι₁ · directSumMap ac bd f g = f · ι₁.
Proof.
unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn1Commutes.
Qed.
Lemma directSumMapEqIn2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
ι₂ · directSumMap ac bd f g = g · ι₂.
Proof.
unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn2Commutes.
Qed.
Definition to_BinOpId' {M:PreAdditive} {a b co : M} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum i1 i2 p1 p2) :
p1 · i1 + p2 · i2 = identity co := to_BinOpId B.
Definition to_BinOpId'' {M:PreAdditive} {a b : M} (ab : BinDirectSum a b)
: (to_Pr1 ab · to_In1 ab) + (to_Pr2 ab · to_In2 ab) = 1
:= to_BinOpId ab.
Definition ismonoidfun_prop {G H:abgr} (f:G→H) : hProp := make_hProp (ismonoidfun f) (isapropismonoidfun f).
Definition PreAdditive_functor (M N:PreAdditive) :=
∑ F : M ⟶ N, ∀ A B:M, ismonoidfun_prop (@functor_on_morphisms M N F A B : A --> B → F A --> F B).
Coercion PreAdditive_functor_to_functor {M N:PreAdditive} : PreAdditive_functor M N → functor M N := pr1.
Definition functor_on_morphisms_add {C C' : PreAdditive} (F : PreAdditive_functor C C') { a b : C}
: monoidfun (a --> b) (F a --> F b)
:= monoidfunconstr (pr2 F a b).
Local Notation "# F" := (functor_on_morphisms_add F) : abgrcat.
Lemma add_functor_comp {M N:PreAdditive} (F : PreAdditive_functor M N) {A B C:M} (f:A --> B) (g:B --> C) :
# F (f · g) = # F f · # F g.
Proof.
exact (functor_comp F f g).
Qed.
Lemma add_functor_add {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (f g:A --> B) :
# F (f+g) = # F f + # F g.
Proof.
exact (ismonoidfunisbinopfun (pr2 F A B) f g).
Qed.
Lemma add_functor_zero {M N:PreAdditive} (F : PreAdditive_functor M N) (A B:M) :
functor_on_morphisms_add (a:=A) (b:=B) F 0 = 0.
Proof.
exact (ismonoidfununel (pr2 F A B)).
Qed.
Lemma add_functor_sub {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (g:A --> B) :
# F (-g) = - # F g.
Proof.
exact (grinvandmonoidfun _ _ (pr2 F A B) g).
Qed.
Lemma zeroCriterion {M:PreAdditive} {Z:M} : identity Z = 0 ↔ isZero Z.
Proof.
split.
{ intros e. split.
- intros T. ∃ 0. intros h. refine (! id_left h @ _). induction (!e); clear e. apply zeroLeft.
- intros T. ∃ 0. intros h. refine (! id_right h @ _). induction (!e); clear e. apply zeroRight. }
{ intros i. apply (isapropifcontr (pr1 i Z)). }
Qed.
Lemma applyFunctorToIsZero {M N:PreAdditive} (F : PreAdditive_functor M N) (Z : M) :
isZero Z → isZero (F Z).
Proof.
exact (λ i, pr1 zeroCriterion (! functor_id F Z @ maponpaths (#F) (pr2 zeroCriterion i) @ add_functor_zero F Z Z)).
Qed.
Definition applyFunctorToZero {M N:PreAdditive} (F : PreAdditive_functor M N) : Zero M → Zero N.
Proof.
intros Z. exact (F Z,, applyFunctorToIsZero F Z (pr2 Z)).
Defined.
Definition applyFunctorToIsBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N)
(A B S : M) (i1 : A --> S) (i2 : B --> S) (p1 : S --> A) (p2 : S --> B) :
isBinDirectSum i1 i2 p1 p2 → isBinDirectSum (# F i1) (# F i2) (# F p1) (# F p2).
Proof.
intros ds.
repeat split.
- rewrite <- add_functor_comp. rewrite (to_IdIn1 ds). apply functor_id.
- rewrite <- add_functor_comp. rewrite (to_IdIn2 ds). apply functor_id.
- rewrite <- add_functor_comp. rewrite (to_Unel1 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
- rewrite <- add_functor_comp. rewrite (to_Unel2 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
- rewrite <- 2 add_functor_comp. rewrite <- add_functor_add. rewrite (to_BinOpId' ds). apply functor_id.
Qed.
Definition applyFunctorToBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} :
BinDirectSum A B → BinDirectSum (F A) (F B)
:= λ S, make_BinDirectSum _ _ _ _ _ _ _ _ (applyFunctorToIsBinDirectSum F A B S ι₁ ι₂ π₁ π₂ (pr2 S)).
Definition induced_PreAdditive_incl (M : PreAdditive) {X:Type} (j : X → ob M) :
PreAdditive_functor (induced_PreAdditive M j) M.
Proof.
∃ (induced_precategory_incl j). intros A B. split.
+ intros f g. reflexivity.
+ reflexivity.
Defined.
Definition SwitchMap {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : ab --> ba := π₁ · ι₂ + π₂ · ι₁.
Lemma SwitchMapEqn {M:PreAdditive} {a b:M} (ab : BinDirectSum a b) (ba : BinDirectSum b a) : SwitchMap a b ab ba · SwitchMap b a ba ab = 1.
Proof.
unfold SwitchMap.
rewrite <- to_BinOpId''.
rewrite leftDistribute, 2 rightDistribute.
rewrite assoc', (assoc ι₂). rewrite DirectSumIn2Pr1.
rewrite zeroLeft, zeroRight, lunax.
rewrite assoc', (assoc ι₂). rewrite (to_IdIn2 ba), id_left.
apply maponpaths.
rewrite assoc', (assoc ι₁). rewrite (to_IdIn1 ba), id_left.
rewrite assoc', (assoc ι₁). rewrite DirectSumIn1Pr2.
rewrite zeroLeft, zeroRight, runax.
reflexivity.
Defined.
Definition SwitchIso {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : z_iso ab ba.
Proof.
∃ (SwitchMap _ _ _ _). ∃ (SwitchMap _ _ _ _). split; apply SwitchMapEqn.
Defined.
Lemma SwitchMapEqnTo {M:PreAdditive} {a b c:M} (bc : BinDirectSum b c) (cb : BinDirectSum c b) (f:a-->b) (g:a-->c) :
ToBinDirectSum bc f g · SwitchMap b c bc cb = ToBinDirectSum cb g f.
Proof.
unfold SwitchMap. apply ToBinDirectSumsEq.
- rewrite rightDistribute. rewrite 2 assoc.
rewrite 2 BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
rewrite leftDistribute. rewrite 2 assoc'.
rewrite (to_Unel2 cb).
unfold to_unel. rewrite zeroRight. rewrite lunax.
rewrite (to_IdIn1 cb). rewrite id_right. reflexivity.
- rewrite assoc'. rewrite leftDistribute. rewrite (assoc' π₂ _ π₂).
rewrite (to_Unel1 cb). unfold to_unel. rewrite zeroRight. rewrite runax.
rewrite 2 assoc. rewrite BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
rewrite assoc'. rewrite (to_IdIn2 cb). rewrite id_right. reflexivity.
Qed.
Lemma SwitchMapMapEqn {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (ca : BinDirectSum c a)
(bd : BinDirectSum b d) (db : BinDirectSum d b)
(f : a --> b) (g : c --> d) :
SwitchMap c a ca ac · directSumMap ac bd f g = directSumMap ca db g f · SwitchMap d b db bd.
Proof.
unfold SwitchMap.
rewrite leftDistribute.
rewrite assoc'. rewrite directSumMapEqIn2. rewrite assoc.
rewrite rightDistribute. rewrite assoc. rewrite directSumMapEqPr1.
apply maponpaths.
rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc.
rewrite assoc. rewrite directSumMapEqPr2.
reflexivity.
Qed.
Definition directSumMapSwitch {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (ca : BinDirectSum c a)
(bd : BinDirectSum b d) (db : BinDirectSum d b)
(f : a --> b) (g : c --> d) :
IsoArrow (directSumMap ac bd f g) (directSumMap ca db g f).
Proof.
∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
Defined.
Lemma opposite_directSumMap {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (bd : BinDirectSum b d)
(f : a --> b) (g : c --> d) :
directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g)
=
opp_mor (directSumMap ac bd f g).
Proof.
apply BinDirectSumIndArEq.
Qed.
Lemma opposite_directSumMap' {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (bd : BinDirectSum b d)
(f : a --> b) (g : c --> d) :
opp_mor (directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g))
=
directSumMap ac bd f g.
Proof.
apply (maponpaths opp_mor). apply opposite_directSumMap.
Qed.
Lemma SumOfKernels {M:PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
(f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
isKernel' f g → isKernel' f' g' → isKernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'. split.
{ refine (BinDirectSumIndArComp _ _ _ _ _ _ _ _ @ ! _).
apply ToBinDirectSumUnique.
- exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i)).
- exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i')). }
intros w h e. apply iscontraprop1.
2:{
assert (e1 := ! assoc _ _ _
@ ! maponpaths (precomp_with _) directSumMapEqPr1
@ assoc _ _ _
@ maponpaths (postcomp_with _) e
@ zeroLeft _).
assert (e2 := ! assoc _ _ _
@ ! maponpaths (precomp_with _) directSumMapEqPr2
@ assoc _ _ _
@ maponpaths (postcomp_with _) e
@ zeroLeft _).
induction (iscontrpr1 (pr2 i w (h · π₁) e1)) as [h1 H1].
induction (iscontrpr1 (pr2 i' w (h · π₂) e2)) as [h2 H2].
∃ (ToBinDirectSum _ h1 h2).
apply ToBinDirectSumsEq.
+ refine (! assoc _ _ _ @ _ @ H1).
refine (maponpaths (precomp_with _) directSumMapEqPr1 @ _).
unfold precomp_with.
refine (assoc _ _ _ @ _).
apply (maponpaths (postcomp_with _)).
apply BinDirectSumPr1Commutes.
+ refine (! assoc _ _ _ @ _ @ H2).
refine (maponpaths (precomp_with _) directSumMapEqPr2 @ _).
unfold precomp_with.
refine (assoc _ _ _ @ _).
apply (maponpaths (postcomp_with _)).
apply BinDirectSumPr2Commutes. }
apply invproofirrelevance.
intros [k K] [k' K'].
apply subtypePath_prop; cbn.
apply ToBinDirectSumsEq.
- refine (KernelIsMonic _ _ i _ _ _ _).
exact (! assoc _ _ _
@ ! maponpaths (precomp_with k) directSumMapEqPr1
@ assoc _ _ _
@ maponpaths (postcomp_with _) (K @ !K')
@ ! assoc _ _ _
@ maponpaths (precomp_with k') directSumMapEqPr1
@ assoc _ _ _).
- refine (KernelIsMonic _ _ i' _ _ _ _).
exact (! assoc _ _ _
@ ! maponpaths (precomp_with k) directSumMapEqPr2
@ assoc _ _ _
@ maponpaths (postcomp_with _) (K @ !K')
@ ! assoc _ _ _
@ maponpaths (precomp_with k') directSumMapEqPr2
@ assoc _ _ _).
Qed.
Lemma SumOfCokernels {M:PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
(f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
isCokernel' f g → isCokernel' f' g' → isCokernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'.
rewrite <- (opposite_directSumMap' xX yY f f').
rewrite <- (opposite_directSumMap' yY zZ g g').
exact (SumOfKernels (M:=oppositePreAdditive M) (oppositeBinDirectSum zZ) (oppositeBinDirectSum yY) (oppositeBinDirectSum xX) g f g' f' i i').
Qed.
Lemma inducedMapReflectsKernels (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isKernel' (# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isKernel' i p.
Proof.
exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
Qed.
Lemma inducedMapReflectsCokernels (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isCokernel' (# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isCokernel' i p.
Proof.
exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
Qed.
End PreAdditive.
Section KernelCokernelPairs.
Definition isKernelCokernelPair {M :PreAdditive} {A B C:M} (i : A --> B) (p: B --> C) : hProp
:= isKernel' i p ∧ isCokernel' i p.
Definition PairToKernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isKernel' i p := pr1.
Definition PairToCokernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isCokernel' i p := pr2.
Lemma inducedMapReflectsKernelCokernelPairs (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isKernelCokernelPair
(# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isKernelCokernelPair i p.
Proof.
intros [k c]. split.
- now apply inducedMapReflectsKernels.
- now apply inducedMapReflectsCokernels.
Qed.
Definition opposite_isKernelCokernelPair {M:PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isKernelCokernelPair (M:=oppositePreAdditive M) p i.
Proof.
intros s.
split.
- exact (PairToCokernel s).
- exact (PairToKernel s).
Defined.
Lemma PairUniqueness1 {M :PreAdditive} {A A' B C:M} (i : A --> B) (i' : A' --> B) (p: B --> C) :
isKernelCokernelPair i p → isKernelCokernelPair i' p → iscontr (IsoArrowTo i i').
Proof.
intros [k _] [k' _]. exact (KernelUniqueness k k').
Defined.
Lemma PairUniqueness2 {M :PreAdditive} {A B C C':M} (i : A --> B) (p: B --> C) (p': B --> C') :
isKernelCokernelPair i p → isKernelCokernelPair i p' → iscontr (IsoArrowFrom p p').
Proof.
intros [_ c] [_ c']. exact (CokernelUniqueness c c').
Defined.
Lemma kerCokerDirectSum {M :PreAdditive} {A B:M} (S:BinDirectSum A B) : isKernelCokernelPair (to_In1 S) (to_Pr2 S).
Proof.
assert (E := BinDirectSum_isBinDirectSum M S).
split.
- ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
+ exact (h · to_Pr1 S).
+ refine (! assoc _ _ _ @ _ @ id_right _). rewrite <- (to_BinOpId' S).
rewrite rightDistribute. rewrite (assoc h (to_Pr2 S) (to_In2 S)).
rewrite H; clear H. rewrite zeroLeft. apply pathsinv0. apply (runax (T-->S)).
+ intros k. apply to_has_homsets.
+ clear H. intros k e. induction e. rewrite assoc'.
rewrite (to_IdIn1 S). apply pathsinv0, id_right.
- ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
+ exact (ι₂ · h).
+ refine (assoc _ _ _ @ _ @ id_left h). rewrite <- (to_BinOpId' S).
rewrite leftDistribute.
rewrite <- (assoc (to_Pr1 S) (to_In1 S) h). rewrite H; clear H.
rewrite zeroRight. apply pathsinv0. apply (lunax (S-->T)).
+ intros k. apply to_has_homsets.
+ clear H. intros k e. induction e. rewrite assoc. rewrite (to_IdIn2 S).
exact (! id_left _).
Qed.
Lemma kerCoker10 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (identity A) (0 : A --> Z).
Proof.
exact (kerCokerDirectSum (TrivialDirectSum Z A)).
Qed.
Lemma kerCoker01 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (0 : Z --> A) (identity A).
Proof.
exact (kerCokerDirectSum (TrivialDirectSum' Z A)).
Qed.
Lemma PairPushoutMap {M :PreAdditive} {A B C A':M} {i : A --> B} {p : B --> C}
(pr : isKernelCokernelPair i p)
(r : A --> A') (po : Pushout i r) :
∑ (q : po --> C), PushoutIn1 po · q = p × PushoutIn2 po · q = 0.
Proof.
refine (iscontrpr1 (isPushout_Pushout po C p 0 _)).
refine (pr1 (PairToCokernel pr) @ ! _). apply zeroRight.
Qed.
Lemma PairPullbackMap {M :PreAdditive} {A B C A':M} {i : A <-- B} {p : B <-- C}
(pr : isKernelCokernelPair p i)
(r : A <-- A') (pb : Pullback i r) :
∑ (q : pb <-- C), PullbackPr1 pb ∘ q = p × PullbackPr2 pb ∘ q = 0.
Proof.
exact (PairPushoutMap (M:=oppositePreAdditive M) (opposite_isKernelCokernelPair pr) r pb).
Defined.
Lemma PairPushoutCokernel {M :PreAdditive} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isKernelCokernelPair i p)
(r : A --> A') (po : Pushout i r)
(j := PushoutIn2 po)
(pp := PairPushoutMap pr r po) :
isCokernel' j (pr1 pp).
Proof.
set (s := PushoutIn1 po).
induction pp as [q [e1 e2]]; change (isCokernel' j q);
change (hProptoType (s · q = p)) in e1;
change (hProptoType (j · q = 0)) in e2.
∃ e2.
intros T h e.
assert (L : i · (s · h) = 0).
{ refine (assoc _ _ _ @ _).
intermediate_path (r · j · h).
{ apply (maponpaths (λ s, s · h)). exact (PushoutSqrCommutes po). }
refine (! assoc _ _ _ @ _).
induction (!e).
apply zeroRight. }
assert (V := iscontrpr1 ((pr22 pr) T (s · h) L)); clear L.
induction V as [k e3].
use iscontraprop1.
{ apply invproofirrelevance; intros φ φ'.
apply subtypePath_prop.
induction φ as [φ e4]; induction φ' as [φ' e5]; cbn.
use (_ : isEpi q).
{ apply (isEpi_precomp M s q). rewrite e1. apply (CokernelIsEpi i p). apply pr. }
exact (e4 @ ! e5). }
∃ k.
use (MorphismsOutofPushoutEqual (isPushout_Pushout po)); fold s j.
{ refine (assoc _ _ _ @ _ @ e3). apply (maponpaths (λ s, s · k)). exact e1. }
{ refine (assoc _ _ _ @ _ @ ! e). rewrite e2. apply zeroLeft. }
Qed.
Lemma PairPullbackKernel {M : PreAdditive} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isKernelCokernelPair p i)
(r : A <-- A') (pb : Pullback i r)
(j := PullbackPr2 pb)
(pp := PairPullbackMap pr r pb) :
isKernel' (pr1 pp) j.
Proof.
exact (PairPushoutCokernel (M:=oppositePreAdditive M) i p (opposite_isKernelCokernelPair pr) r pb).
Defined.
Lemma SumOfKernelCokernelPairs {M : PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
{f : x --> y} {g : y --> z} {f' : X --> Y} {g' : Y --> Z}
: isKernelCokernelPair f g → isKernelCokernelPair f' g' → isKernelCokernelPair (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'.
∃ (SumOfKernels _ _ _ f g f' g' (pr1 i) (pr1 i')).
exact (SumOfCokernels _ _ _ f g f' g' (pr2 i) (pr2 i')).
Qed.
End KernelCokernelPairs.
Section theDefinition.
Definition ExactCategoryData := ∑ M:AdditiveCategory, MorphismPair M → hProp. Coercion ExactCategoryDataToAdditiveCategory (ME : ExactCategoryData) : AdditiveCategory := pr1 ME.
Definition isExact {M : ExactCategoryData} (E : MorphismPair M) : hProp := pr2 M E.
Definition isExact2 {M : ExactCategoryData} {A B C:M} (f:A-->B) (g:B-->C) := isExact (make_MorphismPair f g).
Definition isAdmissibleMonomorphism {M : ExactCategoryData} {A B:M} (i : A --> B) : hProp :=
∃ C (p : B --> C), isExact2 i p.
Definition AdmissibleMonomorphism {M : ExactCategoryData} (A B:M) : Type :=
∑ (i : A --> B), isAdmissibleMonomorphism i.
Coercion AdmMonoToMap {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → A --> B := pr1.
Coercion AdmMonoToMap' {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → (A --> B)%cat := pr1.
Definition isAdmissibleEpimorphism {M : ExactCategoryData} {B C:M} (p : B --> C) : hProp :=
∃ A (i : A --> B), isExact2 i p.
Definition AdmissibleEpimorphism {M : ExactCategoryData} (B C:M) : Type :=
∑ (p : B --> C), isAdmissibleEpimorphism p.
Coercion AdmEpiToMap {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → B --> C := pr1.
Coercion AdmEpiToMap' {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → (B --> C)%cat := pr1.
Lemma ExactToAdmMono {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleMonomorphism i.
Proof.
intros e. exact (hinhpr(C,,p,,e)).
Qed.
Lemma ExactToAdmEpi {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleEpimorphism p.
Proof.
intros e. exact (hinhpr(A,,i,,e)).
Qed.
Proof.
intermediate_path ((0:a-->Z) · g).
- apply (maponpaths (postcomp_with g)). apply ArrowsToZero.
- apply to_postmor_unel'.
Qed.
Definition elem21 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : AB-->AB := 1 + π₁·f·ι₂.
Section Foo. Definition elem21_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:A-->B) : is_z_isomorphism (elem21 AB f).
Proof.
∃ (1 - π₁·f·ι₂).
unfold elem21. split.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
rewrite grinvunel. reflexivity.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc π₁ f ι₂).
rewrite (assoc ι₂). rewrite DirectSumIn2Pr1. rewrite zeroLeft. rewrite zeroRight.
rewrite grinvunel. reflexivity.
Defined.
End Foo.
Definition elem12 {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : AB-->AB := 1 + π₂·f·ι₁.
Definition elem12_isiso {M:PreAdditive} {A B:M} (AB : BinDirectSum A B) (f:B-->A) : is_z_isomorphism (elem12 AB f).
Proof.
∃ (1 - π₂·f·ι₁). unfold elem12. split.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite rightMinus.
rewrite <- assocax. rewrite grlinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
rewrite 2 (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite zeroLeft. rewrite zeroLeft.
rewrite 2 zeroRight.
use grinvunel.
- rewrite leftDistribute, 2 rightDistribute. rewrite id_left. refine (_ @ runax (Hom_add _ _ _) _).
rewrite assocax. apply maponpaths. rewrite id_right, id_left. rewrite leftMinus.
rewrite <- assocax. rewrite grrinvax. rewrite lunax. rewrite assoc'. rewrite <- (assoc _ f _).
rewrite (assoc ι₁). rewrite (assoc ι₁). rewrite DirectSumIn1Pr2. rewrite 2 zeroLeft.
rewrite 2 zeroRight. use grinvunel.
Defined.
Definition isKernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
f · g = 0 ∧ ∀ (w : M) (h : w --> y), h · g = 0 ⇒ ∃! φ : w --> x, φ · f = h.
Definition hasKernel {M:PreAdditive} {y z : M} (g : y --> z) : hProp :=
∃ x (f:x-->y), isKernel' f g.
Lemma isKernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x --> y) (g : y --> z) :
isKernel' f g ↔ ∑ e : f · g = ZeroArrow Z x z, isKernel Z f g e.
Proof.
split.
{ intros [e' ik].
use tpair.
{ refine (e' @ _). apply PreAdditive_unel_zero. }
intros T h e.
exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
{ intros [e ik]. use tpair.
{ refine (e @ ! _). apply PreAdditive_unel_zero. }
cbn beta. intros T h e'.
exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
Qed.
Definition isKernel'_to_Kernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
isKernel' f g → Kernel Z g.
Proof.
intros co. ∃ (x,,f). now apply isKernel_iff.
Defined.
Definition isCokernel' {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) : hProp :=
f · g = 0 ∧ ∀ (w : M) (h : y --> w), f · h = 0 ⇒ ∃! φ : z --> w, g · φ = h.
Definition hasCokernel {M:PreAdditive} {x y : M} (f : x --> y) : hProp :=
∃ z (g:y-->z), isCokernel' f g.
Lemma isCokernel_iff {M:PreAdditive} {x y z : M} (Z:Zero M) (f : x <-- y) (g : y <-- z) :
isCokernel' g f ↔ ∑ e : f ∘ g = ZeroArrow Z z x, isCokernel Z g f e.
Proof.
split.
{ intros [e' ik].
use tpair.
{ refine (e' @ _). apply PreAdditive_unel_zero. }
intros T h e.
exact (ik T h (e @ ! PreAdditive_unel_zero _ _ _ _)). }
{ intros [e ik]. use tpair.
{ refine (e @ ! _). apply PreAdditive_unel_zero. }
cbn beta. intros T h e'.
exact (ik T h (e' @ PreAdditive_unel_zero _ _ _ _)). }
Qed.
Definition isCokernel'_to_Cokernel {M:PreAdditive} (Z:Zero M) {x y z : M} (f : x --> y) (g : y --> z) :
isCokernel' f g → Cokernel Z f.
Proof.
intros co. ∃ (z,,g). now apply isCokernel_iff.
Defined.
Section Tmp.
Lemma PushoutCokernel {M:PreAdditive} {A B C D E:M} (i:A-->B) (p:B-->C)
(j:B-->D) (p':D-->E) (j':C-->E) :
isCokernel' i p → isPushout' (M:=M) j p p' j' → isCokernel' (i·j) p'.
Proof.
intros [b co] [e po].
split.
- rewrite assoc'.
Fail rewrite e.
unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e.
rewrite e.
rewrite assoc. rewrite b. apply zeroLeft.
- intros T h v. rewrite assoc' in v.
assert (Q := co T (j·h) v); cbn in Q. generalize Q; clear Q.
apply iscontrweqb. use make_weq.
+ intros [k w]; ∃ (j'·k); abstract (rewrite assoc; unfold categoryWithAbgrops_category, category_to_precategory, pr1 in e; rewrite <- e; rewrite assoc';
rewrite w; reflexivity) using _L_.
+ cbn beta. intros [l w]; unfold hfiber. assert (PO := po T h l (!w)); clear po.
generalize PO; clear PO. apply iscontrweqb.
refine (weqcomp (weqtotal2asstor _ _) _). apply weqfibtototal; intros m. cbn.
apply weqiff.
{ split.
- intros [x y]. split.
+ exact x.
+ exact (maponpaths pr1 y).
- intros [x y]. ∃ x. induction y. apply maponpaths, to_has_homsets.
}
{ apply isofhleveltotal2.
- apply to_has_homsets.
- intros u. refine ((_:isofhlevel 2 _) _ _). apply isofhleveltotal2.
+ apply to_has_homsets.
+ intros n. apply hlevelntosn. apply to_has_homsets. }
{ apply isapropdirprod; apply to_has_homsets. }
Qed.
End Tmp.
Lemma PullbackKernel {M:PreAdditive} {A B C D E:M} (i:A<--B) (p:B<--C)
(j:B<--D) (p':D<--E) (j':C<--E) :
isKernel' p i → isPullback' (M:=M) j p p' j' → isKernel' p' (i∘j).
Proof.
exact (@PushoutCokernel (oppositePreAdditive M) A B C D E i p j p' j').
Defined.
Lemma KernelIsMonic {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isKernel' f g → isMonic f.
Proof.
intros [t i] w p q e.
set (T := ∑ r : w --> x, r · f = q · f). assert (ic : isProofIrrelevant T).
{ apply proofirrelevance, isapropifcontr.
use i. rewrite assoc'. rewrite t. apply zeroRight. }
set (t1 := (p,,e) : T). set (t2 := (q,,idpath _) : T).
assert (Q := ic t1 t2). exact (maponpaths pr1 Q).
Qed.
Lemma CokernelIsEpi {M:PreAdditive} {x y z:M} (f : x --> y) (g : y --> z) : isCokernel' f g → isEpi g.
Proof.
exact (KernelIsMonic (M:=oppositePreAdditive M) g f).
Qed.
Definition makeMonicKernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
isMonic f → f · g = 0 →
(∏ (w : M) (h : w --> y), h · g = 0 → ∑ φ : w --> x, φ · f = h) →
isKernel' f g.
Proof.
intros im eq ex. ∃ eq. intros w h e.
apply iscontraprop1.
- apply invproofirrelevance; intros [r R] [s S].
apply subtypePath_prop; simpl. apply im. exact (R@!S).
- apply ex. exact e.
Qed.
Definition makeEpiCokernel {M:PreAdditive} {x y z : M} (f : x --> y) (g : y --> z) :
isEpi g → f · g = 0 →
(∏ (w : M) (h : y --> w), f · h = 0 → ∑ φ : z --> w, g · φ = h) →
isCokernel' f g.
Proof.
exact (makeMonicKernel (M:=oppositePreAdditive M) g f).
Qed.
Lemma IsoWithKernel {M:PreAdditive} {x y z z':M} (f : x --> y) (g : y --> z) (h : z --> z') :
isKernel' f g → is_z_isomorphism h → isKernel' f (g·h).
Proof.
intros i j.
apply makeMonicKernel.
- exact (KernelIsMonic _ _ i).
- exact (assoc _ _ _ @ maponpaths (postcomp_with _) (pr1 i) @ zeroLeft h).
- intros w k e. apply (pr2 i).
refine (post_comp_with_iso_is_inj _ _ _ h (is_iso_from_is_z_iso h j) _ _ _ _).
refine (! assoc _ _ _ @ e @ ! zeroLeft _).
Qed.
Lemma IsoWithCokernel {M:PreAdditive} {x x' y z:M} (f : x --> y) (g : y --> z) (h : x' --> x) :
isCokernel' f g → is_z_isomorphism h → isCokernel' (h·f) g.
Proof.
exact (λ c i, IsoWithKernel (M:=oppositePreAdditive M) g f h c (opp_is_z_isomorphism h i)).
Qed.
Lemma KernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : x --> y) : isKernel' g (0 : y --> z) → is_z_isomorphism g.
Proof.
intros [_ ke]. use (is_z_iso_from_is_iso' M). intros T h. exact (ke _ _ (zeroRight _)).
Defined.
Lemma CokernelOfZeroMapIsIso {M:PreAdditive} {x y z:M} (g : y --> z) : isCokernel' (0 : x --> y) g → is_z_isomorphism g.
Proof.
intros [_ co]. use is_z_iso_from_is_iso. intros T h. exact (co _ _ (zeroLeft _)).
Defined.
Lemma KernelUniqueness {M:PreAdditive} {x x' y z : M} {f : x --> y} {f' : x' --> y} {g : y --> z} :
isKernel' f g → isKernel' f' g → iscontr (IsoArrowTo f f').
Proof.
intros i j. apply iscontraprop1.
- exact (IsoArrowTo_isaprop M f f' (KernelIsMonic f' g j)).
- induction (iscontrpr1 (pr2 j _ f (pr1 i))) as [p P].
induction (iscontrpr1 (pr2 i _ f' (pr1 j))) as [q Q].
use tpair.
+ ∃ p. ∃ q. split.
× apply (KernelIsMonic _ _ i). rewrite assoc'. rewrite Q. rewrite P. rewrite id_left. reflexivity.
× apply (KernelIsMonic _ _ j). rewrite assoc'. rewrite P. rewrite Q. rewrite id_left. reflexivity.
+ cbn. exact P.
Defined.
Lemma CokernelUniqueness {M:PreAdditive} {x y z z' : M} {f : x --> y} {g : y --> z} {g' : y --> z'} :
isCokernel' f g → isCokernel' f g' → iscontr (IsoArrowFrom g g').
Proof.
intros i j.
apply iscontraprop1.
- exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)).
- induction (iscontrpr1 (pr2 j _ g (pr1 i))) as [p P].
induction (iscontrpr1 (pr2 i _ g' (pr1 j))) as [q Q].
use tpair.
+ ∃ q. ∃ p. split.
× apply (CokernelIsEpi _ _ i). rewrite assoc. rewrite Q. rewrite P. rewrite id_right. reflexivity.
× apply (CokernelIsEpi _ _ j). rewrite assoc. rewrite P. rewrite Q. rewrite id_right. reflexivity.
+ cbn. exact Q.
Defined.
Lemma DirectSumToPullback {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
Pullback (0 : A --> Z) (0 : B --> Z).
Proof.
use tpair.
- ∃ S. exact (to_Pr1 S,, to_Pr2 S).
- cbn. use tpair.
+ apply ArrowsToZero.
+ cbn. intros T f g e. exact (to_isBinProduct M S T f g).
Defined.
Lemma DirectSumToPushout {M:PreAdditive} {A B:M} (S : BinDirectSum A B) (Z : Zero M) :
Pushout (0 : Z --> A) (0 : Z --> B).
Proof.
use tpair.
- ∃ S. exact (to_In1 S,, to_In2 S).
- cbn. use tpair.
+ apply ArrowsFromZero.
+ cbn. intros T f g e. exact (to_isBinCoproduct M S T f g).
Defined.
Definition directSumMap {M:PreAdditive} {a b c d:M} (ac : BinDirectSum a c) (bd : BinDirectSum b d) (f : a --> b) (g : c --> d) : ac --> bd
:= BinDirectSumIndAr f g _ _.
Lemma directSumMapEqPr1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
directSumMap ac bd f g · π₁ = π₁ · f.
Proof.
apply BinDirectSumPr1Commutes.
Qed.
Lemma directSumMapEqPr2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
directSumMap ac bd f g · π₂ = π₂ · g.
Proof.
apply BinDirectSumPr2Commutes.
Qed.
Lemma directSumMapEqIn1 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
ι₁ · directSumMap ac bd f g = f · ι₁.
Proof.
unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn1Commutes.
Qed.
Lemma directSumMapEqIn2 {M:PreAdditive} {a b c d:M} {ac : BinDirectSum a c} {bd : BinDirectSum b d} {f : a --> b} {g : c --> d} :
ι₂ · directSumMap ac bd f g = g · ι₂.
Proof.
unfold directSumMap. rewrite BinDirectSumIndArEq. apply BinDirectSumIn2Commutes.
Qed.
Definition to_BinOpId' {M:PreAdditive} {a b co : M} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum i1 i2 p1 p2) :
p1 · i1 + p2 · i2 = identity co := to_BinOpId B.
Definition to_BinOpId'' {M:PreAdditive} {a b : M} (ab : BinDirectSum a b)
: (to_Pr1 ab · to_In1 ab) + (to_Pr2 ab · to_In2 ab) = 1
:= to_BinOpId ab.
Definition ismonoidfun_prop {G H:abgr} (f:G→H) : hProp := make_hProp (ismonoidfun f) (isapropismonoidfun f).
Definition PreAdditive_functor (M N:PreAdditive) :=
∑ F : M ⟶ N, ∀ A B:M, ismonoidfun_prop (@functor_on_morphisms M N F A B : A --> B → F A --> F B).
Coercion PreAdditive_functor_to_functor {M N:PreAdditive} : PreAdditive_functor M N → functor M N := pr1.
Definition functor_on_morphisms_add {C C' : PreAdditive} (F : PreAdditive_functor C C') { a b : C}
: monoidfun (a --> b) (F a --> F b)
:= monoidfunconstr (pr2 F a b).
Local Notation "# F" := (functor_on_morphisms_add F) : abgrcat.
Lemma add_functor_comp {M N:PreAdditive} (F : PreAdditive_functor M N) {A B C:M} (f:A --> B) (g:B --> C) :
# F (f · g) = # F f · # F g.
Proof.
exact (functor_comp F f g).
Qed.
Lemma add_functor_add {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (f g:A --> B) :
# F (f+g) = # F f + # F g.
Proof.
exact (ismonoidfunisbinopfun (pr2 F A B) f g).
Qed.
Lemma add_functor_zero {M N:PreAdditive} (F : PreAdditive_functor M N) (A B:M) :
functor_on_morphisms_add (a:=A) (b:=B) F 0 = 0.
Proof.
exact (ismonoidfununel (pr2 F A B)).
Qed.
Lemma add_functor_sub {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} (g:A --> B) :
# F (-g) = - # F g.
Proof.
exact (grinvandmonoidfun _ _ (pr2 F A B) g).
Qed.
Lemma zeroCriterion {M:PreAdditive} {Z:M} : identity Z = 0 ↔ isZero Z.
Proof.
split.
{ intros e. split.
- intros T. ∃ 0. intros h. refine (! id_left h @ _). induction (!e); clear e. apply zeroLeft.
- intros T. ∃ 0. intros h. refine (! id_right h @ _). induction (!e); clear e. apply zeroRight. }
{ intros i. apply (isapropifcontr (pr1 i Z)). }
Qed.
Lemma applyFunctorToIsZero {M N:PreAdditive} (F : PreAdditive_functor M N) (Z : M) :
isZero Z → isZero (F Z).
Proof.
exact (λ i, pr1 zeroCriterion (! functor_id F Z @ maponpaths (#F) (pr2 zeroCriterion i) @ add_functor_zero F Z Z)).
Qed.
Definition applyFunctorToZero {M N:PreAdditive} (F : PreAdditive_functor M N) : Zero M → Zero N.
Proof.
intros Z. exact (F Z,, applyFunctorToIsZero F Z (pr2 Z)).
Defined.
Definition applyFunctorToIsBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N)
(A B S : M) (i1 : A --> S) (i2 : B --> S) (p1 : S --> A) (p2 : S --> B) :
isBinDirectSum i1 i2 p1 p2 → isBinDirectSum (# F i1) (# F i2) (# F p1) (# F p2).
Proof.
intros ds.
repeat split.
- rewrite <- add_functor_comp. rewrite (to_IdIn1 ds). apply functor_id.
- rewrite <- add_functor_comp. rewrite (to_IdIn2 ds). apply functor_id.
- rewrite <- add_functor_comp. rewrite (to_Unel1 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
- rewrite <- add_functor_comp. rewrite (to_Unel2 ds); unfold to_unel. use ismonoidfununel. use (pr2 F).
- rewrite <- 2 add_functor_comp. rewrite <- add_functor_add. rewrite (to_BinOpId' ds). apply functor_id.
Qed.
Definition applyFunctorToBinDirectSum {M N:PreAdditive} (F : PreAdditive_functor M N) {A B:M} :
BinDirectSum A B → BinDirectSum (F A) (F B)
:= λ S, make_BinDirectSum _ _ _ _ _ _ _ _ (applyFunctorToIsBinDirectSum F A B S ι₁ ι₂ π₁ π₂ (pr2 S)).
Definition induced_PreAdditive_incl (M : PreAdditive) {X:Type} (j : X → ob M) :
PreAdditive_functor (induced_PreAdditive M j) M.
Proof.
∃ (induced_precategory_incl j). intros A B. split.
+ intros f g. reflexivity.
+ reflexivity.
Defined.
Definition SwitchMap {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : ab --> ba := π₁ · ι₂ + π₂ · ι₁.
Lemma SwitchMapEqn {M:PreAdditive} {a b:M} (ab : BinDirectSum a b) (ba : BinDirectSum b a) : SwitchMap a b ab ba · SwitchMap b a ba ab = 1.
Proof.
unfold SwitchMap.
rewrite <- to_BinOpId''.
rewrite leftDistribute, 2 rightDistribute.
rewrite assoc', (assoc ι₂). rewrite DirectSumIn2Pr1.
rewrite zeroLeft, zeroRight, lunax.
rewrite assoc', (assoc ι₂). rewrite (to_IdIn2 ba), id_left.
apply maponpaths.
rewrite assoc', (assoc ι₁). rewrite (to_IdIn1 ba), id_left.
rewrite assoc', (assoc ι₁). rewrite DirectSumIn1Pr2.
rewrite zeroLeft, zeroRight, runax.
reflexivity.
Defined.
Definition SwitchIso {M:PreAdditive} (a b:M) (ab : BinDirectSum a b) (ba : BinDirectSum b a) : z_iso ab ba.
Proof.
∃ (SwitchMap _ _ _ _). ∃ (SwitchMap _ _ _ _). split; apply SwitchMapEqn.
Defined.
Lemma SwitchMapEqnTo {M:PreAdditive} {a b c:M} (bc : BinDirectSum b c) (cb : BinDirectSum c b) (f:a-->b) (g:a-->c) :
ToBinDirectSum bc f g · SwitchMap b c bc cb = ToBinDirectSum cb g f.
Proof.
unfold SwitchMap. apply ToBinDirectSumsEq.
- rewrite rightDistribute. rewrite 2 assoc.
rewrite 2 BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
rewrite leftDistribute. rewrite 2 assoc'.
rewrite (to_Unel2 cb).
unfold to_unel. rewrite zeroRight. rewrite lunax.
rewrite (to_IdIn1 cb). rewrite id_right. reflexivity.
- rewrite assoc'. rewrite leftDistribute. rewrite (assoc' π₂ _ π₂).
rewrite (to_Unel1 cb). unfold to_unel. rewrite zeroRight. rewrite runax.
rewrite 2 assoc. rewrite BinDirectSumPr1Commutes, BinDirectSumPr2Commutes.
rewrite assoc'. rewrite (to_IdIn2 cb). rewrite id_right. reflexivity.
Qed.
Lemma SwitchMapMapEqn {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (ca : BinDirectSum c a)
(bd : BinDirectSum b d) (db : BinDirectSum d b)
(f : a --> b) (g : c --> d) :
SwitchMap c a ca ac · directSumMap ac bd f g = directSumMap ca db g f · SwitchMap d b db bd.
Proof.
unfold SwitchMap.
rewrite leftDistribute.
rewrite assoc'. rewrite directSumMapEqIn2. rewrite assoc.
rewrite rightDistribute. rewrite assoc. rewrite directSumMapEqPr1.
apply maponpaths.
rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc.
rewrite assoc. rewrite directSumMapEqPr2.
reflexivity.
Qed.
Definition directSumMapSwitch {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (ca : BinDirectSum c a)
(bd : BinDirectSum b d) (db : BinDirectSum d b)
(f : a --> b) (g : c --> d) :
IsoArrow (directSumMap ac bd f g) (directSumMap ca db g f).
Proof.
∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
Defined.
Lemma opposite_directSumMap {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (bd : BinDirectSum b d)
(f : a --> b) (g : c --> d) :
directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g)
=
opp_mor (directSumMap ac bd f g).
Proof.
apply BinDirectSumIndArEq.
Qed.
Lemma opposite_directSumMap' {M:PreAdditive} {a b c d:M}
(ac : BinDirectSum a c) (bd : BinDirectSum b d)
(f : a --> b) (g : c --> d) :
opp_mor (directSumMap (M:=oppositePreAdditive M) (oppositeBinDirectSum bd) (oppositeBinDirectSum ac) (opp_mor f) (opp_mor g))
=
directSumMap ac bd f g.
Proof.
apply (maponpaths opp_mor). apply opposite_directSumMap.
Qed.
Lemma SumOfKernels {M:PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
(f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
isKernel' f g → isKernel' f' g' → isKernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'. split.
{ refine (BinDirectSumIndArComp _ _ _ _ _ _ _ _ @ ! _).
apply ToBinDirectSumUnique.
- exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i)).
- exact (zeroLeft _ @ ! zeroRight _ @ maponpaths _ (! pr1 i')). }
intros w h e. apply iscontraprop1.
2:{
assert (e1 := ! assoc _ _ _
@ ! maponpaths (precomp_with _) directSumMapEqPr1
@ assoc _ _ _
@ maponpaths (postcomp_with _) e
@ zeroLeft _).
assert (e2 := ! assoc _ _ _
@ ! maponpaths (precomp_with _) directSumMapEqPr2
@ assoc _ _ _
@ maponpaths (postcomp_with _) e
@ zeroLeft _).
induction (iscontrpr1 (pr2 i w (h · π₁) e1)) as [h1 H1].
induction (iscontrpr1 (pr2 i' w (h · π₂) e2)) as [h2 H2].
∃ (ToBinDirectSum _ h1 h2).
apply ToBinDirectSumsEq.
+ refine (! assoc _ _ _ @ _ @ H1).
refine (maponpaths (precomp_with _) directSumMapEqPr1 @ _).
unfold precomp_with.
refine (assoc _ _ _ @ _).
apply (maponpaths (postcomp_with _)).
apply BinDirectSumPr1Commutes.
+ refine (! assoc _ _ _ @ _ @ H2).
refine (maponpaths (precomp_with _) directSumMapEqPr2 @ _).
unfold precomp_with.
refine (assoc _ _ _ @ _).
apply (maponpaths (postcomp_with _)).
apply BinDirectSumPr2Commutes. }
apply invproofirrelevance.
intros [k K] [k' K'].
apply subtypePath_prop; cbn.
apply ToBinDirectSumsEq.
- refine (KernelIsMonic _ _ i _ _ _ _).
exact (! assoc _ _ _
@ ! maponpaths (precomp_with k) directSumMapEqPr1
@ assoc _ _ _
@ maponpaths (postcomp_with _) (K @ !K')
@ ! assoc _ _ _
@ maponpaths (precomp_with k') directSumMapEqPr1
@ assoc _ _ _).
- refine (KernelIsMonic _ _ i' _ _ _ _).
exact (! assoc _ _ _
@ ! maponpaths (precomp_with k) directSumMapEqPr2
@ assoc _ _ _
@ maponpaths (postcomp_with _) (K @ !K')
@ ! assoc _ _ _
@ maponpaths (precomp_with k') directSumMapEqPr2
@ assoc _ _ _).
Qed.
Lemma SumOfCokernels {M:PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
(f : x --> y) (g : y --> z) (f' : X --> Y) (g' : Y --> Z) :
isCokernel' f g → isCokernel' f' g' → isCokernel' (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'.
rewrite <- (opposite_directSumMap' xX yY f f').
rewrite <- (opposite_directSumMap' yY zZ g g').
exact (SumOfKernels (M:=oppositePreAdditive M) (oppositeBinDirectSum zZ) (oppositeBinDirectSum yY) (oppositeBinDirectSum xX) g f g' f' i i').
Qed.
Lemma inducedMapReflectsKernels (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isKernel' (# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isKernel' i p.
Proof.
exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
Qed.
Lemma inducedMapReflectsCokernels (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isCokernel' (# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isCokernel' i p.
Proof.
exact (λ k, pr1 k,,λ T h e, pr2 k (j T) h e).
Qed.
End PreAdditive.
Section KernelCokernelPairs.
Definition isKernelCokernelPair {M :PreAdditive} {A B C:M} (i : A --> B) (p: B --> C) : hProp
:= isKernel' i p ∧ isCokernel' i p.
Definition PairToKernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isKernel' i p := pr1.
Definition PairToCokernel {M :PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isCokernel' i p := pr2.
Lemma inducedMapReflectsKernelCokernelPairs (M : PreAdditive) {X:Type} (j : X → ob M)
{A B C:induced_PreAdditive M j} (i:A-->B) (p:B-->C) :
isKernelCokernelPair
(# (induced_PreAdditive_incl M j) i)
(# (induced_PreAdditive_incl M j) p)
→
isKernelCokernelPair i p.
Proof.
intros [k c]. split.
- now apply inducedMapReflectsKernels.
- now apply inducedMapReflectsCokernels.
Qed.
Definition opposite_isKernelCokernelPair {M:PreAdditive} {A B C:M} {i : A --> B} {p: B --> C} :
isKernelCokernelPair i p → isKernelCokernelPair (M:=oppositePreAdditive M) p i.
Proof.
intros s.
split.
- exact (PairToCokernel s).
- exact (PairToKernel s).
Defined.
Lemma PairUniqueness1 {M :PreAdditive} {A A' B C:M} (i : A --> B) (i' : A' --> B) (p: B --> C) :
isKernelCokernelPair i p → isKernelCokernelPair i' p → iscontr (IsoArrowTo i i').
Proof.
intros [k _] [k' _]. exact (KernelUniqueness k k').
Defined.
Lemma PairUniqueness2 {M :PreAdditive} {A B C C':M} (i : A --> B) (p: B --> C) (p': B --> C') :
isKernelCokernelPair i p → isKernelCokernelPair i p' → iscontr (IsoArrowFrom p p').
Proof.
intros [_ c] [_ c']. exact (CokernelUniqueness c c').
Defined.
Lemma kerCokerDirectSum {M :PreAdditive} {A B:M} (S:BinDirectSum A B) : isKernelCokernelPair (to_In1 S) (to_Pr2 S).
Proof.
assert (E := BinDirectSum_isBinDirectSum M S).
split.
- ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
+ exact (h · to_Pr1 S).
+ refine (! assoc _ _ _ @ _ @ id_right _). rewrite <- (to_BinOpId' S).
rewrite rightDistribute. rewrite (assoc h (to_Pr2 S) (to_In2 S)).
rewrite H; clear H. rewrite zeroLeft. apply pathsinv0. apply (runax (T-->S)).
+ intros k. apply to_has_homsets.
+ clear H. intros k e. induction e. rewrite assoc'.
rewrite (to_IdIn1 S). apply pathsinv0, id_right.
- ∃ (to_Unel1 S). intros T h H. use unique_exists; cbn beta.
+ exact (ι₂ · h).
+ refine (assoc _ _ _ @ _ @ id_left h). rewrite <- (to_BinOpId' S).
rewrite leftDistribute.
rewrite <- (assoc (to_Pr1 S) (to_In1 S) h). rewrite H; clear H.
rewrite zeroRight. apply pathsinv0. apply (lunax (S-->T)).
+ intros k. apply to_has_homsets.
+ clear H. intros k e. induction e. rewrite assoc. rewrite (to_IdIn2 S).
exact (! id_left _).
Qed.
Lemma kerCoker10 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (identity A) (0 : A --> Z).
Proof.
exact (kerCokerDirectSum (TrivialDirectSum Z A)).
Qed.
Lemma kerCoker01 {M :PreAdditive} (Z:Zero M) (A:M) : isKernelCokernelPair (0 : Z --> A) (identity A).
Proof.
exact (kerCokerDirectSum (TrivialDirectSum' Z A)).
Qed.
Lemma PairPushoutMap {M :PreAdditive} {A B C A':M} {i : A --> B} {p : B --> C}
(pr : isKernelCokernelPair i p)
(r : A --> A') (po : Pushout i r) :
∑ (q : po --> C), PushoutIn1 po · q = p × PushoutIn2 po · q = 0.
Proof.
refine (iscontrpr1 (isPushout_Pushout po C p 0 _)).
refine (pr1 (PairToCokernel pr) @ ! _). apply zeroRight.
Qed.
Lemma PairPullbackMap {M :PreAdditive} {A B C A':M} {i : A <-- B} {p : B <-- C}
(pr : isKernelCokernelPair p i)
(r : A <-- A') (pb : Pullback i r) :
∑ (q : pb <-- C), PullbackPr1 pb ∘ q = p × PullbackPr2 pb ∘ q = 0.
Proof.
exact (PairPushoutMap (M:=oppositePreAdditive M) (opposite_isKernelCokernelPair pr) r pb).
Defined.
Lemma PairPushoutCokernel {M :PreAdditive} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isKernelCokernelPair i p)
(r : A --> A') (po : Pushout i r)
(j := PushoutIn2 po)
(pp := PairPushoutMap pr r po) :
isCokernel' j (pr1 pp).
Proof.
set (s := PushoutIn1 po).
induction pp as [q [e1 e2]]; change (isCokernel' j q);
change (hProptoType (s · q = p)) in e1;
change (hProptoType (j · q = 0)) in e2.
∃ e2.
intros T h e.
assert (L : i · (s · h) = 0).
{ refine (assoc _ _ _ @ _).
intermediate_path (r · j · h).
{ apply (maponpaths (λ s, s · h)). exact (PushoutSqrCommutes po). }
refine (! assoc _ _ _ @ _).
induction (!e).
apply zeroRight. }
assert (V := iscontrpr1 ((pr22 pr) T (s · h) L)); clear L.
induction V as [k e3].
use iscontraprop1.
{ apply invproofirrelevance; intros φ φ'.
apply subtypePath_prop.
induction φ as [φ e4]; induction φ' as [φ' e5]; cbn.
use (_ : isEpi q).
{ apply (isEpi_precomp M s q). rewrite e1. apply (CokernelIsEpi i p). apply pr. }
exact (e4 @ ! e5). }
∃ k.
use (MorphismsOutofPushoutEqual (isPushout_Pushout po)); fold s j.
{ refine (assoc _ _ _ @ _ @ e3). apply (maponpaths (λ s, s · k)). exact e1. }
{ refine (assoc _ _ _ @ _ @ ! e). rewrite e2. apply zeroLeft. }
Qed.
Lemma PairPullbackKernel {M : PreAdditive} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isKernelCokernelPair p i)
(r : A <-- A') (pb : Pullback i r)
(j := PullbackPr2 pb)
(pp := PairPullbackMap pr r pb) :
isKernel' (pr1 pp) j.
Proof.
exact (PairPushoutCokernel (M:=oppositePreAdditive M) i p (opposite_isKernelCokernelPair pr) r pb).
Defined.
Lemma SumOfKernelCokernelPairs {M : PreAdditive} {x y z X Y Z : M}
(xX : BinDirectSum x X) (yY : BinDirectSum y Y) (zZ : BinDirectSum z Z)
{f : x --> y} {g : y --> z} {f' : X --> Y} {g' : Y --> Z}
: isKernelCokernelPair f g → isKernelCokernelPair f' g' → isKernelCokernelPair (directSumMap xX yY f f') (directSumMap yY zZ g g').
Proof.
intros i i'.
∃ (SumOfKernels _ _ _ f g f' g' (pr1 i) (pr1 i')).
exact (SumOfCokernels _ _ _ f g f' g' (pr2 i) (pr2 i')).
Qed.
End KernelCokernelPairs.
Section theDefinition.
Definition ExactCategoryData := ∑ M:AdditiveCategory, MorphismPair M → hProp. Coercion ExactCategoryDataToAdditiveCategory (ME : ExactCategoryData) : AdditiveCategory := pr1 ME.
Definition isExact {M : ExactCategoryData} (E : MorphismPair M) : hProp := pr2 M E.
Definition isExact2 {M : ExactCategoryData} {A B C:M} (f:A-->B) (g:B-->C) := isExact (make_MorphismPair f g).
Definition isAdmissibleMonomorphism {M : ExactCategoryData} {A B:M} (i : A --> B) : hProp :=
∃ C (p : B --> C), isExact2 i p.
Definition AdmissibleMonomorphism {M : ExactCategoryData} (A B:M) : Type :=
∑ (i : A --> B), isAdmissibleMonomorphism i.
Coercion AdmMonoToMap {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → A --> B := pr1.
Coercion AdmMonoToMap' {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B → (A --> B)%cat := pr1.
Definition isAdmissibleEpimorphism {M : ExactCategoryData} {B C:M} (p : B --> C) : hProp :=
∃ A (i : A --> B), isExact2 i p.
Definition AdmissibleEpimorphism {M : ExactCategoryData} (B C:M) : Type :=
∑ (p : B --> C), isAdmissibleEpimorphism p.
Coercion AdmEpiToMap {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → B --> C := pr1.
Coercion AdmEpiToMap' {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C → (B --> C)%cat := pr1.
Lemma ExactToAdmMono {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleMonomorphism i.
Proof.
intros e. exact (hinhpr(C,,p,,e)).
Qed.
Lemma ExactToAdmEpi {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isAdmissibleEpimorphism p.
Proof.
intros e. exact (hinhpr(A,,i,,e)).
Qed.
The following definition is definition 2.1 from the paper of Bühler.
Local Definition ExactCategoryProperties (M : ExactCategoryData) : hProp :=
((∀ (P Q : MorphismPair M), MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q) ∧
(∀ (P Q : MorphismPair M), MorphismPairIsomorphism Q P ⇒ isExact P ⇒ isExact Q)) ∧
((∀ A:M, isAdmissibleMonomorphism (identity A)) ∧
(∀ A:M, isAdmissibleEpimorphism (identity A))) ∧
(∀ P : MorphismPair M, isExact P ⇒ isKernelCokernelPair (Mor1 P) (Mor2 P)) ∧
((∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleMonomorphism f ⇒ isAdmissibleMonomorphism g ⇒
isAdmissibleMonomorphism (f · g)) ∧
(∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g))) ∧
((∀ (A B C:M) (f : A --> B) (g : C --> B),
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)) ∧
(∀ (A B C:M) (f : B --> A) (g : B --> C),
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO))).
((∀ (P Q : MorphismPair M), MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q) ∧
(∀ (P Q : MorphismPair M), MorphismPairIsomorphism Q P ⇒ isExact P ⇒ isExact Q)) ∧
((∀ A:M, isAdmissibleMonomorphism (identity A)) ∧
(∀ A:M, isAdmissibleEpimorphism (identity A))) ∧
(∀ P : MorphismPair M, isExact P ⇒ isKernelCokernelPair (Mor1 P) (Mor2 P)) ∧
((∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleMonomorphism f ⇒ isAdmissibleMonomorphism g ⇒
isAdmissibleMonomorphism (f · g)) ∧
(∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g))) ∧
((∀ (A B C:M) (f : A --> B) (g : C --> B),
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)) ∧
(∀ (A B C:M) (f : B --> A) (g : B --> C),
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO))).
The following definition is from Higher Algebraic K-theory I, by Quillen.
We prove below that the two definitions are equivalent.
Local Definition ExactCategoryProperties_Quillen (M : ExactCategoryData) : hProp :=
(∀ (P Q:MorphismPair M), MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q) ∧
(∀ (A B:M) (AB:BinDirectSum A B), isExact2 (to_In1 AB) (to_Pr2 AB)) ∧
(∀ P : MorphismPair M, isExact P ⇒ isKernel' (Mor1 P) (Mor2 P) ∧ isCokernel' (Mor1 P) (Mor2 P)) ∧
((∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleMonomorphism f ⇒ isAdmissibleMonomorphism g ⇒
isAdmissibleMonomorphism (f · g)) ∧
(∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g))) ∧
((∀ (A B C:M) (f : A --> B) (g : C --> B),
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)) ∧
(∀ (A B C:M) (f : B --> A) (g : B --> C),
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO))) ∧
((∀ (A B C:M) (i:A-->B) (j:B-->C),
hasCokernel i ⇒ isAdmissibleMonomorphism (i·j) ⇒ isAdmissibleMonomorphism i) ∧
(∀ (A B C:M) (i:A-->B) (j:B-->C),
hasKernel j ⇒ isAdmissibleEpimorphism (i·j) ⇒ isAdmissibleEpimorphism j)).
Definition ExactCategory := ∑ (ME:ExactCategoryData), ExactCategoryProperties ME.
Coercion ExactCategoryToData (M:ExactCategory) : ExactCategoryData := pr1 M.
Definition make_ExactCategory (ME:ExactCategoryData) (p : ExactCategoryProperties ME) : ExactCategory := ME,,p.
Definition isExactFunctor {M N:ExactCategory} (F : M ⟶ N) : hProp
:= ∀ (P : MorphismPair M), isExact P ⇒ isExact (applyFunctorToPair F P).
Definition ExactFunctor (M N:ExactCategory)
:= ∑ F : M ⟶ N, isExactFunctor F.
Coercion ExactFunctorToFunctor {M N:ExactCategory}
: ExactFunctor M N → (M ⟶ N)
:= pr1.
Definition ShortExactSequence (M:ExactCategory) := ∑ (P : MorphismPair M), isExact P.
Coercion ShortExactSequenceToMorphismPair {M:ExactCategory} (P : ShortExactSequence M)
: MorphismPair M
:= pr1 P.
Definition ShortExactSequenceMap {M:ExactCategory} (P Q:ShortExactSequence M) := MorphismPairMap P Q.
Definition applyFunctorToShortExactSequence {M N:ExactCategory} (F : ExactFunctor M N) :
ShortExactSequence M → ShortExactSequence N.
Proof.
intros E. ∃ (applyFunctorToPair F E).
induction E as [E iE]. unfold ShortExactSequenceToMorphismPair,pr1.
exact (pr2 F E iE).
Defined.
Definition composeExactFunctors {L M N:ExactCategory} : ExactFunctor L M → ExactFunctor M N → ExactFunctor L N.
Proof.
intros F G. ∃ (F ∙ G). exact (λ E e, pr2 G _ (pr2 F E e)).
Defined.
End theDefinition.
Declare Scope excat.
Delimit Scope excat with excat.
Local Open Scope excat.
Notation "A ↣ B" := (AdmissibleMonomorphism A B) : excat.
Notation "B ↠ C" := (AdmissibleEpimorphism B C) : excat.
Notation "F ∙ G" := (composeExactFunctors F G) : excat.
Notation "M ⟶ N" := (ExactFunctor M N) : excat.
Section ExactCategoryAccessFunctions.
Context {M:ExactCategory}.
Definition EC_IsomorphicToExact {P Q:MorphismPair M}
: MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q
:= pr112 M P Q.
Definition EC_IsomorphicToExact' {P Q:MorphismPair M}
: MorphismPairIsomorphism Q P ⇒ isExact P ⇒ isExact Q
:= pr212 M P Q.
Definition EC_IdentityIsMono (A:M) : isAdmissibleMonomorphism (identity A)
:= pr1 (pr122 M) A.
Definition IdentityMono (A:M) : AdmissibleMonomorphism A A
:= identity A,, EC_IdentityIsMono A.
Definition EC_IdentityIsEpi (A:M) : isAdmissibleEpimorphism (identity A)
:= pr2 (pr122 M) A.
Definition IdentityEpi (A:M) : AdmissibleEpimorphism A A
:= identity A,, EC_IdentityIsEpi A.
Definition EC_ExactToKernelCokernel {P : MorphismPair M} :
isExact P ⇒ isKernelCokernelPair (Mor1 P) (Mor2 P)
:= pr12 (pr22 M) P.
Definition EC_ExactToKernel {P : MorphismPair M} :
isExact P ⇒ isKernel' (Mor1 P) (Mor2 P)
:= λ i, (pr1 (EC_ExactToKernelCokernel i)).
Definition EC_ExactToCokernel {P : MorphismPair M} :
isExact P ⇒ isCokernel' (Mor1 P) (Mor2 P)
:= λ i, (pr2 (EC_ExactToKernelCokernel i)).
Definition EC_ComposeMono {A B C:M} (f : A --> B) (g : B --> C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism g →
isAdmissibleMonomorphism (f · g)
:= pr112 (pr222 M) A B C f g.
Definition EC_ComposeEpi {A B C:M} (f : A --> B) (g : B --> C) :
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g)
:= pr212 (pr222 M) A B C f g.
Definition EC_PullbackEpi {A B C:M} (f : A --> B) (g : C --> B) :
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)
:= pr122 (pr222 M) A B C f g.
Definition EC_PushoutMono {A B C:M} (f : B --> A) (g : B --> C) :
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO)
:= pr222 (pr222 M) A B C f g.
End ExactCategoryAccessFunctions.
Section OppositeExactCategory.
Definition oppositeExactCategoryData (M:ExactCategoryData) : ExactCategoryData.
Proof.
∃ (oppositeAdditiveCategory M). exact (λ p, @isExact M (opp_MorphismPair p)).
Defined.
Definition oppositeExactCategory (M:ExactCategory) : ExactCategory.
Proof.
use (make_ExactCategory (oppositeExactCategoryData M)).
split.
{ split;intros P Q f.
- exact (EC_IsomorphicToExact' (opp_MorphismPairIsomorphism f)).
- exact (EC_IsomorphicToExact (opp_MorphismPairIsomorphism f)). }
split.
{ split.
- exact EC_IdentityIsEpi.
- exact EC_IdentityIsMono. }
split.
{ intros P i. exact (opposite_isKernelCokernelPair (EC_ExactToKernelCokernel i)). }
split.
{ split.
{ intros A B C f g i j. exact (@EC_ComposeEpi M C B A g f j i). }
{ intros A B C f g i j. exact (@EC_ComposeMono M C B A g f j i). } }
{ split.
{ exact (@EC_PushoutMono M). }
{ exact (@EC_PullbackEpi M). } }
Defined.
End OppositeExactCategory.
Notation "C '^op'" := (oppositeExactCategory C) (at level 3, format "C ^op") : excat.
Section ExactCategoryFacts.
Lemma ExactToMono {M : ExactCategory} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isMonic i.
Proof.
intros e. exact (KernelIsMonic i p (EC_ExactToKernel e)).
Qed.
Lemma ExactToEpi {M : ExactCategory} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isEpi p.
Proof.
intros e. refine (CokernelIsEpi i p (EC_ExactToCokernel e)).
Qed.
Lemma ExactSequenceFromMono {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) :
isCokernel' i p → isAdmissibleMonomorphism i → isExact2 i p.
Proof.
intros co mo. apply (squash_to_hProp mo); clear mo; intros [C' [p' e]].
assert (co' := pr2 (EC_ExactToKernelCokernel e) : isCokernel' i p').
assert (R := iscontrpr1 (CokernelUniqueness co' co)). induction R as [R r].
use (EC_IsomorphicToExact _ e).
∃ (identity_z_iso _). ∃ (identity_z_iso _). ∃ R.
split.
- split.
+ exact (id_left _ @ ! id_right _).
+ exact (id_right _ @ ! id_left _).
- split.
+ exact (id_left _ @ ! r).
+ exact (r @ !id_left _).
Qed.
Lemma ExactSequenceFromEpi {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) :
isKernel' i p → isAdmissibleEpimorphism p → isExact2 i p.
Proof.
exact (ExactSequenceFromMono (M:=M^op) p i).
Defined.
Lemma ExactSequence10 {M : ExactCategory} (A:M) (Z:Zero M) : isExact2 (identity A) (0 : A --> Z).
Proof.
exact (ExactSequenceFromMono _ _ (pr2 (kerCoker10 Z A)) (EC_IdentityIsMono A)).
Qed.
Lemma ExactSequence01 {M : ExactCategory} (A:M) (Z:Zero M) : isExact2 (0 : Z --> A) (identity A).
Proof.
exact (ExactSequenceFromEpi _ _ (pr1 (kerCoker01 Z A)) (EC_IdentityIsEpi A)).
Qed.
Lemma FromZeroIsMono {M : ExactCategory} (Z:Zero M) (A:M) : isAdmissibleMonomorphism (0 : Z --> A).
Proof.
apply hinhpr. ∃ A. ∃ (identity A). use ExactSequence01.
Defined.
Definition MonoFromZero {M : ExactCategory} (Z:Zero M) (A:M) : Z ↣ A
:= (0 : Z --> A),,FromZeroIsMono Z A.
Lemma ToZeroIsEpi {M : ExactCategory} (A:M) (Z:Zero M) : isAdmissibleEpimorphism (0 : A --> Z).
Proof.
apply hinhpr. ∃ A. ∃ (identity A). use ExactSequence10.
Defined.
Definition EpiToZero {M : ExactCategory} (A:M) (Z:Zero M) : A ↠ Z
:= (0 : A --> Z),,ToZeroIsEpi A Z.
Goal ∏ (M:ExactCategory) (A:M) (Z:Zero M), EpiToZero A Z = MonoFromZero (M:=M^op) (Zero_opp M Z) A.
Abort.
Lemma IsomMono1 {M : ExactCategory} {A B B':M} (f : A --> B) (f' : A --> B') :
IsoArrowFrom f f' → isAdmissibleMonomorphism f → isAdmissibleMonomorphism f'.
Proof.
intros [i I] E. apply (squash_to_hProp E); clear E; intros [C [p E]].
apply hinhpr. ∃ C. ∃ (z_iso_inv i · p). use (EC_IsomorphicToExact _ E).
∃ (identity_z_iso A). ∃ i. ∃ (identity_z_iso C). split; cbn.
- split.
+ exact (id_left _ @ ! I).
+ exact (I @ ! id_left _).
- split.
+ refine (assoc _ _ _ @ _ @ id_left _ @ ! id_right _).
apply (maponpaths (λ k, k · p)). apply z_iso_inv_after_z_iso.
+ apply pathsinv0.
refine (assoc _ _ _ @ _ @ id_left _ @ ! id_right _).
apply (maponpaths (λ k, k · p)). apply z_iso_inv_after_z_iso.
Qed.
Lemma IsomEpi1 {M : ExactCategory} {A A' B:M} (f : A --> B) (f' : A' --> B) :
IsoArrowTo f' f → isAdmissibleEpimorphism f → isAdmissibleEpimorphism f'.
Proof.
intros i e.
exact (IsomMono1 (M:=M^op) f f' (opposite_IsoArrowTo i) e).
Defined.
Lemma IsomMono {M : ExactCategory} {A A' B B':M} (f : A --> B) (f' : A' --> B') :
IsoArrow f f' → isAdmissibleMonomorphism f → isAdmissibleMonomorphism f'.
Proof.
intros [g [h e]] i. apply (squash_to_hProp i); clear i; intros [C [p E]].
apply hinhpr. ∃ C. ∃ (z_iso_inv h · p). use (EC_IsomorphicToExact _ E).
simple refine (make_MorphismPairIsomorphism
(make_MorphismPair f p) (make_MorphismPair f' (z_iso_inv h · p))
g h (identity_z_iso C) e _).
refine (assoc _ _ _ @ maponpaths (postcomp_with p) _ @ id_left p @ ! id_right p).
apply z_iso_inv_after_z_iso.
Qed.
Lemma IsomEpi {M : ExactCategory} {A A' B B':M} (f : A --> B) (f' : A' --> B') :
IsoArrow f' f → isAdmissibleEpimorphism f → isAdmissibleEpimorphism f'.
Proof.
intros i.
exact (IsomMono (M:=M^op) f f' (opposite_IsoArrow _ _ i)).
Defined.
Lemma PullbackEpiIsEpi {M : ExactCategory} {A B C:M} (f : A --> B) (g : C --> B)
(pb : Pullback f g) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (PullbackPr2 pb).
Proof.
intros fepi.
assert (qb := EC_PullbackEpi f g fepi).
apply (squash_to_hProp qb); clear qb; intros [qb epi2].
assert (I := pullbackiso2 pb qb).
apply (IsomEpi1 _ _ I). exact epi2.
Qed.
Lemma IsPullbackEpiIsEpi {M : ExactCategory} {P A B C:M} {f : A --> B} {g : C --> B}
{h : P --> A} {k : P --> C} :
isPullback' (M:=M) f g h k → isAdmissibleEpimorphism f → isAdmissibleEpimorphism k.
Proof.
intros pb. exact (PullbackEpiIsEpi f g (make_Pullback _ _ _ _ _ _ (pr2 pb))).
Qed.
Lemma IsIsoIsMono {M : ExactCategory} {A B:M} (f:A-->B) :
is_z_isomorphism f → isAdmissibleMonomorphism f.
Proof.
intros i.
use (IsomMono1 (identity A)).
- use tpair.
+ exact (f,,i).
+ cbn. apply id_left.
- apply EC_IdentityIsMono.
Qed.
Lemma IsoIsMono {M : ExactCategory} {A B:M} (f:z_iso A B) : isAdmissibleMonomorphism (z_iso_mor f).
Proof.
use IsIsoIsMono. apply f.
Qed.
Definition IsoToAdmMono {M : ExactCategory} {A B:M} (f:z_iso A B) : AdmissibleMonomorphism A B
:= z_iso_mor f,,IsoIsMono f.
Lemma IsoIsEpi {M : ExactCategory} {A B:M} (f:z_iso A B) : isAdmissibleEpimorphism (z_iso_mor f).
Proof.
exact (IsoIsMono (M:=M^op) (opp_z_iso f)).
Defined.
Definition IsoToAdmEpi {M : ExactCategory} {A B:M} (f:z_iso A B) : AdmissibleEpimorphism A B
:= z_iso_mor f,,IsoIsEpi f.
Lemma DirectSumToExact {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isExact2 (to_In1 S) (to_Pr2 S).
Proof.
use ExactSequenceFromEpi.
{ exact (PairToKernel (kerCokerDirectSum S)). }
apply (squash_to_hProp (to_hasZero M)); intros Z.
set (pb := DirectSumToPullback S Z).
change (isAdmissibleEpimorphism (PullbackPr2 pb)).
assert (Q := EC_PullbackEpi (0 : A --> Z) (0 : B --> Z) (ToZeroIsEpi A Z)).
apply (squash_to_hProp Q); clear Q; intros [pb' R'].
exact (IsomEpi1 (PullbackPr2 pb') (PullbackPr2 pb) (pullbackiso2 pb pb') R').
Qed.
Lemma DirectSumToExact' {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isExact2 (to_In2 S) (to_Pr1 S).
Proof.
exact (DirectSumToExact (reverseBinDirectSum S)).
Qed.
Lemma In1IsAdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleMonomorphism (ι₁ : A --> S).
Proof.
exact (hinhpr (B,,to_Pr2 S,,DirectSumToExact S)).
Qed.
Lemma In2IsAdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleMonomorphism (ι₂ : B --> S).
Proof.
exact (hinhpr (A,,to_Pr1 S,,DirectSumToExact' S)).
Qed.
Lemma Pr1IsAdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleEpimorphism (π₁ : S --> A).
Proof.
exact (hinhpr (B,,to_In2 S,,DirectSumToExact' S)).
Qed.
Lemma Pr2IsAdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleEpimorphism (π₂ : S --> B).
Proof.
exact (hinhpr (A,,to_In1 S,,DirectSumToExact S)).
Qed.
Definition In1AdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleMonomorphism A S := ι₁ ,, In1IsAdmMono S.
Definition In2AdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleMonomorphism B S := ι₂ ,, In2IsAdmMono S.
Definition Pr1AdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleEpimorphism S A := π₁ ,, Pr1IsAdmEpi S.
Definition Pr2AdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleEpimorphism S B := π₂ ,, Pr2IsAdmEpi S.
Definition TrivialExactSequence {M : ExactCategory} (A:M) (Z:Zero M) : ShortExactSequence M.
Proof.
assert (Q := DirectSumToExact (TrivialDirectSum Z A)).
exact (make_MorphismPair ι₁ π₂,, Q).
Defined.
Definition TrivialExactSequence' {M : ExactCategory} (Z:Zero M) (A:M) : ShortExactSequence M.
Proof.
assert (Q := DirectSumToExact (TrivialDirectSum' Z A)).
exact (make_MorphismPair ι₁ π₂,, Q).
Defined.
Lemma ExactPushout {M : ExactCategory} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isExact2 i p) (r : A --> A') :
∃ (po : Pushout i r),
isExact2 (PushoutIn2 po) (pr1 (PairPushoutMap (EC_ExactToKernelCokernel pr) r po)).
Proof.
assert (I := ExactToAdmMono pr).
assert (R := EC_PushoutMono i r I).
apply (squash_to_hProp R); clear R; intros [po J]; apply hinhpr.
∃ po. use ExactSequenceFromMono.
{ exact (PairPushoutCokernel i p (EC_ExactToKernelCokernel pr) r po). }
exact J.
Qed.
Lemma ExactPushout' {M : ExactCategory} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isExact2 i p) (r : A --> A') :
∃ (B':M) (i':A'-->B') (s:B-->B') (p':B'-->C),
s·p' = p ∧ isPushout' (M:=M) i r s i' ∧ isExact2 i' p'.
Proof.
assert (I := ExactToAdmMono pr). assert (R := EC_PushoutMono i r I).
use (hinhfun _ R); clear R; intros [po J].
set (pomap := PairPushoutMap (EC_ExactToKernelCokernel pr) r po).
set (p' := pr1 pomap).
∃ po. ∃ (PushoutIn2 po). ∃ (PushoutIn1 po). ∃ p'.
split.
{ exact (pr12 pomap). }
split.
{ apply Pushout_to_isPushout'. }
{ use ExactSequenceFromMono.
{ exact (PairPushoutCokernel i p (EC_ExactToKernelCokernel pr) r po). }
exact J. }
Qed.
Lemma ExactPullback {M : ExactCategory} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isExact2 p i)
(r : A <-- A') :
∃ (pb : Pullback i r),
isExact2 (pr1 (PairPullbackMap (EC_ExactToKernelCokernel pr) r pb)) (PullbackPr2 pb).
Proof.
assert (I := hinhpr (C ,, p ,, pr) : isAdmissibleEpimorphism i).
assert (R := EC_PullbackEpi i r I).
apply (squash_to_hProp R); clear R; intros [pb J]; apply hinhpr.
∃ pb. use ExactSequenceFromEpi.
{ exact (PairPullbackKernel i p (EC_ExactToKernelCokernel pr) r pb). }
exact J.
Qed.
Lemma ExactPullback' {M : ExactCategory} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isExact2 p i) (r : A <-- A') :
∃ (B':M) (i':A'<--B') (s:B<--B') (p':B'<--C),
s∘p' = p ∧ isPullback' (M:=M) i r s i' ∧ isExact2 p' i'.
Proof.
assert (I := ExactToAdmEpi pr). assert (R := EC_PullbackEpi i r I).
use (hinhfun _ R); clear R; intros [pb J].
set (pbmap := PairPullbackMap (EC_ExactToKernelCokernel pr) r pb).
set (p' := pr1 pbmap).
∃ pb. ∃ (PullbackPr2 pb). ∃ (PullbackPr1 pb). ∃ p'.
split.
{ exact (pr12 pbmap). }
split.
{ apply Pullback_to_isPullback'. }
{ use ExactSequenceFromEpi.
{ exact (PairPullbackKernel i p (EC_ExactToKernelCokernel pr) r pb). }
exact J. }
Qed.
Lemma MonicAdmEpiIsIso {M : ExactCategory} {A B:M} (p : A ↠ B) : isMonic p → is_z_isomorphism p.
Proof.
induction p as [p E]. cbn. intros I. apply (squash_to_prop E).
{ apply isaprop_is_z_isomorphism. apply to_has_homsets. }
clear E; intros [K [i E]].
assert (Q := EC_ExactToKernelCokernel E); clear E.
induction Q as [ke co];
change (hProptoType (isKernel' i p)) in ke;
change (hProptoType (isCokernel' i p)) in co.
assert (Q : i = 0).
{ use (I K i 0). exact (pr1 ke @ ! zeroLeft _). }
clear I ke. induction (!Q); clear Q. exact (CokernelOfZeroMapIsIso p co).
Qed.
Lemma EpiAdmMonoIsIso {M : ExactCategory} {A B:M} (i : A ↣ B) : isEpi i → is_z_isomorphism i.
Proof.
intros e.
exact (opp_is_z_isomorphism _ (MonicAdmEpiIsIso (M:=M^op) i e)).
Defined.
Lemma MonoPlusIdentity {M : ExactCategory} {A B:M}
(f:A-->B) (C:M) (AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism (directSumMap AC BC f (identity C)).
Proof.
intro i. apply (squash_to_hProp i). intros [D [p j]].
apply hinhpr. ∃ D. ∃ (π₁ · p). apply ExactSequenceFromEpi.
2:{ apply EC_ComposeEpi.
- apply Pr1IsAdmEpi.
- exact (hinhpr(A,,f,,j)). }
apply (squash_to_hProp (to_hasZero M)); intros Z.
apply (squash_to_hProp (to_hasBinDirectSums D Z)); intros DZ.
assert (m := pr1 (SumOfKernelCokernelPairs AC BC DZ
(EC_ExactToKernelCokernel j : isKernelCokernelPair f p)
(kerCoker10 Z C : isKernelCokernelPair (identity C) 0))).
assert (R : directSumMap BC DZ p 0 · to_Pr1 DZ = to_Pr1 BC · p).
{ apply directSumMapEqPr1. }
induction R. apply IsoWithKernel.
{ exact m. }
∃ (ι₁). split.
{ refine (! runax (_ --> _) _ @ ! _ @ to_BinOpId'' _). apply maponpaths. apply ThroughZeroIsZero. }
{ refine (to_IdIn1 DZ). }
Qed.
Lemma EpiPlusIdentity {M : ExactCategory} {A B:M} (f:A-->B) (C:M) (AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (directSumMap AC BC f (identity C)).
Proof.
intro i. rewrite <- opposite_directSumMap'.
exact (MonoPlusIdentity (M:=M^op) f C (oppositeBinDirectSum BC) (oppositeBinDirectSum AC) i).
Defined.
Lemma IdentityPlusMono {M : ExactCategory} {B C:M} (A:M) (f:B-->C)
(AB : BinDirectSum A B) (AC : BinDirectSum A C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism (directSumMap AB AC (identity A) f).
Proof.
intros i. use (IsomMono (directSumMap (reverseBinDirectSum AB) (reverseBinDirectSum AC) f (identity A)) (directSumMap AB AC (identity A) f)).
- ∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
- apply MonoPlusIdentity. exact i.
Defined.
Lemma IdentityPlusEpi {M : ExactCategory} {B C:M} (A:M) (f:B-->C)
(AB : BinDirectSum A B) (AC : BinDirectSum A C) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (directSumMap AB AC (identity A) f).
Proof.
intros i. use (IsomEpi (directSumMap (reverseBinDirectSum AB) (reverseBinDirectSum AC) f (identity A)) (directSumMap AB AC (identity A) f)).
- ∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
- apply EpiPlusIdentity. exact i.
Defined.
Lemma SumOfExactSequences {M:ExactCategory} {A B C A' B' C':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B') (CC' : BinDirectSum C C')
{f : A --> B} {g : B --> C} {f' : A' --> B'} {g' : B' --> C'} :
isExact2 f g → isExact2 f' g' → isExact2 (directSumMap AA' BB' f f') (directSumMap BB' CC' g g').
Proof.
intros i i'. apply ExactSequenceFromMono.
{ use SumOfCokernels.
- exact (EC_ExactToCokernel i).
- exact (EC_ExactToCokernel i'). }
apply (squash_to_hProp (to_hasBinDirectSums A B')); intros AB'.
set (j := directSumMap AB' BB' f (identity B')).
set (k := directSumMap AA' AB' (identity A) f').
assert (kj : k · j = directSumMap AA' BB' f f').
{ apply ToBinDirectSumUnique.
- refine (! assoc _ _ _ @ _). intermediate_path (k · (π₁ · f)).
+ apply maponpaths. apply directSumMapEqPr1.
+ refine (assoc _ _ _ @ _). apply (maponpaths (postcomp_with _)).
exact (directSumMapEqPr1 @ id_right _).
- refine (! assoc _ _ _ @ _). intermediate_path (k · (π₂ · (identity B'))).
+ apply maponpaths. apply directSumMapEqPr2.
+ refine (assoc _ _ _ @ id_right _ @ _). apply directSumMapEqPr2. }
induction kj. use (EC_ComposeMono k j).
- apply IdentityPlusMono. exact (ExactToAdmMono i').
- apply MonoPlusIdentity. exact (ExactToAdmMono i).
Qed.
Lemma AdmMonoEnlargement {M:ExactCategory} {A B C:M}
(BC : BinDirectSum B C) (i:A-->B) (f:A-->C) :
isAdmissibleMonomorphism i → isAdmissibleMonomorphism (ToBinDirectSum BC i f).
Proof.
intros I.
apply (squash_to_hProp (to_hasBinDirectSums A C)); intros AC.
assert (e : ToBinDirectSum BC i f = ι₁ · (1 + π₁·f·ι₂) · (directSumMap AC _ i 1)).
{ apply ToBinDirectSumsEq.
- rewrite BinDirectSumPr1Commutes. rewrite assoc'. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes.
rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute.
rewrite id_right. rewrite (to_IdIn1 AC). rewrite id_left.
refine (! runax (A-->B) _ @ _). apply maponpaths. rewrite assoc.
rewrite (assoc' _ _ π₁). rewrite (to_Unel2 AC). unfold to_unel.
rewrite zeroRight, zeroLeft. reflexivity.
- rewrite BinDirectSumPr2Commutes. rewrite assoc'. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite BinDirectSumPr2Commutes.
rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute.
rewrite 2 id_right. rewrite (to_Unel1 AC). unfold to_unel.
rewrite lunax. rewrite id_right. rewrite 2 assoc.
rewrite (to_IdIn1 AC). rewrite id_left.
rewrite assoc'. rewrite (to_IdIn2 AC). rewrite id_right. reflexivity. }
induction (!e); clear e.
apply EC_ComposeMono.
- apply EC_ComposeMono.
+ apply In1IsAdmMono.
+ apply IsIsoIsMono. apply elem21_isiso.
- now apply MonoPlusIdentity.
Qed.
Lemma SumOfAdmissibleEpis {M:ExactCategory} {A B A' B':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B')
(f : A --> B) (f' : A' --> B') :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism f' → isAdmissibleEpimorphism (directSumMap AA' BB' f f').
Proof.
intros e e'.
apply (squash_to_hProp e); clear e; intros [C [g e]].
apply (squash_to_hProp e'); clear e'; intros [C' [g' e']].
apply (squash_to_hProp (to_hasBinDirectSums C C')); intros CC'.
exact (ExactToAdmEpi (SumOfExactSequences CC' _ _ e e')).
Qed.
Lemma SumOfAdmissibleMonos {M:ExactCategory} {A B A' B':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B')
(f : A --> B) (f' : A' --> B') :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism f' → isAdmissibleMonomorphism (directSumMap AA' BB' f f').
Proof.
intros e e'.
apply (squash_to_hProp e); clear e; intros [C [g e]].
apply (squash_to_hProp e'); clear e'; intros [C' [g' e']].
apply (squash_to_hProp (to_hasBinDirectSums C C')); intros CC'.
exact (ExactToAdmMono (SumOfExactSequences _ _ CC' e e')).
Qed.
Lemma MapPlusIdentityToCommSq {M:ExactCategory} {A B:M}
(f:A-->B) (C:M)
(AC : BinDirectSum A C) (BC : BinDirectSum B C) :
f · ι₁ = ι₁ · (directSumMap AC BC f (identity C)).
Proof.
apply ToBinDirectSumsEq.
- rewrite assoc'. rewrite (to_IdIn1 BC). rewrite id_right. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite assoc'. rewrite BinDirectSumPr1Commutes.
rewrite assoc. rewrite (to_IdIn1 AC). rewrite id_left. reflexivity.
- rewrite assoc'. rewrite (to_Unel1 BC). unfold to_unel. rewrite zeroRight.
unfold directSumMap, BinDirectSumIndAr. rewrite assoc'.
rewrite BinDirectSumPr2Commutes. rewrite id_right. apply pathsinv0.
use (to_Unel1 AC).
Qed.
Lemma KernelPlusIdentity {M:ExactCategory} {A B C:M}
(f:A-->B) (g:B-->C) (D:M)
(BD : BinDirectSum B D) (CD : BinDirectSum C D) :
isKernel' (f · ι₁) (directSumMap BD CD g (identity D)) → isKernel' f g.
Proof.
intros K. apply makeMonicKernel.
- exact (isMonic_postcomp _ _ _ (KernelIsMonic _ _ K)).
- use (to_In1_isMonic _ CD). rewrite zeroLeft. rewrite assoc'.
assert (Q := pr1 K); simpl in Q. rewrite assoc' in Q.
rewrite directSumMapEqIn1 in Q. exact Q.
- intros T h eqn.
assert (E : h · ι₁ · directSumMap BD CD g (identity D) = 0).
{ rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc.
refine (maponpaths (λ r, r·ι₁) eqn @ _). apply zeroLeft. }
assert (Q := iscontrpr1 (pr2 K T (h·ι₁) E)); simpl in Q.
induction Q as [p e].
∃ p.
rewrite assoc in e.
apply (to_In1_isMonic _ _ _ _ _ e).
Qed.
Lemma CokernelPlusIdentity {M:ExactCategory} {A B C:M} (f:A-->B) (g:B-->C) (D:M)
(BD : BinDirectSum B D) (CD : BinDirectSum C D):
isCokernel' f g →
isCokernel' (f · ι₁) (directSumMap BD CD g (identity D)).
Proof.
intros ic.
split.
{ rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc. rewrite (pr1 ic). apply zeroLeft. }
intros T h u.
apply iscontraprop1.
{ apply invproofirrelevance. intros [r r'] [s s']. apply subtypePath_prop; cbn.
assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq.
- assert (L := maponpaths (λ w, ι₁ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L.
rewrite directSumMapEqIn1 in L.
rewrite 2 assoc' in L. exact (CokernelIsEpi _ g ic _ _ _ L).
- assert (L := maponpaths (λ w, ι₂ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L.
rewrite directSumMapEqIn2 in L.
rewrite 2 assoc' in L. rewrite 2 id_left in L. exact L. }
assert (Q := iscontrpr1 (pr2 ic _ _ (assoc _ _ _ @ u))).
induction Q as [q Q].
∃ (π₁ · q + π₂ · ι₂ · h).
rewrite rightDistribute.
rewrite assoc. rewrite assoc. rewrite assoc.
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes,BinDirectSumPr2Commutes.
rewrite id_right.
rewrite assoc'. rewrite Q. rewrite assoc.
rewrite <- leftDistribute.
refine (_ @ id_left _).
apply (maponpaths (λ w, w·h)).
use to_BinOpId''.
Qed.
Lemma MapPlusIdentityToPullback {M:ExactCategory} {A B:M} (f:A-->B) (C:M)
(AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isPullback _ _ _ _ (MapPlusIdentityToCommSq f C AC BC).
Proof.
intros T g h e. apply iscontraprop1.
- apply invproofirrelevance. intros [p [P P']] [q [Q Q']].
apply subtypePath.
{ intros r. apply isapropdirprod; apply to_has_homsets. }
cbn. clear P Q.
refine (! id_right _ @ _ @ id_right _).
rewrite <- (to_IdIn1 AC). rewrite 2 assoc. induction (!P'), (!Q'). reflexivity.
- ∃ (h · π₁).
split.
+ refine (_ @ id_right _). rewrite <- (to_IdIn1 BC).
rewrite (assoc g). rewrite e. rewrite (assoc' h _ π₁).
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes.
rewrite assoc. reflexivity.
+ refine (_ @ id_right _). rewrite <- (to_BinOpId' AC).
rewrite rightDistribute. rewrite assoc. refine (! runax (Hom_add _ _ _) _ @ _).
apply maponpaths. rewrite assoc. apply pathsinv0.
assert (K : h · π₂ = 0).
{ refine ( _ @ maponpaths (λ w, w · π₂) (!e) @ _ ).
- rewrite assoc'.
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr2Commutes.
rewrite id_right. reflexivity.
- rewrite assoc'. rewrite (to_Unel1 BC). unfold to_unel.
apply zeroRight. }
rewrite K. apply zeroLeft.
Qed.
(∀ (P Q:MorphismPair M), MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q) ∧
(∀ (A B:M) (AB:BinDirectSum A B), isExact2 (to_In1 AB) (to_Pr2 AB)) ∧
(∀ P : MorphismPair M, isExact P ⇒ isKernel' (Mor1 P) (Mor2 P) ∧ isCokernel' (Mor1 P) (Mor2 P)) ∧
((∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleMonomorphism f ⇒ isAdmissibleMonomorphism g ⇒
isAdmissibleMonomorphism (f · g)) ∧
(∀ (A B C:M) (f : A --> B) (g : B --> C),
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g))) ∧
((∀ (A B C:M) (f : A --> B) (g : C --> B),
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)) ∧
(∀ (A B C:M) (f : B --> A) (g : B --> C),
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO))) ∧
((∀ (A B C:M) (i:A-->B) (j:B-->C),
hasCokernel i ⇒ isAdmissibleMonomorphism (i·j) ⇒ isAdmissibleMonomorphism i) ∧
(∀ (A B C:M) (i:A-->B) (j:B-->C),
hasKernel j ⇒ isAdmissibleEpimorphism (i·j) ⇒ isAdmissibleEpimorphism j)).
Definition ExactCategory := ∑ (ME:ExactCategoryData), ExactCategoryProperties ME.
Coercion ExactCategoryToData (M:ExactCategory) : ExactCategoryData := pr1 M.
Definition make_ExactCategory (ME:ExactCategoryData) (p : ExactCategoryProperties ME) : ExactCategory := ME,,p.
Definition isExactFunctor {M N:ExactCategory} (F : M ⟶ N) : hProp
:= ∀ (P : MorphismPair M), isExact P ⇒ isExact (applyFunctorToPair F P).
Definition ExactFunctor (M N:ExactCategory)
:= ∑ F : M ⟶ N, isExactFunctor F.
Coercion ExactFunctorToFunctor {M N:ExactCategory}
: ExactFunctor M N → (M ⟶ N)
:= pr1.
Definition ShortExactSequence (M:ExactCategory) := ∑ (P : MorphismPair M), isExact P.
Coercion ShortExactSequenceToMorphismPair {M:ExactCategory} (P : ShortExactSequence M)
: MorphismPair M
:= pr1 P.
Definition ShortExactSequenceMap {M:ExactCategory} (P Q:ShortExactSequence M) := MorphismPairMap P Q.
Definition applyFunctorToShortExactSequence {M N:ExactCategory} (F : ExactFunctor M N) :
ShortExactSequence M → ShortExactSequence N.
Proof.
intros E. ∃ (applyFunctorToPair F E).
induction E as [E iE]. unfold ShortExactSequenceToMorphismPair,pr1.
exact (pr2 F E iE).
Defined.
Definition composeExactFunctors {L M N:ExactCategory} : ExactFunctor L M → ExactFunctor M N → ExactFunctor L N.
Proof.
intros F G. ∃ (F ∙ G). exact (λ E e, pr2 G _ (pr2 F E e)).
Defined.
End theDefinition.
Declare Scope excat.
Delimit Scope excat with excat.
Local Open Scope excat.
Notation "A ↣ B" := (AdmissibleMonomorphism A B) : excat.
Notation "B ↠ C" := (AdmissibleEpimorphism B C) : excat.
Notation "F ∙ G" := (composeExactFunctors F G) : excat.
Notation "M ⟶ N" := (ExactFunctor M N) : excat.
Section ExactCategoryAccessFunctions.
Context {M:ExactCategory}.
Definition EC_IsomorphicToExact {P Q:MorphismPair M}
: MorphismPairIsomorphism P Q ⇒ isExact P ⇒ isExact Q
:= pr112 M P Q.
Definition EC_IsomorphicToExact' {P Q:MorphismPair M}
: MorphismPairIsomorphism Q P ⇒ isExact P ⇒ isExact Q
:= pr212 M P Q.
Definition EC_IdentityIsMono (A:M) : isAdmissibleMonomorphism (identity A)
:= pr1 (pr122 M) A.
Definition IdentityMono (A:M) : AdmissibleMonomorphism A A
:= identity A,, EC_IdentityIsMono A.
Definition EC_IdentityIsEpi (A:M) : isAdmissibleEpimorphism (identity A)
:= pr2 (pr122 M) A.
Definition IdentityEpi (A:M) : AdmissibleEpimorphism A A
:= identity A,, EC_IdentityIsEpi A.
Definition EC_ExactToKernelCokernel {P : MorphismPair M} :
isExact P ⇒ isKernelCokernelPair (Mor1 P) (Mor2 P)
:= pr12 (pr22 M) P.
Definition EC_ExactToKernel {P : MorphismPair M} :
isExact P ⇒ isKernel' (Mor1 P) (Mor2 P)
:= λ i, (pr1 (EC_ExactToKernelCokernel i)).
Definition EC_ExactToCokernel {P : MorphismPair M} :
isExact P ⇒ isCokernel' (Mor1 P) (Mor2 P)
:= λ i, (pr2 (EC_ExactToKernelCokernel i)).
Definition EC_ComposeMono {A B C:M} (f : A --> B) (g : B --> C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism g →
isAdmissibleMonomorphism (f · g)
:= pr112 (pr222 M) A B C f g.
Definition EC_ComposeEpi {A B C:M} (f : A --> B) (g : B --> C) :
isAdmissibleEpimorphism f ⇒ isAdmissibleEpimorphism g ⇒
isAdmissibleEpimorphism (f · g)
:= pr212 (pr222 M) A B C f g.
Definition EC_PullbackEpi {A B C:M} (f : A --> B) (g : C --> B) :
isAdmissibleEpimorphism f ⇒
∃ (PB : Pullback f g), isAdmissibleEpimorphism (PullbackPr2 PB)
:= pr122 (pr222 M) A B C f g.
Definition EC_PushoutMono {A B C:M} (f : B --> A) (g : B --> C) :
isAdmissibleMonomorphism f ⇒
∃ (PO : Pushout f g), isAdmissibleMonomorphism (PushoutIn2 PO)
:= pr222 (pr222 M) A B C f g.
End ExactCategoryAccessFunctions.
Section OppositeExactCategory.
Definition oppositeExactCategoryData (M:ExactCategoryData) : ExactCategoryData.
Proof.
∃ (oppositeAdditiveCategory M). exact (λ p, @isExact M (opp_MorphismPair p)).
Defined.
Definition oppositeExactCategory (M:ExactCategory) : ExactCategory.
Proof.
use (make_ExactCategory (oppositeExactCategoryData M)).
split.
{ split;intros P Q f.
- exact (EC_IsomorphicToExact' (opp_MorphismPairIsomorphism f)).
- exact (EC_IsomorphicToExact (opp_MorphismPairIsomorphism f)). }
split.
{ split.
- exact EC_IdentityIsEpi.
- exact EC_IdentityIsMono. }
split.
{ intros P i. exact (opposite_isKernelCokernelPair (EC_ExactToKernelCokernel i)). }
split.
{ split.
{ intros A B C f g i j. exact (@EC_ComposeEpi M C B A g f j i). }
{ intros A B C f g i j. exact (@EC_ComposeMono M C B A g f j i). } }
{ split.
{ exact (@EC_PushoutMono M). }
{ exact (@EC_PullbackEpi M). } }
Defined.
End OppositeExactCategory.
Notation "C '^op'" := (oppositeExactCategory C) (at level 3, format "C ^op") : excat.
Section ExactCategoryFacts.
Lemma ExactToMono {M : ExactCategory} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isMonic i.
Proof.
intros e. exact (KernelIsMonic i p (EC_ExactToKernel e)).
Qed.
Lemma ExactToEpi {M : ExactCategory} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p → isEpi p.
Proof.
intros e. refine (CokernelIsEpi i p (EC_ExactToCokernel e)).
Qed.
Lemma ExactSequenceFromMono {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) :
isCokernel' i p → isAdmissibleMonomorphism i → isExact2 i p.
Proof.
intros co mo. apply (squash_to_hProp mo); clear mo; intros [C' [p' e]].
assert (co' := pr2 (EC_ExactToKernelCokernel e) : isCokernel' i p').
assert (R := iscontrpr1 (CokernelUniqueness co' co)). induction R as [R r].
use (EC_IsomorphicToExact _ e).
∃ (identity_z_iso _). ∃ (identity_z_iso _). ∃ R.
split.
- split.
+ exact (id_left _ @ ! id_right _).
+ exact (id_right _ @ ! id_left _).
- split.
+ exact (id_left _ @ ! r).
+ exact (r @ !id_left _).
Qed.
Lemma ExactSequenceFromEpi {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) :
isKernel' i p → isAdmissibleEpimorphism p → isExact2 i p.
Proof.
exact (ExactSequenceFromMono (M:=M^op) p i).
Defined.
Lemma ExactSequence10 {M : ExactCategory} (A:M) (Z:Zero M) : isExact2 (identity A) (0 : A --> Z).
Proof.
exact (ExactSequenceFromMono _ _ (pr2 (kerCoker10 Z A)) (EC_IdentityIsMono A)).
Qed.
Lemma ExactSequence01 {M : ExactCategory} (A:M) (Z:Zero M) : isExact2 (0 : Z --> A) (identity A).
Proof.
exact (ExactSequenceFromEpi _ _ (pr1 (kerCoker01 Z A)) (EC_IdentityIsEpi A)).
Qed.
Lemma FromZeroIsMono {M : ExactCategory} (Z:Zero M) (A:M) : isAdmissibleMonomorphism (0 : Z --> A).
Proof.
apply hinhpr. ∃ A. ∃ (identity A). use ExactSequence01.
Defined.
Definition MonoFromZero {M : ExactCategory} (Z:Zero M) (A:M) : Z ↣ A
:= (0 : Z --> A),,FromZeroIsMono Z A.
Lemma ToZeroIsEpi {M : ExactCategory} (A:M) (Z:Zero M) : isAdmissibleEpimorphism (0 : A --> Z).
Proof.
apply hinhpr. ∃ A. ∃ (identity A). use ExactSequence10.
Defined.
Definition EpiToZero {M : ExactCategory} (A:M) (Z:Zero M) : A ↠ Z
:= (0 : A --> Z),,ToZeroIsEpi A Z.
Goal ∏ (M:ExactCategory) (A:M) (Z:Zero M), EpiToZero A Z = MonoFromZero (M:=M^op) (Zero_opp M Z) A.
Abort.
Lemma IsomMono1 {M : ExactCategory} {A B B':M} (f : A --> B) (f' : A --> B') :
IsoArrowFrom f f' → isAdmissibleMonomorphism f → isAdmissibleMonomorphism f'.
Proof.
intros [i I] E. apply (squash_to_hProp E); clear E; intros [C [p E]].
apply hinhpr. ∃ C. ∃ (z_iso_inv i · p). use (EC_IsomorphicToExact _ E).
∃ (identity_z_iso A). ∃ i. ∃ (identity_z_iso C). split; cbn.
- split.
+ exact (id_left _ @ ! I).
+ exact (I @ ! id_left _).
- split.
+ refine (assoc _ _ _ @ _ @ id_left _ @ ! id_right _).
apply (maponpaths (λ k, k · p)). apply z_iso_inv_after_z_iso.
+ apply pathsinv0.
refine (assoc _ _ _ @ _ @ id_left _ @ ! id_right _).
apply (maponpaths (λ k, k · p)). apply z_iso_inv_after_z_iso.
Qed.
Lemma IsomEpi1 {M : ExactCategory} {A A' B:M} (f : A --> B) (f' : A' --> B) :
IsoArrowTo f' f → isAdmissibleEpimorphism f → isAdmissibleEpimorphism f'.
Proof.
intros i e.
exact (IsomMono1 (M:=M^op) f f' (opposite_IsoArrowTo i) e).
Defined.
Lemma IsomMono {M : ExactCategory} {A A' B B':M} (f : A --> B) (f' : A' --> B') :
IsoArrow f f' → isAdmissibleMonomorphism f → isAdmissibleMonomorphism f'.
Proof.
intros [g [h e]] i. apply (squash_to_hProp i); clear i; intros [C [p E]].
apply hinhpr. ∃ C. ∃ (z_iso_inv h · p). use (EC_IsomorphicToExact _ E).
simple refine (make_MorphismPairIsomorphism
(make_MorphismPair f p) (make_MorphismPair f' (z_iso_inv h · p))
g h (identity_z_iso C) e _).
refine (assoc _ _ _ @ maponpaths (postcomp_with p) _ @ id_left p @ ! id_right p).
apply z_iso_inv_after_z_iso.
Qed.
Lemma IsomEpi {M : ExactCategory} {A A' B B':M} (f : A --> B) (f' : A' --> B') :
IsoArrow f' f → isAdmissibleEpimorphism f → isAdmissibleEpimorphism f'.
Proof.
intros i.
exact (IsomMono (M:=M^op) f f' (opposite_IsoArrow _ _ i)).
Defined.
Lemma PullbackEpiIsEpi {M : ExactCategory} {A B C:M} (f : A --> B) (g : C --> B)
(pb : Pullback f g) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (PullbackPr2 pb).
Proof.
intros fepi.
assert (qb := EC_PullbackEpi f g fepi).
apply (squash_to_hProp qb); clear qb; intros [qb epi2].
assert (I := pullbackiso2 pb qb).
apply (IsomEpi1 _ _ I). exact epi2.
Qed.
Lemma IsPullbackEpiIsEpi {M : ExactCategory} {P A B C:M} {f : A --> B} {g : C --> B}
{h : P --> A} {k : P --> C} :
isPullback' (M:=M) f g h k → isAdmissibleEpimorphism f → isAdmissibleEpimorphism k.
Proof.
intros pb. exact (PullbackEpiIsEpi f g (make_Pullback _ _ _ _ _ _ (pr2 pb))).
Qed.
Lemma IsIsoIsMono {M : ExactCategory} {A B:M} (f:A-->B) :
is_z_isomorphism f → isAdmissibleMonomorphism f.
Proof.
intros i.
use (IsomMono1 (identity A)).
- use tpair.
+ exact (f,,i).
+ cbn. apply id_left.
- apply EC_IdentityIsMono.
Qed.
Lemma IsoIsMono {M : ExactCategory} {A B:M} (f:z_iso A B) : isAdmissibleMonomorphism (z_iso_mor f).
Proof.
use IsIsoIsMono. apply f.
Qed.
Definition IsoToAdmMono {M : ExactCategory} {A B:M} (f:z_iso A B) : AdmissibleMonomorphism A B
:= z_iso_mor f,,IsoIsMono f.
Lemma IsoIsEpi {M : ExactCategory} {A B:M} (f:z_iso A B) : isAdmissibleEpimorphism (z_iso_mor f).
Proof.
exact (IsoIsMono (M:=M^op) (opp_z_iso f)).
Defined.
Definition IsoToAdmEpi {M : ExactCategory} {A B:M} (f:z_iso A B) : AdmissibleEpimorphism A B
:= z_iso_mor f,,IsoIsEpi f.
Lemma DirectSumToExact {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isExact2 (to_In1 S) (to_Pr2 S).
Proof.
use ExactSequenceFromEpi.
{ exact (PairToKernel (kerCokerDirectSum S)). }
apply (squash_to_hProp (to_hasZero M)); intros Z.
set (pb := DirectSumToPullback S Z).
change (isAdmissibleEpimorphism (PullbackPr2 pb)).
assert (Q := EC_PullbackEpi (0 : A --> Z) (0 : B --> Z) (ToZeroIsEpi A Z)).
apply (squash_to_hProp Q); clear Q; intros [pb' R'].
exact (IsomEpi1 (PullbackPr2 pb') (PullbackPr2 pb) (pullbackiso2 pb pb') R').
Qed.
Lemma DirectSumToExact' {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isExact2 (to_In2 S) (to_Pr1 S).
Proof.
exact (DirectSumToExact (reverseBinDirectSum S)).
Qed.
Lemma In1IsAdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleMonomorphism (ι₁ : A --> S).
Proof.
exact (hinhpr (B,,to_Pr2 S,,DirectSumToExact S)).
Qed.
Lemma In2IsAdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleMonomorphism (ι₂ : B --> S).
Proof.
exact (hinhpr (A,,to_Pr1 S,,DirectSumToExact' S)).
Qed.
Lemma Pr1IsAdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleEpimorphism (π₁ : S --> A).
Proof.
exact (hinhpr (B,,to_In2 S,,DirectSumToExact' S)).
Qed.
Lemma Pr2IsAdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : isAdmissibleEpimorphism (π₂ : S --> B).
Proof.
exact (hinhpr (A,,to_In1 S,,DirectSumToExact S)).
Qed.
Definition In1AdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleMonomorphism A S := ι₁ ,, In1IsAdmMono S.
Definition In2AdmMono {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleMonomorphism B S := ι₂ ,, In2IsAdmMono S.
Definition Pr1AdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleEpimorphism S A := π₁ ,, Pr1IsAdmEpi S.
Definition Pr2AdmEpi {M : ExactCategory} {A B:M} (S:BinDirectSum A B) : AdmissibleEpimorphism S B := π₂ ,, Pr2IsAdmEpi S.
Definition TrivialExactSequence {M : ExactCategory} (A:M) (Z:Zero M) : ShortExactSequence M.
Proof.
assert (Q := DirectSumToExact (TrivialDirectSum Z A)).
exact (make_MorphismPair ι₁ π₂,, Q).
Defined.
Definition TrivialExactSequence' {M : ExactCategory} (Z:Zero M) (A:M) : ShortExactSequence M.
Proof.
assert (Q := DirectSumToExact (TrivialDirectSum' Z A)).
exact (make_MorphismPair ι₁ π₂,, Q).
Defined.
Lemma ExactPushout {M : ExactCategory} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isExact2 i p) (r : A --> A') :
∃ (po : Pushout i r),
isExact2 (PushoutIn2 po) (pr1 (PairPushoutMap (EC_ExactToKernelCokernel pr) r po)).
Proof.
assert (I := ExactToAdmMono pr).
assert (R := EC_PushoutMono i r I).
apply (squash_to_hProp R); clear R; intros [po J]; apply hinhpr.
∃ po. use ExactSequenceFromMono.
{ exact (PairPushoutCokernel i p (EC_ExactToKernelCokernel pr) r po). }
exact J.
Qed.
Lemma ExactPushout' {M : ExactCategory} {A B C A':M} (i : A --> B) (p : B --> C)
(pr : isExact2 i p) (r : A --> A') :
∃ (B':M) (i':A'-->B') (s:B-->B') (p':B'-->C),
s·p' = p ∧ isPushout' (M:=M) i r s i' ∧ isExact2 i' p'.
Proof.
assert (I := ExactToAdmMono pr). assert (R := EC_PushoutMono i r I).
use (hinhfun _ R); clear R; intros [po J].
set (pomap := PairPushoutMap (EC_ExactToKernelCokernel pr) r po).
set (p' := pr1 pomap).
∃ po. ∃ (PushoutIn2 po). ∃ (PushoutIn1 po). ∃ p'.
split.
{ exact (pr12 pomap). }
split.
{ apply Pushout_to_isPushout'. }
{ use ExactSequenceFromMono.
{ exact (PairPushoutCokernel i p (EC_ExactToKernelCokernel pr) r po). }
exact J. }
Qed.
Lemma ExactPullback {M : ExactCategory} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isExact2 p i)
(r : A <-- A') :
∃ (pb : Pullback i r),
isExact2 (pr1 (PairPullbackMap (EC_ExactToKernelCokernel pr) r pb)) (PullbackPr2 pb).
Proof.
assert (I := hinhpr (C ,, p ,, pr) : isAdmissibleEpimorphism i).
assert (R := EC_PullbackEpi i r I).
apply (squash_to_hProp R); clear R; intros [pb J]; apply hinhpr.
∃ pb. use ExactSequenceFromEpi.
{ exact (PairPullbackKernel i p (EC_ExactToKernelCokernel pr) r pb). }
exact J.
Qed.
Lemma ExactPullback' {M : ExactCategory} {A B C A':M} (i : A <-- B) (p : B <-- C)
(pr : isExact2 p i) (r : A <-- A') :
∃ (B':M) (i':A'<--B') (s:B<--B') (p':B'<--C),
s∘p' = p ∧ isPullback' (M:=M) i r s i' ∧ isExact2 p' i'.
Proof.
assert (I := ExactToAdmEpi pr). assert (R := EC_PullbackEpi i r I).
use (hinhfun _ R); clear R; intros [pb J].
set (pbmap := PairPullbackMap (EC_ExactToKernelCokernel pr) r pb).
set (p' := pr1 pbmap).
∃ pb. ∃ (PullbackPr2 pb). ∃ (PullbackPr1 pb). ∃ p'.
split.
{ exact (pr12 pbmap). }
split.
{ apply Pullback_to_isPullback'. }
{ use ExactSequenceFromEpi.
{ exact (PairPullbackKernel i p (EC_ExactToKernelCokernel pr) r pb). }
exact J. }
Qed.
Lemma MonicAdmEpiIsIso {M : ExactCategory} {A B:M} (p : A ↠ B) : isMonic p → is_z_isomorphism p.
Proof.
induction p as [p E]. cbn. intros I. apply (squash_to_prop E).
{ apply isaprop_is_z_isomorphism. apply to_has_homsets. }
clear E; intros [K [i E]].
assert (Q := EC_ExactToKernelCokernel E); clear E.
induction Q as [ke co];
change (hProptoType (isKernel' i p)) in ke;
change (hProptoType (isCokernel' i p)) in co.
assert (Q : i = 0).
{ use (I K i 0). exact (pr1 ke @ ! zeroLeft _). }
clear I ke. induction (!Q); clear Q. exact (CokernelOfZeroMapIsIso p co).
Qed.
Lemma EpiAdmMonoIsIso {M : ExactCategory} {A B:M} (i : A ↣ B) : isEpi i → is_z_isomorphism i.
Proof.
intros e.
exact (opp_is_z_isomorphism _ (MonicAdmEpiIsIso (M:=M^op) i e)).
Defined.
Lemma MonoPlusIdentity {M : ExactCategory} {A B:M}
(f:A-->B) (C:M) (AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism (directSumMap AC BC f (identity C)).
Proof.
intro i. apply (squash_to_hProp i). intros [D [p j]].
apply hinhpr. ∃ D. ∃ (π₁ · p). apply ExactSequenceFromEpi.
2:{ apply EC_ComposeEpi.
- apply Pr1IsAdmEpi.
- exact (hinhpr(A,,f,,j)). }
apply (squash_to_hProp (to_hasZero M)); intros Z.
apply (squash_to_hProp (to_hasBinDirectSums D Z)); intros DZ.
assert (m := pr1 (SumOfKernelCokernelPairs AC BC DZ
(EC_ExactToKernelCokernel j : isKernelCokernelPair f p)
(kerCoker10 Z C : isKernelCokernelPair (identity C) 0))).
assert (R : directSumMap BC DZ p 0 · to_Pr1 DZ = to_Pr1 BC · p).
{ apply directSumMapEqPr1. }
induction R. apply IsoWithKernel.
{ exact m. }
∃ (ι₁). split.
{ refine (! runax (_ --> _) _ @ ! _ @ to_BinOpId'' _). apply maponpaths. apply ThroughZeroIsZero. }
{ refine (to_IdIn1 DZ). }
Qed.
Lemma EpiPlusIdentity {M : ExactCategory} {A B:M} (f:A-->B) (C:M) (AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (directSumMap AC BC f (identity C)).
Proof.
intro i. rewrite <- opposite_directSumMap'.
exact (MonoPlusIdentity (M:=M^op) f C (oppositeBinDirectSum BC) (oppositeBinDirectSum AC) i).
Defined.
Lemma IdentityPlusMono {M : ExactCategory} {B C:M} (A:M) (f:B-->C)
(AB : BinDirectSum A B) (AC : BinDirectSum A C) :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism (directSumMap AB AC (identity A) f).
Proof.
intros i. use (IsomMono (directSumMap (reverseBinDirectSum AB) (reverseBinDirectSum AC) f (identity A)) (directSumMap AB AC (identity A) f)).
- ∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
- apply MonoPlusIdentity. exact i.
Defined.
Lemma IdentityPlusEpi {M : ExactCategory} {B C:M} (A:M) (f:B-->C)
(AB : BinDirectSum A B) (AC : BinDirectSum A C) :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism (directSumMap AB AC (identity A) f).
Proof.
intros i. use (IsomEpi (directSumMap (reverseBinDirectSum AB) (reverseBinDirectSum AC) f (identity A)) (directSumMap AB AC (identity A) f)).
- ∃ (SwitchIso _ _ _ _). ∃ (SwitchIso _ _ _ _). apply SwitchMapMapEqn.
- apply EpiPlusIdentity. exact i.
Defined.
Lemma SumOfExactSequences {M:ExactCategory} {A B C A' B' C':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B') (CC' : BinDirectSum C C')
{f : A --> B} {g : B --> C} {f' : A' --> B'} {g' : B' --> C'} :
isExact2 f g → isExact2 f' g' → isExact2 (directSumMap AA' BB' f f') (directSumMap BB' CC' g g').
Proof.
intros i i'. apply ExactSequenceFromMono.
{ use SumOfCokernels.
- exact (EC_ExactToCokernel i).
- exact (EC_ExactToCokernel i'). }
apply (squash_to_hProp (to_hasBinDirectSums A B')); intros AB'.
set (j := directSumMap AB' BB' f (identity B')).
set (k := directSumMap AA' AB' (identity A) f').
assert (kj : k · j = directSumMap AA' BB' f f').
{ apply ToBinDirectSumUnique.
- refine (! assoc _ _ _ @ _). intermediate_path (k · (π₁ · f)).
+ apply maponpaths. apply directSumMapEqPr1.
+ refine (assoc _ _ _ @ _). apply (maponpaths (postcomp_with _)).
exact (directSumMapEqPr1 @ id_right _).
- refine (! assoc _ _ _ @ _). intermediate_path (k · (π₂ · (identity B'))).
+ apply maponpaths. apply directSumMapEqPr2.
+ refine (assoc _ _ _ @ id_right _ @ _). apply directSumMapEqPr2. }
induction kj. use (EC_ComposeMono k j).
- apply IdentityPlusMono. exact (ExactToAdmMono i').
- apply MonoPlusIdentity. exact (ExactToAdmMono i).
Qed.
Lemma AdmMonoEnlargement {M:ExactCategory} {A B C:M}
(BC : BinDirectSum B C) (i:A-->B) (f:A-->C) :
isAdmissibleMonomorphism i → isAdmissibleMonomorphism (ToBinDirectSum BC i f).
Proof.
intros I.
apply (squash_to_hProp (to_hasBinDirectSums A C)); intros AC.
assert (e : ToBinDirectSum BC i f = ι₁ · (1 + π₁·f·ι₂) · (directSumMap AC _ i 1)).
{ apply ToBinDirectSumsEq.
- rewrite BinDirectSumPr1Commutes. rewrite assoc'. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes.
rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute.
rewrite id_right. rewrite (to_IdIn1 AC). rewrite id_left.
refine (! runax (A-->B) _ @ _). apply maponpaths. rewrite assoc.
rewrite (assoc' _ _ π₁). rewrite (to_Unel2 AC). unfold to_unel.
rewrite zeroRight, zeroLeft. reflexivity.
- rewrite BinDirectSumPr2Commutes. rewrite assoc'. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite BinDirectSumPr2Commutes.
rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute.
rewrite 2 id_right. rewrite (to_Unel1 AC). unfold to_unel.
rewrite lunax. rewrite id_right. rewrite 2 assoc.
rewrite (to_IdIn1 AC). rewrite id_left.
rewrite assoc'. rewrite (to_IdIn2 AC). rewrite id_right. reflexivity. }
induction (!e); clear e.
apply EC_ComposeMono.
- apply EC_ComposeMono.
+ apply In1IsAdmMono.
+ apply IsIsoIsMono. apply elem21_isiso.
- now apply MonoPlusIdentity.
Qed.
Lemma SumOfAdmissibleEpis {M:ExactCategory} {A B A' B':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B')
(f : A --> B) (f' : A' --> B') :
isAdmissibleEpimorphism f → isAdmissibleEpimorphism f' → isAdmissibleEpimorphism (directSumMap AA' BB' f f').
Proof.
intros e e'.
apply (squash_to_hProp e); clear e; intros [C [g e]].
apply (squash_to_hProp e'); clear e'; intros [C' [g' e']].
apply (squash_to_hProp (to_hasBinDirectSums C C')); intros CC'.
exact (ExactToAdmEpi (SumOfExactSequences CC' _ _ e e')).
Qed.
Lemma SumOfAdmissibleMonos {M:ExactCategory} {A B A' B':M}
(AA' : BinDirectSum A A') (BB' : BinDirectSum B B')
(f : A --> B) (f' : A' --> B') :
isAdmissibleMonomorphism f → isAdmissibleMonomorphism f' → isAdmissibleMonomorphism (directSumMap AA' BB' f f').
Proof.
intros e e'.
apply (squash_to_hProp e); clear e; intros [C [g e]].
apply (squash_to_hProp e'); clear e'; intros [C' [g' e']].
apply (squash_to_hProp (to_hasBinDirectSums C C')); intros CC'.
exact (ExactToAdmMono (SumOfExactSequences _ _ CC' e e')).
Qed.
Lemma MapPlusIdentityToCommSq {M:ExactCategory} {A B:M}
(f:A-->B) (C:M)
(AC : BinDirectSum A C) (BC : BinDirectSum B C) :
f · ι₁ = ι₁ · (directSumMap AC BC f (identity C)).
Proof.
apply ToBinDirectSumsEq.
- rewrite assoc'. rewrite (to_IdIn1 BC). rewrite id_right. unfold directSumMap.
unfold BinDirectSumIndAr. rewrite assoc'. rewrite BinDirectSumPr1Commutes.
rewrite assoc. rewrite (to_IdIn1 AC). rewrite id_left. reflexivity.
- rewrite assoc'. rewrite (to_Unel1 BC). unfold to_unel. rewrite zeroRight.
unfold directSumMap, BinDirectSumIndAr. rewrite assoc'.
rewrite BinDirectSumPr2Commutes. rewrite id_right. apply pathsinv0.
use (to_Unel1 AC).
Qed.
Lemma KernelPlusIdentity {M:ExactCategory} {A B C:M}
(f:A-->B) (g:B-->C) (D:M)
(BD : BinDirectSum B D) (CD : BinDirectSum C D) :
isKernel' (f · ι₁) (directSumMap BD CD g (identity D)) → isKernel' f g.
Proof.
intros K. apply makeMonicKernel.
- exact (isMonic_postcomp _ _ _ (KernelIsMonic _ _ K)).
- use (to_In1_isMonic _ CD). rewrite zeroLeft. rewrite assoc'.
assert (Q := pr1 K); simpl in Q. rewrite assoc' in Q.
rewrite directSumMapEqIn1 in Q. exact Q.
- intros T h eqn.
assert (E : h · ι₁ · directSumMap BD CD g (identity D) = 0).
{ rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc.
refine (maponpaths (λ r, r·ι₁) eqn @ _). apply zeroLeft. }
assert (Q := iscontrpr1 (pr2 K T (h·ι₁) E)); simpl in Q.
induction Q as [p e].
∃ p.
rewrite assoc in e.
apply (to_In1_isMonic _ _ _ _ _ e).
Qed.
Lemma CokernelPlusIdentity {M:ExactCategory} {A B C:M} (f:A-->B) (g:B-->C) (D:M)
(BD : BinDirectSum B D) (CD : BinDirectSum C D):
isCokernel' f g →
isCokernel' (f · ι₁) (directSumMap BD CD g (identity D)).
Proof.
intros ic.
split.
{ rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc. rewrite (pr1 ic). apply zeroLeft. }
intros T h u.
apply iscontraprop1.
{ apply invproofirrelevance. intros [r r'] [s s']. apply subtypePath_prop; cbn.
assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq.
- assert (L := maponpaths (λ w, ι₁ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L.
rewrite directSumMapEqIn1 in L.
rewrite 2 assoc' in L. exact (CokernelIsEpi _ g ic _ _ _ L).
- assert (L := maponpaths (λ w, ι₂ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L.
rewrite directSumMapEqIn2 in L.
rewrite 2 assoc' in L. rewrite 2 id_left in L. exact L. }
assert (Q := iscontrpr1 (pr2 ic _ _ (assoc _ _ _ @ u))).
induction Q as [q Q].
∃ (π₁ · q + π₂ · ι₂ · h).
rewrite rightDistribute.
rewrite assoc. rewrite assoc. rewrite assoc.
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes,BinDirectSumPr2Commutes.
rewrite id_right.
rewrite assoc'. rewrite Q. rewrite assoc.
rewrite <- leftDistribute.
refine (_ @ id_left _).
apply (maponpaths (λ w, w·h)).
use to_BinOpId''.
Qed.
Lemma MapPlusIdentityToPullback {M:ExactCategory} {A B:M} (f:A-->B) (C:M)
(AC : BinDirectSum A C) (BC : BinDirectSum B C) :
isPullback _ _ _ _ (MapPlusIdentityToCommSq f C AC BC).
Proof.
intros T g h e. apply iscontraprop1.
- apply invproofirrelevance. intros [p [P P']] [q [Q Q']].
apply subtypePath.
{ intros r. apply isapropdirprod; apply to_has_homsets. }
cbn. clear P Q.
refine (! id_right _ @ _ @ id_right _).
rewrite <- (to_IdIn1 AC). rewrite 2 assoc. induction (!P'), (!Q'). reflexivity.
- ∃ (h · π₁).
split.
+ refine (_ @ id_right _). rewrite <- (to_IdIn1 BC).
rewrite (assoc g). rewrite e. rewrite (assoc' h _ π₁).
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes.
rewrite assoc. reflexivity.
+ refine (_ @ id_right _). rewrite <- (to_BinOpId' AC).
rewrite rightDistribute. rewrite assoc. refine (! runax (Hom_add _ _ _) _ @ _).
apply maponpaths. rewrite assoc. apply pathsinv0.
assert (K : h · π₂ = 0).
{ refine ( _ @ maponpaths (λ w, w · π₂) (!e) @ _ ).
- rewrite assoc'.
unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr2Commutes.
rewrite id_right. reflexivity.
- rewrite assoc'. rewrite (to_Unel1 BC). unfold to_unel.
apply zeroRight. }
rewrite K. apply zeroLeft.
Qed.
The "obscure" axiom c of Quillen.