Library UniMath.CategoryTheory.categories.abgrs
Category of abelian groups
Contents
- Precategory of abelian groups
- Category of abelian groups
- Zero object and Zero arrow
- Zero object
- Zero arrow
- Category of abelian groups is preadditive
- Category of abelian groups is additive
- Kernels and Cokernels
- Kernels
- Cokernels
- Monics are inclusions and Epis are surjections
- Epis are surjections
- Monics are inclusions
- Monics are kernels of their cokernels and epis are cokernels of their kernels
- Monics are Kernels
- Epis are Cokernels
- The category of abelian groups is an abelian category
- Corollaries to additive categories
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.NumberSystems.Integers.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.CategoriesWithBinOps.
Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops.
Require Import UniMath.CategoryTheory.PreAdditive.
Require Import UniMath.CategoryTheory.Additive.
Require Import UniMath.CategoryTheory.Abelian.
Require Import UniMath.CategoryTheory.limits.zero.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Require Import UniMath.CategoryTheory.limits.kernels.
Require Import UniMath.CategoryTheory.limits.cokernels.
Require Import UniMath.CategoryTheory.limits.BinDirectSums.
Local Open Scope cat.
Definition abgr_fun_space (A B : abgr) : hSet := make_hSet (monoidfun A B) (isasetmonoidfun A B).
Definition abgr_precategory_ob_mor : precategory_ob_mor :=
tpair (λ ob : UU, ob -> ob -> UU) abgr (λ A B : abgr, abgr_fun_space A B).
Definition abgr_precategory_data : precategory_data :=
make_precategory_data
abgr_precategory_ob_mor (λ (A : abgr), ((idmonoidiso A) : monoidfun A A))
(fun (A B C : abgr) (f : monoidfun A B) (g : monoidfun B C) => monoidfuncomp f g).
Lemma is_precategory_abgr_precategory_data : is_precategory abgr_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros a b f. use monoidfunidleft.
- intros a b f. use monoidfunidright.
- intros a b c d f g h. use monoidfunassoc.
- intros a b f. use monoidfunidleft.
- intros a b f. use monoidfunidright.
- intros a b c d f g h. use monoidfunassoc.
Definition abgr_precategory : precategory :=
make_precategory abgr_precategory_data is_precategory_abgr_precategory_data.
Lemma has_homsets_abgr : has_homsets abgr_precategory.
Show proof.
Definition abgr_category : category := make_category abgr_precategory has_homsets_abgr.
End def_abgr_precategory.
Lemma abgr_z_iso_is_equiv (A B : ob abgr_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
Show proof.
use isweq_iso.
- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
- exact (pr1monoidfun _ _ (inv_from_z_iso f)).
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
intros x0. use isapropismonoidfun.
- intros x.
use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
intros x0. use isapropismonoidfun.
Lemma abgr_z_iso_equiv (X Y : ob abgr_category) : z_iso X Y -> monoidiso (X : abgr) (Y : abgr).
Show proof.
intro f.
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (abgr_z_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
use make_monoidiso.
- exact (make_weq (pr1 (pr1 f)) (abgr_z_iso_is_equiv X Y f)).
- exact (pr2 (pr1 f)).
Lemma abgr_equiv_is_z_iso (X Y : ob abgr_category) (f : monoidiso (X : abgr) (Y : abgr)) :
@is_z_isomorphism abgr_category X Y (monoidfunconstr (pr2 f)).
Show proof.
exists (monoidfunconstr (pr2 (invmonoidiso f))).
split.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
split.
- use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
- use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
Definition abgr_equiv_z_iso (X Y : ob abgr_category) (f : monoidiso (X : abgr) (Y : abgr)) :
z_iso X Y := @make_z_iso' abgr_category X Y (monoidfunconstr (pr2 f)) (abgr_equiv_is_z_iso X Y f).
Lemma abgr_z_iso_equiv_is_equiv (X Y : abgr_category) : isweq (abgr_z_iso_equiv X Y).
Show proof.
use isweq_iso.
- exact (abgr_equiv_z_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- exact (abgr_equiv_z_iso X Y).
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
Definition abgr_z_iso_equiv_weq (X Y : ob abgr_category) :
weq (z_iso X Y) (monoidiso (X : abgr) (Y : abgr)).
Show proof.
Lemma abgr_equiv_z_iso_is_equiv (X Y : ob abgr_category) : isweq (abgr_equiv_z_iso X Y).
Show proof.
use isweq_iso.
- exact (abgr_z_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
- exact (abgr_z_iso_equiv X Y).
- intros y. use monoidiso_paths. use subtypePath.
+ intros x0. use isapropisweq.
+ use idpath.
- intros x. use z_iso_eq. use monoidfun_paths. use idpath.
Definition abgr_equiv_weq_z_iso (X Y : ob abgr_category) :
(monoidiso (X : abgr) (Y : abgr)) ≃ (z_iso X Y).
Show proof.
Definition abgr_category_isweq (a b : ob abgr_category) : isweq (λ p : a = b, idtoiso p).
Show proof.
use (@isweqhomot
(a = b) (z_iso a b)
(pr1weq (weqcomp (abgr_univalence a b) (abgr_equiv_weq_z_iso a b)))
_ _ (weqproperty (weqcomp (abgr_univalence a b) (abgr_equiv_weq_z_iso a b)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use total2_paths_f.
+ use idpath.
+ use proofirrelevance. use isapropismonoidfun.
- use proofirrelevance. use isaprop_is_z_isomorphism.
(a = b) (z_iso a b)
(pr1weq (weqcomp (abgr_univalence a b) (abgr_equiv_weq_z_iso a b)))
_ _ (weqproperty (weqcomp (abgr_univalence a b) (abgr_equiv_weq_z_iso a b)))).
intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use total2_paths_f.
- use total2_paths_f.
+ use idpath.
+ use proofirrelevance. use isapropismonoidfun.
- use proofirrelevance. use isaprop_is_z_isomorphism.
Definition abgr_category_is_univalent : is_univalent abgr_category.
Show proof.
Definition abgr_univalent_category : univalent_category :=
make_univalent_category abgr_category abgr_category_is_univalent.
End def_abgr_category.
Zero object and Zero arrow
- Zero object is the abelian group which consists of one element, the unit element.
- The unique morphism to zero object maps every element to the unit element.
- The unique morphism from the zero object maps unit to unit.
- The unique morphisms which factors through zero object maps every element to the unit element.
- Computations on zero object
Lemma isconnectedfromunitabgr (a : abgr_category) (t : abgr_category ⟦unitabgr, a⟧):
(t : monoidfun unitabgr (a : abgr)) = abgrfunfromunit (a : abgr).
Show proof.
use monoidfun_paths. use funextfun. intros x.
use (pathscomp0 _ (monoidfununel t)). use maponpaths. use isProofIrrelevantUnit.
use (pathscomp0 _ (monoidfununel t)). use maponpaths. use isProofIrrelevantUnit.
Lemma isconnectedtounitabgr (a : abgr_category) (t : abgr_category ⟦a, unitabgr⟧):
(t : monoidfun (a : abgr) unitabgr) = abgrfuntounit a.
Show proof.
Definition abgr_isZero : @isZero abgr_category unitabgr.
Show proof.
use make_isZero.
- intros a. use make_iscontr.
+ exact (abgrfunfromunit a).
+ intros t. exact (isconnectedfromunitabgr a t).
- intros a. use make_iscontr.
+ exact (abgrfuntounit a).
+ intros t. exact (isconnectedtounitabgr a t).
- intros a. use make_iscontr.
+ exact (abgrfunfromunit a).
+ intros t. exact (isconnectedfromunitabgr a t).
- intros a. use make_iscontr.
+ exact (abgrfuntounit a).
+ intros t. exact (isconnectedtounitabgr a t).
Definition abgr_Zero : Zero abgr_category := @make_Zero abgr_category unitabgr abgr_isZero.
Lemma abgr_Zero_comp : ZeroObject (abgr_Zero) = unitabgr.
Show proof.
Lemma abgr_Zero_from_comp (A : abgr) :
@ZeroArrowFrom abgr_category abgr_Zero A = abgrfunfromunit A.
Show proof.
Lemma abgr_Zero_to_comp (A : abgr) :
@ZeroArrowTo abgr_category abgr_Zero A = abgrfuntounit A.
Show proof.
Lemma abgr_Zero_arrow_comp (A B : abgr) :
@ZeroArrow abgr_category abgr_Zero A B = unelabgrfun A B.
Show proof.
End def_abgr_zero.
Preadditive structure on the category of abelian groups
- Binary operation on homsets.
- Abelian group structure on homsets
- PreAdditive structure on the category of abelian groups
Binary operations on homsets
Let f, g : X --> Y be morphisms in the category of abelian groups. Then f + g is defined to be the morphism (f + g) x = (f x) + (g x). This gives precategoryWithBinOps structure on the category.Definition abgr_WithBinOpsData : precategoryWithBinOpsData abgr_category.
Show proof.
Definition abgr_WithBinOps : precategoryWithBinOps :=
make_precategoryWithBinOps abgr_category abgr_WithBinOpsData.
categoryWithAbgrops structure on the category of abelian groups
Definition abgr_WithAbGrops : categoryWithAbgrops.
Show proof.
use make_categoryWithAbgrops.
- exact abgr_WithBinOps.
- use make_categoryWithAbgropsData.
intros X Y. exact (@abgrshomabgr_isabgrop X Y).
- exact abgr_WithBinOps.
- use make_categoryWithAbgropsData.
intros X Y. exact (@abgrshomabgr_isabgrop X Y).
PreAdditive structure on the category of abelian groups
Definition abgr_isPreAdditive : isPreAdditive abgr_WithAbGrops.
Show proof.
use make_isPreAdditive.
- intros X Y Z f.
use make_ismonoidfun.
+ use make_isbinopfun. intros g h. use monoidfun_paths. use funextfun. intros x. use idpath.
+ use monoidfun_paths. use funextfun. intros x. use idpath.
- intros X Y Z f.
use make_ismonoidfun.
+ use make_isbinopfun. intros g h. use monoidfun_paths. use funextfun. intros x.
use (pathscomp0 ((pr1 (pr2 f)) _ _)). use idpath.
+ use monoidfun_paths. use funextfun. intros x. exact (monoidfununel f).
- intros X Y Z f.
use make_ismonoidfun.
+ use make_isbinopfun. intros g h. use monoidfun_paths. use funextfun. intros x. use idpath.
+ use monoidfun_paths. use funextfun. intros x. use idpath.
- intros X Y Z f.
use make_ismonoidfun.
+ use make_isbinopfun. intros g h. use monoidfun_paths. use funextfun. intros x.
use (pathscomp0 ((pr1 (pr2 f)) _ _)). use idpath.
+ use monoidfun_paths. use funextfun. intros x. exact (monoidfununel f).
Definition abgr_PreAdditive : PreAdditive :=
make_PreAdditive abgr_WithAbGrops abgr_isPreAdditive.
End abgr_preadditive.
Direct sums
Direct sum of X and Y is given by the direct product abelian group X × Y. The inclusions and projections are given by- In1 : x ↦ (x, 0)
- In2 : y ↦ (0, y)
- Pr1 : (x, y) ↦ x
- Pr2 : (x, y) ↦ y
Lemma abgr_DirectSumPr1_ismonoidfun (A B : abgr) :
ismonoidfun (λ X : abgrdirprod A B, dirprod_pr1 X).
Show proof.
Definition abgr_DirectSumPr1 (A B : abgr) : abgr_category⟦abgrdirprod A B, A⟧ :=
monoidfunconstr (abgr_DirectSumPr1_ismonoidfun A B).
Lemma abgr_DirectSumPr2_ismonoidfun (A B : abgr) :
ismonoidfun (λ X : abgrdirprod A B, dirprod_pr2 X).
Show proof.
Definition abgr_DirectSumPr2 (A B : abgr) : abgr_category⟦abgrdirprod A B, B⟧ :=
monoidfunconstr (abgr_DirectSumPr2_ismonoidfun A B).
Lemma abgr_DirectSumIn1_ismonoidfun (A B : abgr) :
@ismonoidfun A (abgrdirprod A B) (λ a : A, make_dirprod a (unel B)).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use dirprod_paths.
+ use idpath.
+ use pathsinv0. use (runax B).
- use dirprod_paths.
+ use idpath.
+ use idpath.
- use make_isbinopfun. intros x x'. use dirprod_paths.
+ use idpath.
+ use pathsinv0. use (runax B).
- use dirprod_paths.
+ use idpath.
+ use idpath.
Definition abgr_DirectSumIn1 (A B : abgr) : abgr_category⟦A, abgrdirprod A B⟧ :=
monoidfunconstr (abgr_DirectSumIn1_ismonoidfun A B).
Lemma abgr_DirectSumIn2_ismonoidfun (A B : abgr) :
@ismonoidfun B (abgrdirprod A B) (λ b : B, make_dirprod (unel A) b).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use dirprod_paths.
+ use pathsinv0. use (runax A).
+ use idpath.
- use dirprod_paths.
+ use idpath.
+ use idpath.
- use make_isbinopfun. intros x x'. use dirprod_paths.
+ use pathsinv0. use (runax A).
+ use idpath.
- use dirprod_paths.
+ use idpath.
+ use idpath.
Definition abgr_DirectSumIn2 (A B : abgr) : abgr_category⟦B, abgrdirprod A B⟧ :=
monoidfunconstr (abgr_DirectSumIn2_ismonoidfun A B).
Lemma abgr_DirectSumIdIn1 (A B : abgr) :
abgr_DirectSumIn1 A B · abgr_DirectSumPr1 A B = (idmonoidiso A : monoidfun A A).
Show proof.
Lemma abgr_DirectSumIdIn2 (A B : abgr) :
abgr_DirectSumIn2 A B · abgr_DirectSumPr2 A B = (idmonoidiso B : monoidfun B B).
Show proof.
Lemma abgr_DirectSumUnel1 (A B : abgr) :
abgr_DirectSumIn1 A B · abgr_DirectSumPr2 A B = @to_unel abgr_PreAdditive A B.
Show proof.
Lemma abgr_DirectSumUnel2 (A B : abgr) :
abgr_DirectSumIn2 A B · abgr_DirectSumPr1 A B = @to_unel abgr_PreAdditive B A.
Show proof.
Lemma abgr_DirectSumId (A B : abgr) :
@abmonoidshombinop
(abgrdirprod A B) (abgrdirprod A B)
(abgr_DirectSumPr1 A B · abgr_DirectSumIn1 A B)
(abgr_DirectSumPr2 A B · abgr_DirectSumIn2 A B) =
((idmonoidiso (abgrdirprod A B)) : monoidfun (abgrdirprod A B) (abgrdirprod A B)) .
Show proof.
Lemma abgr_isBinDirectSum (X Y : abgr) :
@isBinDirectSum
abgr_PreAdditive X Y (abgrdirprod X Y) (abgr_DirectSumIn1 X Y) (abgr_DirectSumIn2 X Y)
(abgr_DirectSumPr1 X Y) (abgr_DirectSumPr2 X Y).
Show proof.
use make_isBinDirectSum.
- exact (abgr_DirectSumIdIn1 X Y).
- exact (abgr_DirectSumIdIn2 X Y).
- exact (abgr_DirectSumUnel1 X Y).
- exact (abgr_DirectSumUnel2 X Y).
- exact (abgr_DirectSumId X Y).
- exact (abgr_DirectSumIdIn1 X Y).
- exact (abgr_DirectSumIdIn2 X Y).
- exact (abgr_DirectSumUnel1 X Y).
- exact (abgr_DirectSumUnel2 X Y).
- exact (abgr_DirectSumId X Y).
Definition abgr_AdditiveStructure : AdditiveStructure abgr_PreAdditive.
Show proof.
use make_AdditiveStructure.
- exact abgr_Zero.
- use make_BinDirectSums. intros X Y. use make_BinDirectSum.
+ exact (abgrdirprod X Y).
+ exact (abgr_DirectSumIn1 X Y).
+ exact (abgr_DirectSumIn2 X Y).
+ exact (abgr_DirectSumPr1 X Y).
+ exact (abgr_DirectSumPr2 X Y).
+ exact (abgr_isBinDirectSum X Y).
- exact abgr_Zero.
- use make_BinDirectSums. intros X Y. use make_BinDirectSum.
+ exact (abgrdirprod X Y).
+ exact (abgr_DirectSumIn1 X Y).
+ exact (abgr_DirectSumIn2 X Y).
+ exact (abgr_DirectSumPr1 X Y).
+ exact (abgr_DirectSumPr2 X Y).
+ exact (abgr_isBinDirectSum X Y).
Definition abgr_Additive : CategoryWithAdditiveStructure := make_Additive abgr_PreAdditive abgr_AdditiveStructure.
End abgr_additive.
Kernels and Cokernels
- Kernels in the category of abelian groups
- Cokernels in the category of abelian groups
Section abgr_kernels_and_cokernels.
Definition abgr_Kernel_monoidfun {A B : abgr} (f : monoidfun A B) :
abgr_category⟦carrierofasubabgr (abgr_Kernel_subabgr f), A⟧ :=
monoidincltomonoidfun
(abgr_Kernel_subabgr f) A
(@make_monoidmono (abgr_Kernel_subabgr f) A
(make_incl (pr1carrier (abgr_kernel_hsubtype f))
(isinclpr1carrier (abgr_kernel_hsubtype f)))
(abgr_Kernel_monoidfun_ismonoidfun f)).
Definition abgr_Kernel_monoidfun {A B : abgr} (f : monoidfun A B) :
abgr_category⟦carrierofasubabgr (abgr_Kernel_subabgr f), A⟧ :=
monoidincltomonoidfun
(abgr_Kernel_subabgr f) A
(@make_monoidmono (abgr_Kernel_subabgr f) A
(make_incl (pr1carrier (abgr_kernel_hsubtype f))
(isinclpr1carrier (abgr_kernel_hsubtype f)))
(abgr_Kernel_monoidfun_ismonoidfun f)).
Definition abgr_Kernel_eq {A B : abgr} (f : monoidfun A B) :
abgr_Kernel_monoidfun f · f = ZeroArrow abgr_Zero (carrierofasubabgr (abgr_Kernel_subabgr f)) B.
Show proof.
Lemma abgr_KernelArrowIn_map_property {A B C : abgr_category} (h : C --> A) (f : A --> B)
(H : h · f = ZeroArrow abgr_Zero C B) (c : (C : abgr)) :
(pr1 f (pr1 h c) = 1%multmonoid).
Show proof.
Definition abgr_KernelArrowIn_map {A B C : abgr_category} (h : C --> A) (f : A --> B)
(H : h · f = ZeroArrow abgr_Zero C B) (c : (C : abgr)) : abgr_Kernel_subabgr f.
Show proof.
Lemma abgr_KernelArrowIn_ismonoidfun {A B C : abgr_category} (h : C --> A)
(f : A --> B) (H : h · f = ZeroArrow abgr_Zero C B) :
@ismonoidfun (C : abgr) (@abgr_Kernel_subabgr A B f) (@abgr_KernelArrowIn_map A B C h f H).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use total2_paths_f.
+ exact (binopfunisbinopfun (h : monoidfun (C : abgr) (A : abgr)) x x').
+ use proofirrelevance. use propproperty.
- use total2_paths_f.
+ exact (monoidfununel h).
+ use proofirrelevance. use propproperty.
- use make_isbinopfun. intros x x'. use total2_paths_f.
+ exact (binopfunisbinopfun (h : monoidfun (C : abgr) (A : abgr)) x x').
+ use proofirrelevance. use propproperty.
- use total2_paths_f.
+ exact (monoidfununel h).
+ use proofirrelevance. use propproperty.
Definition abgr_KernelArrowIn {A B C : abgr_category} (h : C --> A) (f : A --> B)
(H : h · f = ZeroArrow abgr_Zero C B) :
abgr_category⟦C, carrierofasubabgr (abgr_Kernel_subabgr f)⟧.
Show proof.
use monoidfunconstr.
- exact (abgr_KernelArrowIn_map h f H).
- exact (abgr_KernelArrowIn_ismonoidfun h f H).
- exact (abgr_KernelArrowIn_map h f H).
- exact (abgr_KernelArrowIn_ismonoidfun h f H).
Definition abgr_Kernel_isKernel_KernelArrrow {A B C : abgr} (f : abgr_category ⟦A, B⟧)
(h : abgr_category ⟦C, A⟧) (H' : h · f = ZeroArrow abgr_Zero C B) :
∑ ψ : abgr_category ⟦C, carrierofasubabgr (abgr_Kernel_subabgr f)⟧,
ψ · abgr_Kernel_monoidfun f = h.
Show proof.
use tpair.
- exact (abgr_KernelArrowIn h f H').
- use monoidfun_paths. use funextfun. intros x. use idpath.
- exact (abgr_KernelArrowIn h f H').
- use monoidfun_paths. use funextfun. intros x. use idpath.
Definition abgr_Kernel_isKernel_uniqueness {A B C : abgr} (f : abgr_category ⟦A, B⟧)
(h : abgr_category ⟦C, A⟧) (H' : h · f = ZeroArrow abgr_Zero C B)
(t : ∑ (t1 : abgr_category ⟦C, carrierofasubabgr (abgr_Kernel_subabgr f)⟧),
t1 · abgr_Kernel_monoidfun f = h) :
t = abgr_Kernel_isKernel_KernelArrrow f h H'.
Show proof.
use total2_paths_f.
- use monoidfun_paths. use funextfun. intros x. use total2_paths_f.
+ exact (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x).
+ use proofirrelevance. use propproperty.
- use proofirrelevance. use setproperty.
- use monoidfun_paths. use funextfun. intros x. use total2_paths_f.
+ exact (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x).
+ use proofirrelevance. use propproperty.
- use proofirrelevance. use setproperty.
Definition abgr_Kernel_isKernel {A B : abgr} (f : abgr_category⟦A, B⟧) :
isKernel abgr_Zero (abgr_Kernel_monoidfun f) f (abgr_Kernel_eq f).
Show proof.
use make_isKernel.
- intros w h H'.
use make_iscontr.
+ exact (abgr_Kernel_isKernel_KernelArrrow f h H').
+ intros t. exact (abgr_Kernel_isKernel_uniqueness f h H' t).
- intros w h H'.
use make_iscontr.
+ exact (abgr_Kernel_isKernel_KernelArrrow f h H').
+ intros t. exact (abgr_Kernel_isKernel_uniqueness f h H' t).
Definition abgr_Kernel {A B : abgr} (f : monoidfun A B) :
Kernel abgr_Zero f :=
make_Kernel (abgr_Zero) (abgr_Kernel_monoidfun f) f (abgr_Kernel_eq f) (abgr_Kernel_isKernel f).
Corollary abgr_Kernels : Kernels abgr_Zero.
Show proof.
Cokernels
- Let f : X --> Y be a morphism of abelian groups. A cokernel for f is given by the quotient quotient group Y/(Im f) together with the canonical morphism Y --> Y/(Im f).
Subgroup gives an equivalence relation.
Definition abgr_Cokernel_eqrel_istrans {A B : abgr} (f : monoidfun A B) :
istrans (λ b1 b2 : B, ∃ a : A, f a = (b1 * grinv B b2)%multmonoid).
Show proof.
intros x1 x2 x3 y1 y2.
use (hinhuniv _ y1). intros y1'.
use (hinhuniv _ y2). intros y2'.
use hinhpr.
use tpair.
- exact (@op A (pr1 y1') (pr1 y2')).
- use (pathscomp0 (binopfunisbinopfun f (pr1 y1') (pr1 y2'))).
rewrite (pr2 y1'). rewrite (pr2 y2').
rewrite <- assocax. rewrite (assocax _ _ _ x2). rewrite (grlinvax B). rewrite (runax B).
use idpath.
use (hinhuniv _ y1). intros y1'.
use (hinhuniv _ y2). intros y2'.
use hinhpr.
use tpair.
- exact (@op A (pr1 y1') (pr1 y2')).
- use (pathscomp0 (binopfunisbinopfun f (pr1 y1') (pr1 y2'))).
rewrite (pr2 y1'). rewrite (pr2 y2').
rewrite <- assocax. rewrite (assocax _ _ _ x2). rewrite (grlinvax B). rewrite (runax B).
use idpath.
Definition abgr_Cokernel_eqrel_isrefl {A B : abgr} (f : monoidfun A B) :
isrefl (λ b1 b2 : B, ∃ a : A, f a = (b1 * grinv B b2)%multmonoid).
Show proof.
intros x1 P X. use X. clear P X.
use tpair.
- exact (unel A).
- cbn. rewrite (grrinvax B). use (monoidfununel f).
use tpair.
- exact (unel A).
- cbn. rewrite (grrinvax B). use (monoidfununel f).
Definition abgr_Cokernel_eqrel_issymm {A B : abgr} (f : monoidfun A B) :
issymm (λ b1 b2 : B, ∃ a : A, f a = (b1 * grinv B b2)%multmonoid).
Show proof.
intros x1 x2 x3.
use (hinhuniv _ x3). intros x3'.
intros P X. use X. clear P X.
use tpair.
- exact (grinv A (pr1 x3')).
- use (pathscomp0 (monoidfuninvtoinv f (pr1 x3'))).
rewrite (pr2 x3'). rewrite grinvop. use two_arg_paths.
+ use grinvinv.
+ use idpath.
use (hinhuniv _ x3). intros x3'.
intros P X. use X. clear P X.
use tpair.
- exact (grinv A (pr1 x3')).
- use (pathscomp0 (monoidfuninvtoinv f (pr1 x3'))).
rewrite (pr2 x3'). rewrite grinvop. use two_arg_paths.
+ use grinvinv.
+ use idpath.
Definition abgr_Cokernel_eqrel {A B : abgr} (f : monoidfun A B) : eqrel B :=
@eqrelconstr B (λ b1 : B, λ b2 : B, ∃ a : A, (f a) = (op b1 (grinv B b2)))
(abgr_Cokernel_eqrel_istrans f) (abgr_Cokernel_eqrel_isrefl f)
(abgr_Cokernel_eqrel_issymm f).
Definition abgr_Cokernel_abgr_isbinoprel {A B : abgr} (f : monoidfun A B) :
isbinophrel (λ b1 b2 : pr1 B, ∃ a : pr1 A, pr1 f a = (b1 * grinv B b2)%multmonoid).
Show proof.
use isbinophrelif.
- exact (commax B).
- intros x1 x2 x3 y1. use (hinhuniv _ y1). intros y1'. use hinhpr.
use tpair.
+ exact (pr1 y1').
+ use (pathscomp0 (pr2 y1')). rewrite grinvop.
rewrite (commax B x3). rewrite (assocax B). rewrite (commax B x3).
rewrite (assocax B). rewrite (grlinvax B x3). rewrite (runax B). use idpath.
- exact (commax B).
- intros x1 x2 x3 y1. use (hinhuniv _ y1). intros y1'. use hinhpr.
use tpair.
+ exact (pr1 y1').
+ use (pathscomp0 (pr2 y1')). rewrite grinvop.
rewrite (commax B x3). rewrite (assocax B). rewrite (commax B x3).
rewrite (assocax B). rewrite (grlinvax B x3). rewrite (runax B). use idpath.
Definition abgr_Cokernel_abgr {A B : abgr} (f : monoidfun A B) : abgr :=
@abgrquot B (make_binopeqrel (abgr_Cokernel_eqrel f) (abgr_Cokernel_abgr_isbinoprel f)).
Lemma abgr_CokernelArrow_ismonoidfun {A B : abgr} (f : monoidfun A B) :
@ismonoidfun B (@abgr_Cokernel_abgr A B f) (@setquotpr B (@abgr_Cokernel_eqrel A B f)).
Show proof.
Definition abgr_CokernelArrow {A B : abgr} (f : monoidfun A B) :
abgr_category⟦B, abgr_Cokernel_abgr f⟧.
Show proof.
use monoidfunconstr.
- exact (setquotpr (abgr_Cokernel_eqrel f)).
- exact (abgr_CokernelArrow_ismonoidfun f).
- exact (setquotpr (abgr_Cokernel_eqrel f)).
- exact (abgr_CokernelArrow_ismonoidfun f).
Lemma abgr_Cokernel_monoidfun_issurjective {A B : abgr} (f : monoidfun A B) :
issurjective (pr1 (abgr_CokernelArrow f)).
Show proof.
Definition abgr_Cokernel_eq {A B : abgr} (f : abgr_category⟦A, B⟧) :
f · abgr_CokernelArrow f = ZeroArrow abgr_Zero A (abgr_Cokernel_abgr f).
Show proof.
use monoidfun_paths. use funextfun. intros a.
use (iscompsetquotpr (abgr_Cokernel_eqrel f)).
use hinhpr.
use tpair.
- exact a.
- use (pathscomp0 (pathsinv0 (runax B (pr1 f a)))).
use two_arg_paths.
+ use idpath.
+ use pathsinv0. use (grinvunel B).
use (iscompsetquotpr (abgr_Cokernel_eqrel f)).
use hinhpr.
use tpair.
- exact a.
- use (pathscomp0 (pathsinv0 (runax B (pr1 f a)))).
use two_arg_paths.
+ use idpath.
+ use pathsinv0. use (grinvunel B).
Definition abgr_CokernelArrowOutUniv_iscomprelfun {A B C : abgr_category}
(f : A --> B) (h : B --> C) (H : f · h = ZeroArrow abgr_Zero A C) :
iscomprelfun (λ b1 b2 : pr1 B, ∃ a : pr1 A, pr1 f a = (b1 * grinv (abgrtogr B) b2)%multmonoid)
(pr1 h).
Show proof.
intros x x' X.
use (squash_to_prop X (setproperty (C : abgr) (pr1 h x) (pr1 h x'))). intros X'.
use (grrcan (abgrtogr C) ((pr1 h) (grinv (abgrtogr B) x'))).
use (pathscomp0 _ (binopfunisbinopfun
(h : monoidfun (B : abgr) (C : abgr)) x' (grinv (B : abgr) x'))).
use (pathscomp0 _ (! maponpaths (λ xx : (B : abgr), pr1 h xx) (grrinvax (B : abgr) x'))).
use (pathscomp0 _ (! (monoidfununel h))).
use (pathscomp0 _ (toforallpaths _ _ _ (base_paths _ _ H) (pr1 X'))).
use (pathscomp0 (! (binopfunisbinopfun
(h : monoidfun (B : abgr) (C : abgr)) x (grinv (B : abgr) x')))).
use maponpaths. use pathsinv0. exact (pr2 X').
use (squash_to_prop X (setproperty (C : abgr) (pr1 h x) (pr1 h x'))). intros X'.
use (grrcan (abgrtogr C) ((pr1 h) (grinv (abgrtogr B) x'))).
use (pathscomp0 _ (binopfunisbinopfun
(h : monoidfun (B : abgr) (C : abgr)) x' (grinv (B : abgr) x'))).
use (pathscomp0 _ (! maponpaths (λ xx : (B : abgr), pr1 h xx) (grrinvax (B : abgr) x'))).
use (pathscomp0 _ (! (monoidfununel h))).
use (pathscomp0 _ (toforallpaths _ _ _ (base_paths _ _ H) (pr1 X'))).
use (pathscomp0 (! (binopfunisbinopfun
(h : monoidfun (B : abgr) (C : abgr)) x (grinv (B : abgr) x')))).
use maponpaths. use pathsinv0. exact (pr2 X').
Definition abgr_CokernelOut_map {A B C : abgr_category} (f : A --> B)
(h : B --> C) (H : f · h = ZeroArrow abgr_Zero A C) :
(abgr_Cokernel_abgr f) -> (pr1 C) :=
setquotuniv (λ b1 b2 : pr1 B, ∃ a : pr1 A, pr1 f a = (b1 * grinv (abgrtogr B) b2)%multmonoid)
(pr1 C) (pr1 h) (abgr_CokernelArrowOutUniv_iscomprelfun f h H).
Definition abgr_CokernelOut_ismonoidfun {A B C : abgr} (f : abgr_category ⟦A, B⟧)
(h : abgr_category ⟦B, C⟧) (H : f · h = ZeroArrow abgr_Zero A C) :
@ismonoidfun (@abgr_Cokernel_abgr A B f) C (@abgr_CokernelOut_map A B C f h H).
Show proof.
use make_ismonoidfun.
- exact (@isbinopfun_twooutof3b
(pr1 B) (abgr_Cokernel_abgr f) C
(pr1 (abgr_CokernelArrow f))
(abgr_CokernelOut_map f h H)
(abgr_Cokernel_monoidfun_issurjective f)
(binopfunisbinopfun (h : monoidfun B C))
(binopfunisbinopfun ((abgr_CokernelArrow f) : monoidfun B _))).
- exact (monoidfununel (h : monoidfun B C)).
- exact (@isbinopfun_twooutof3b
(pr1 B) (abgr_Cokernel_abgr f) C
(pr1 (abgr_CokernelArrow f))
(abgr_CokernelOut_map f h H)
(abgr_Cokernel_monoidfun_issurjective f)
(binopfunisbinopfun (h : monoidfun B C))
(binopfunisbinopfun ((abgr_CokernelArrow f) : monoidfun B _))).
- exact (monoidfununel (h : monoidfun B C)).
Definition abgr_CokernelOut {A B C : abgr} (f : abgr_category⟦A, B⟧) (h : abgr_category⟦B, C⟧)
(H : f · h = ZeroArrow abgr_Zero A C) : monoidfun (abgr_Cokernel_abgr f) C :=
monoidfunconstr (abgr_CokernelOut_ismonoidfun f h H).
Lemma abgr_CokernelOut_Comm {A B C : abgr} (f : abgr_category⟦A, B⟧) (h : abgr_category⟦B, C⟧)
(H : f · h = ZeroArrow abgr_Zero A C) :
monoidfuncomp (abgr_CokernelArrow f) (abgr_CokernelOut f h H) = h.
Show proof.
Definition make_abgr_CokernelOut {A B C : abgr} (f : abgr_category ⟦A, B⟧)
(h : abgr_category ⟦B, C⟧) (H : f · h = ZeroArrow abgr_Zero A C) :
∑ ψ : abgr_category⟦abgr_Cokernel_abgr f, C⟧, abgr_CokernelArrow f · ψ = h.
Show proof.
Lemma abgr_isCokernel_uniquenss {A B C : abgr} (f : abgr_category⟦A, B⟧) (h : abgr_category⟦B, C⟧)
(H : f · h = ZeroArrow abgr_Zero A C)
(t : ∑ ψ : abgr_category ⟦abgr_Cokernel_abgr f, C⟧, abgr_CokernelArrow f · ψ = h) :
t = make_abgr_CokernelOut f h H.
Show proof.
use total2_paths_f.
- use monoidfun_paths. use funextfun. intros x.
use (squash_to_prop (abgr_Cokernel_monoidfun_issurjective f x) (setproperty C _ _)).
intros hf. rewrite <- (hfiberpr2 _ _ hf).
exact (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) (hfiberpr1 _ _ hf)).
- use proofirrelevance. use homset_property.
- use monoidfun_paths. use funextfun. intros x.
use (squash_to_prop (abgr_Cokernel_monoidfun_issurjective f x) (setproperty C _ _)).
intros hf. rewrite <- (hfiberpr2 _ _ hf).
exact (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) (hfiberpr1 _ _ hf)).
- use proofirrelevance. use homset_property.
Definition abgr_isCokernel {A B : abgr} (f : abgr_category⟦A, B⟧) :
isCokernel abgr_Zero f (abgr_CokernelArrow f) (abgr_Cokernel_eq f).
Show proof.
use make_isCokernel.
- intros C h H. use make_iscontr.
+ exact (make_abgr_CokernelOut f h H).
+ intros t. exact (abgr_isCokernel_uniquenss f h H t).
- intros C h H. use make_iscontr.
+ exact (make_abgr_CokernelOut f h H).
+ intros t. exact (abgr_isCokernel_uniquenss f h H t).
Definition abgr_Cokernel {A B : abgr} (f : abgr_category⟦A, B⟧) : Cokernel abgr_Zero f :=
make_Cokernel abgr_Zero f (abgr_CokernelArrow f) (abgr_Cokernel_eq f) (abgr_isCokernel f).
Corollary abgr_Cokernels : Cokernels abgr_Zero.
Show proof.
End abgr_kernels_and_cokernels.
Definition abgr_epi_hfiber_inhabited
{A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) (b : B)
(H : setquotpr (abgr_Cokernel_eqrel f) b =
setquotpr (abgr_Cokernel_eqrel f) 1%multmonoid) : ∥ hfiber (pr1 f) b ∥.
Show proof.
set (tmp := weqpathsinsetquot (abgr_Cokernel_eqrel f) b (unel _)).
use (hinhuniv _ ((invweq tmp) H)). intros Y. use hinhpr. induction Y as [t p].
rewrite grinvunel in p. rewrite (runax B) in p.
exact (make_hfiber (pr1 f) t p).
use (hinhuniv _ ((invweq tmp) H)). intros Y. use hinhpr. induction Y as [t p].
rewrite grinvunel in p. rewrite (runax B) in p.
exact (make_hfiber (pr1 f) t p).
Definition abgr_epi_issurjective {A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) :
issurjective (pr1 f).
Show proof.
intros x. use abgr_epi_hfiber_inhabited.
- exact isE.
- set (tmp := isE (abgr_Cokernel_abgr f) (abgr_CokernelArrow f)
(unelabgrfun B (abgr_Cokernel_abgr f))).
assert (H : f · abgr_CokernelArrow f = f · unelabgrfun B (abgr_Cokernel_abgr f)).
{
rewrite abgr_Cokernel_eq.
rewrite <- abgr_Zero_arrow_comp.
rewrite ZeroArrow_comp_right.
use idpath.
}
exact (toforallpaths _ _ _ (base_paths _ _ (tmp H)) x).
- exact isE.
- set (tmp := isE (abgr_Cokernel_abgr f) (abgr_CokernelArrow f)
(unelabgrfun B (abgr_Cokernel_abgr f))).
assert (H : f · abgr_CokernelArrow f = f · unelabgrfun B (abgr_Cokernel_abgr f)).
{
rewrite abgr_Cokernel_eq.
rewrite <- abgr_Zero_arrow_comp.
rewrite ZeroArrow_comp_right.
use idpath.
}
exact (toforallpaths _ _ _ (base_paths _ _ (tmp H)) x).
Lemma nat_nat_prod_abgr_monoidfun_paths {A B : abgr} (a1 a2 : A) (f : monoidfun A B)
(H : f a1 = f a2) : monoidfuncomp (nat_nat_prod_abmonoid_monoidfun a1) f =
monoidfuncomp (nat_nat_prod_abmonoid_monoidfun a2) f.
Show proof.
use monoidfun_paths. use funextfun. intros x. induction x as [x1 x2]. cbn.
unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
unfold nat_nat_to_monoid_fun. Opaque nat_to_monoid_fun. cbn.
use (pathscomp0 (binopfunisbinopfun f _ _)).
use (pathscomp0 _ (! (binopfunisbinopfun f _ _))). cbn.
rewrite (monoidfun_nat_to_monoid_fun f a1 x1).
rewrite (monoidfun_nat_to_monoid_fun f a2 x1).
rewrite (monoidfun_nat_to_monoid_fun f (grinv A a1) x2).
rewrite (monoidfun_nat_to_monoid_fun f (grinv A a2) x2).
use two_arg_paths.
- induction H. use idpath.
- assert (e : f (grinv A a1) = f (grinv A a2)). {
use (@grlcan B _ _ (pr1 f a1)).
use (pathscomp0 (! binopfunisbinopfun f a1 (grinv A a1))).
use (pathscomp0 (maponpaths (pr1 f) (grrinvax A a1))).
cbn in H. rewrite H.
use (pathscomp0 _ (binopfunisbinopfun f a2 (grinv A a2))).
use (pathscomp0 _ (! (maponpaths (pr1 f) (grrinvax A a2)))).
use idpath.
}
induction e. use idpath.
Transparent nat_to_monoid_fun.unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
unfold nat_nat_to_monoid_fun. Opaque nat_to_monoid_fun. cbn.
use (pathscomp0 (binopfunisbinopfun f _ _)).
use (pathscomp0 _ (! (binopfunisbinopfun f _ _))). cbn.
rewrite (monoidfun_nat_to_monoid_fun f a1 x1).
rewrite (monoidfun_nat_to_monoid_fun f a2 x1).
rewrite (monoidfun_nat_to_monoid_fun f (grinv A a1) x2).
rewrite (monoidfun_nat_to_monoid_fun f (grinv A a2) x2).
use two_arg_paths.
- induction H. use idpath.
- assert (e : f (grinv A a1) = f (grinv A a2)). {
use (@grlcan B _ _ (pr1 f a1)).
use (pathscomp0 (! binopfunisbinopfun f a1 (grinv A a1))).
use (pathscomp0 (maponpaths (pr1 f) (grrinvax A a1))).
cbn in H. rewrite H.
use (pathscomp0 _ (binopfunisbinopfun f a2 (grinv A a2))).
use (pathscomp0 _ (! (maponpaths (pr1 f) (grrinvax A a2)))).
use idpath.
}
induction e. use idpath.
Lemma abgr_monoidfun_precomp {A :abmonoid} {B C : abgr} (f1 f2 : monoidfun B C)
(g : monoidfun A B) (H : issurjective (pr1 g)) :
monoidfuncomp g f1 = monoidfuncomp g f2 -> f1 = f2.
Show proof.
intros e. use monoidfun_paths. use funextfun. intros x.
use (squash_to_prop (H x) (setproperty C _ _)). intros hf.
rewrite <- (hfiberpr2 _ _ hf).
exact (toforallpaths _ _ _ (base_paths _ _ e) (hfiberpr1 _ _ hf)).
use (squash_to_prop (H x) (setproperty C _ _)). intros hf.
rewrite <- (hfiberpr2 _ _ hf).
exact (toforallpaths _ _ _ (base_paths _ _ e) (hfiberpr1 _ _ hf)).
Lemma hz_abgr_fun_monoifun_paths {A B : abgr} (a1 a2 : A) (f : monoidfun A B) (H : f a1 = f a2) :
monoidfuncomp (hz_abgr_fun_monoidfun a1) f = monoidfuncomp (hz_abgr_fun_monoidfun a2) f.
Show proof.
use (@abgr_monoidfun_precomp
(abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig))
hzaddabgr B
(monoidfuncomp (hz_abgr_fun_monoidfun a1) f)
(monoidfuncomp (hz_abgr_fun_monoidfun a2) f)
hz_abmonoid_monoidfun).
- use issurjsetquotpr.
- rewrite monoidfunassoc. rewrite monoidfunassoc.
rewrite abgr_natnat_hz_X_comm. rewrite abgr_natnat_hz_X_comm.
exact (nat_nat_prod_abgr_monoidfun_paths a1 a2 f H).
(abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig))
hzaddabgr B
(monoidfuncomp (hz_abgr_fun_monoidfun a1) f)
(monoidfuncomp (hz_abgr_fun_monoidfun a2) f)
hz_abmonoid_monoidfun).
- use issurjsetquotpr.
- rewrite monoidfunassoc. rewrite monoidfunassoc.
rewrite abgr_natnat_hz_X_comm. rewrite abgr_natnat_hz_X_comm.
exact (nat_nat_prod_abgr_monoidfun_paths a1 a2 f H).
Definition abgr_monic_isincl {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
isincl (pr1 f).
Show proof.
intros b h1 h2.
use make_iscontr.
- use total2_paths_f.
+ set (e := hfiberpr2 _ _ h1 @ (! hfiberpr2 _ _ h2)).
set (tmp := isM hzaddabgr (hz_abgr_fun_monoidfun (pr1 h1))
(hz_abgr_fun_monoidfun (pr1 h2))
(hz_abgr_fun_monoifun_paths (pr1 h1) (pr1 h2) f e)).
set (e' := toforallpaths _ _ _ (base_paths _ _ tmp) hzone).
use (grrcan A (unel A)). use (grrcan A (unel A)). exact e'.
+ use proofirrelevance. use (setproperty B).
- intros t. use proofirrelevance. use isaset_hfiber.
+ use setproperty.
+ use setproperty.
use make_iscontr.
- use total2_paths_f.
+ set (e := hfiberpr2 _ _ h1 @ (! hfiberpr2 _ _ h2)).
set (tmp := isM hzaddabgr (hz_abgr_fun_monoidfun (pr1 h1))
(hz_abgr_fun_monoidfun (pr1 h2))
(hz_abgr_fun_monoifun_paths (pr1 h1) (pr1 h2) f e)).
set (e' := toforallpaths _ _ _ (base_paths _ _ tmp) hzone).
use (grrcan A (unel A)). use (grrcan A (unel A)). exact e'.
+ use proofirrelevance. use (setproperty B).
- intros t. use proofirrelevance. use isaset_hfiber.
+ use setproperty.
+ use setproperty.
Definition abgr_monic_isInjective {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
isInjective (pr1 f).
Show proof.
Lemma abgr_monic_paths {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) (a1 a2 : A) :
pr1 f a1 = pr1 f a2 -> a1 = a2.
Show proof.
Lemma abgr_monoidfun_postcomp {A B C : abgr} (f1 f2 : monoidfun A B) (g : monoidfun B C)
(isM : isMonic (g : abgr_category⟦B, C⟧)) :
monoidfuncomp f1 g = monoidfuncomp f2 g -> f1 = f2.
Show proof.
intros e. use monoidfun_paths. use funextfun. intros x.
use (invmap (make_weq _ (abgr_monic_isInjective g isM (pr1 f1 x) (pr1 f2 x)))).
exact (toforallpaths _ _ _ (base_paths _ _ e) x).
use (invmap (make_weq _ (abgr_monic_isInjective g isM (pr1 f1 x) (pr1 f2 x)))).
exact (toforallpaths _ _ _ (base_paths _ _ e) x).
End abgr_monics_and_epis.
Definition abgr_monic_kernel_in_hfiber_iscontr {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (h : abgr_category⟦C, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) =
ZeroArrow abgr_Zero C (abgr_Cokernel f)) (c : C) :
iscontr (hfiber (pr1 f) (pr1 h c)).
Show proof.
use (squash_to_prop
((invweq (weqpathsinsetquot (abgr_Cokernel_eqrel f) (pr1 h c) (unel _)))
(toforallpaths _ _ _ (base_paths _ _ H) c)) (isapropiscontr _)).
intros hf.
use make_iscontr.
- use make_hfiber.
+ exact (pr1 hf).
+ use (pathscomp0 (pr2 hf)). rewrite grinvunel. use (runax B).
- intros t. use total2_paths_f.
+ use (invmap (make_weq _ (abgr_monic_isInjective f isM (pr1 t) (pr1 hf)))).
use (pathscomp0 (hfiberpr2 _ _ t)). use (pathscomp0 _ (! (pr2 hf))).
rewrite grinvunel. rewrite runax. use idpath.
+ use proofirrelevance. use (setproperty B).
((invweq (weqpathsinsetquot (abgr_Cokernel_eqrel f) (pr1 h c) (unel _)))
(toforallpaths _ _ _ (base_paths _ _ H) c)) (isapropiscontr _)).
intros hf.
use make_iscontr.
- use make_hfiber.
+ exact (pr1 hf).
+ use (pathscomp0 (pr2 hf)). rewrite grinvunel. use (runax B).
- intros t. use total2_paths_f.
+ use (invmap (make_weq _ (abgr_monic_isInjective f isM (pr1 t) (pr1 hf)))).
use (pathscomp0 (hfiberpr2 _ _ t)). use (pathscomp0 _ (! (pr2 hf))).
rewrite grinvunel. rewrite runax. use idpath.
+ use proofirrelevance. use (setproperty B).
Lemma abgr_monic_kernel_in_hfiber_mult_eq {A B : abgr} (f : abgr_category⟦A, B⟧)
(w : abgr) (x x' : w) (h : abgr_category⟦w, B⟧) (X : hfiber (pr1 f) (pr1 h x))
(X0 : hfiber (pr1 f) (pr1 h x')) :
pr1 f (pr1 X * pr1 X0)%multmonoid = pr1 h (x * x')%multmonoid.
Show proof.
Definition abgr_monic_kernel_in_hfiber_mult {A B : abgr} (f : abgr_category⟦A, B⟧)
(w : abgr) (x x' : w) (h : abgr_category⟦w, B⟧) :
hfiber (pr1 f) (pr1 h x) -> hfiber (pr1 f) (pr1 h x')
-> hfiber (pr1 f) (pr1 h (x * x')%multmonoid).
Show proof.
intros X X0.
exact (make_hfiber (pr1 f) ((pr1 X) * (pr1 X0))%multmonoid
(abgr_monic_kernel_in_hfiber_mult_eq f w x x' h X X0)).
exact (make_hfiber (pr1 f) ((pr1 X) * (pr1 X0))%multmonoid
(abgr_monic_kernel_in_hfiber_mult_eq f w x x' h X X0)).
Lemma abgr_monic_kernel_in_hfiber_unel_eq {A B C : abgr} (f : abgr_category⟦A, B⟧)
(h : abgr_category⟦C, B⟧) : pr1 f 1%multmonoid = pr1 h 1%multmonoid.
Show proof.
Definition abgr_monic_kernel_in_hfiber_unel {A B : abgr} (f : abgr_category⟦A, B⟧) (w : abgr)
(h : abgr_category⟦w, B⟧) : hfiber (pr1 f) (pr1 h 1%multmonoid) :=
make_hfiber (pr1 f) 1%multmonoid (abgr_monic_kernel_in_hfiber_unel_eq f h).
Definition abgr_monic_kernel_in {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f)
(w : abgr) (h: abgr_category⟦w, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero _ _) : w -> A.
Show proof.
intros x.
exact (hfiberpr1 _ _ (iscontrpr1 (@abgr_monic_kernel_in_hfiber_iscontr A B w f isM h H x))).
exact (hfiberpr1 _ _ (iscontrpr1 (@abgr_monic_kernel_in_hfiber_iscontr A B w f isM h H x))).
Definition abgr_monic_kernel_in_ismonoidfun {A B : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (w : abgr) (h: abgr_category⟦w, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero _ _) :
ismonoidfun (abgr_monic_kernel_in f isM w h H).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'.
set (t := abgr_monic_kernel_in_hfiber_iscontr f isM h H x).
set (tmp := abgr_monic_kernel_in_hfiber_mult
f w x x' h
(iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))
(iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x'))).
use pathscomp0.
+ exact (hfiberpr1 _ _ tmp).
+ unfold abgr_monic_kernel_in.
use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr
f isM h H (x * x')%multmonoid)))).
use pathsinv0.
exact (hfiberpr2 _ _ tmp).
+ use idpath.
- assert (e : iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H 1%multmonoid)
= (abgr_monic_kernel_in_hfiber_unel f w h)).
{
use total2_paths_f.
- use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr
f isM h H 1%multmonoid)))).
use pathsinv0.
exact (hfiberpr2 _ _ (abgr_monic_kernel_in_hfiber_unel f w h)).
- use proofirrelevance. use setproperty.
}
exact (base_paths _ _ e).
- use make_isbinopfun. intros x x'.
set (t := abgr_monic_kernel_in_hfiber_iscontr f isM h H x).
set (tmp := abgr_monic_kernel_in_hfiber_mult
f w x x' h
(iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))
(iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x'))).
use pathscomp0.
+ exact (hfiberpr1 _ _ tmp).
+ unfold abgr_monic_kernel_in.
use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr
f isM h H (x * x')%multmonoid)))).
use pathsinv0.
exact (hfiberpr2 _ _ tmp).
+ use idpath.
- assert (e : iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H 1%multmonoid)
= (abgr_monic_kernel_in_hfiber_unel f w h)).
{
use total2_paths_f.
- use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr
f isM h H 1%multmonoid)))).
use pathsinv0.
exact (hfiberpr2 _ _ (abgr_monic_kernel_in_hfiber_unel f w h)).
- use proofirrelevance. use setproperty.
}
exact (base_paths _ _ e).
Definition abgr_monic_kernel_in_monoidfun {A B : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (w : abgr) (h: abgr_category⟦w, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero _ _) :
monoidfun w A := monoidfunconstr (abgr_monic_kernel_in_ismonoidfun f isM w h H).
Definition abgr_monic_Kernel_eq {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
f · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero A (abgr_Cokernel f).
Show proof.
Lemma abgr_monic_Kernel_isKernel_comm {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (h : abgr_category⟦C, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero C (abgr_Cokernel f)):
monoidfuncomp (abgr_monic_kernel_in_monoidfun f isM C h H) f = h.
Show proof.
use monoidfun_paths. use funextfun. intros x.
exact (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))).
exact (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))).
Definition make_abgr_monic_Kernel_isKernel {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (h : abgr_category⟦C, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero C (abgr_Cokernel f)) :
∑ ψ : abgr_category ⟦C, A⟧, ψ · f = h.
Show proof.
use tpair.
- exact (abgr_monic_kernel_in_monoidfun f isM C h H).
- exact (abgr_monic_Kernel_isKernel_comm f isM h H).
- exact (abgr_monic_kernel_in_monoidfun f isM C h H).
- exact (abgr_monic_Kernel_isKernel_comm f isM h H).
Definition abgr_monic_Kernel_isKernel_uniqueness {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isM : isMonic f) (h : abgr_category⟦C, B⟧)
(H : h · CokernelArrow (abgr_Cokernel f) = ZeroArrow abgr_Zero C (abgr_Cokernel f))
(t : ∑ ψ : abgr_category ⟦C, A⟧, ψ · f = h) :
t = make_abgr_monic_Kernel_isKernel f isM h H.
Show proof.
use total2_paths_f.
- use monoidfun_paths. use funextfun. intros x.
use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x)).
use pathsinv0.
exact (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))).
- use proofirrelevance. use setproperty.
- use monoidfun_paths. use funextfun. intros x.
use (invmap (make_weq _ (abgr_monic_isInjective f isM _ _))).
use (pathscomp0 (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x)).
use pathsinv0.
exact (hfiberpr2 _ _ (iscontrpr1 (abgr_monic_kernel_in_hfiber_iscontr f isM h H x))).
- use proofirrelevance. use setproperty.
Definition abgr_monic_Kernel_isKernel {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
isKernel abgr_Zero f (CokernelArrow (abgr_Cokernel f))
(CokernelCompZero abgr_Zero (abgr_Cokernel f)).
Show proof.
use make_isKernel.
- intros w h H.
use make_iscontr.
+ exact (make_abgr_monic_Kernel_isKernel f isM h H).
+ exact (abgr_monic_Kernel_isKernel_uniqueness f isM h H).
- intros w h H.
use make_iscontr.
+ exact (make_abgr_monic_Kernel_isKernel f isM h H).
+ exact (abgr_monic_Kernel_isKernel_uniqueness f isM h H).
Definition abgr_monic_kernel {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
Kernel abgr_Zero (CokernelArrow (abgr_Cokernel f)) :=
make_Kernel abgr_Zero f (CokernelArrow (abgr_Cokernel f)) (abgr_monic_Kernel_eq f isM)
(abgr_monic_Kernel_isKernel f isM).
Lemma abgr_monic_kernel_comp {A B : abgr} (f : abgr_category⟦A, B⟧) (isM : isMonic f) :
KernelArrow (abgr_monic_kernel f isM) = f.
Show proof.
Definition abgr_epi_cokernel_out_kernel_hsubtype {A B : abgr}
(f : abgr_category⟦A, B⟧) (a : A)
(H : pr1 f a = 1%multmonoid) : abgr_kernel_hsubtype f.
Show proof.
Lemma abgr_epi_cokernel_out_data_eq {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero (abgr_Kernel f) C) :
∏ x : abgr_kernel_hsubtype f, pr1 h (pr1carrier (abgr_kernel_hsubtype f) x) = 1%multmonoid.
Show proof.
Lemma abgr_epi_cokernel_out_data_hfibers_to_unel {A B : abgr} (f : abgr_category⟦A, B⟧) (b : B)
(hfib1 hfib2 : hfiber (pr1 f) b) :
(pr1 f) ((pr1 hfib1) * (grinv A (pr1 hfib2)))%multmonoid = unel B.
Show proof.
rewrite (pr1 (pr2 f)).
use (grrcan (abgrtogr B) (pr1 f (pr1 hfib2))).
rewrite (assocax B). rewrite <- (pr1 (pr2 f)).
rewrite (grlinvax A). rewrite (pr2 (pr2 f)).
rewrite (runax B). rewrite (lunax B).
rewrite (pr2 hfib1). rewrite (pr2 hfib2).
use idpath.
use (grrcan (abgrtogr B) (pr1 f (pr1 hfib2))).
rewrite (assocax B). rewrite <- (pr1 (pr2 f)).
rewrite (grlinvax A). rewrite (pr2 (pr2 f)).
rewrite (runax B). rewrite (lunax B).
rewrite (pr2 hfib1). rewrite (pr2 hfib2).
use idpath.
Lemma abgr_epi_cokernel_out_data_hfiber_eq {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) (b : B)
(X : hfiber (pr1 f) b) : ∏ hfib : hfiber (pr1 f) b, pr1 h (pr1 hfib) = pr1 h (pr1 X).
Show proof.
intros hfib.
use (grrcan C (grinv (abgrtogr C) (pr1 h (pr1 X)))).
rewrite (grrinvax C).
set (e1 := abgr_epi_cokernel_out_data_hfibers_to_unel f b hfib X).
set (tmp1 := ! (monoidfuninvtoinv h (hfiberpr1 _ _ X))). cbn in tmp1.
use (pathscomp0 (maponpaths (λ k : _, ((pr1 h (pr1 hfib)) * k)%multmonoid) tmp1)).
rewrite <- (pr1 (pr2 h)).
set (tmp2 := abgr_epi_cokernel_out_data_eq f isE h H).
set (tmp3 := abgr_epi_cokernel_out_kernel_hsubtype
f (pr1 hfib * grinv A (pr1 X))%multmonoid e1).
set (tmp4 := tmp2 tmp3). cbn in tmp4. exact tmp4.
use (grrcan C (grinv (abgrtogr C) (pr1 h (pr1 X)))).
rewrite (grrinvax C).
set (e1 := abgr_epi_cokernel_out_data_hfibers_to_unel f b hfib X).
set (tmp1 := ! (monoidfuninvtoinv h (hfiberpr1 _ _ X))). cbn in tmp1.
use (pathscomp0 (maponpaths (λ k : _, ((pr1 h (pr1 hfib)) * k)%multmonoid) tmp1)).
rewrite <- (pr1 (pr2 h)).
set (tmp2 := abgr_epi_cokernel_out_data_eq f isE h H).
set (tmp3 := abgr_epi_cokernel_out_kernel_hsubtype
f (pr1 hfib * grinv A (pr1 X))%multmonoid e1).
set (tmp4 := tmp2 tmp3). cbn in tmp4. exact tmp4.
Lemma abgr_epi_CokernelOut_iscontr {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) (b : B) :
iscontr (∑ x : C, ∏ (hfib : hfiber (pr1 f) b), pr1 h (pr1 hfib) = x).
Show proof.
use (squash_to_prop (abgr_epi_issurjective f isE b) (isapropiscontr _)).
intros X. use make_iscontr.
- use tpair.
+ exact (pr1 h (pr1 X)).
+ exact (abgr_epi_cokernel_out_data_hfiber_eq f isE h H b X).
- intros t. use total2_paths_f.
+ exact (! ((pr2 t) X)).
+ use proofirrelevance. use impred. intros t0. use (setproperty C).
intros X. use make_iscontr.
- use tpair.
+ exact (pr1 h (pr1 X)).
+ exact (abgr_epi_cokernel_out_data_hfiber_eq f isE h H b X).
- intros t. use total2_paths_f.
+ exact (! ((pr2 t) X)).
+ use proofirrelevance. use impred. intros t0. use (setproperty C).
Definition abgr_epi_CokernelOut_mult_eq {A B C : abgr} (b1 b2 : B)
(f : abgr_category⟦A, B⟧) (isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _)
(X : ∑ x : C, ∏ hfib : hfiber (pr1 f) b1, pr1 h (pr1 hfib) = x)
(X0 : ∑ x : C, ∏ hfib : hfiber (pr1 f) b2, pr1 h (pr1 hfib) = x) :
∏ hfib : hfiber (pr1 f) (b1 * b2)%multmonoid, pr1 h (pr1 hfib) = (pr1 X * pr1 X0)%multmonoid.
Show proof.
intros hfib.
use (squash_to_prop (abgr_epi_issurjective f isE b1) (setproperty C _ _)). intros X1.
use (squash_to_prop (abgr_epi_issurjective f isE b2) (setproperty C _ _)). intros X2.
rewrite <- ((pr2 X) X1). rewrite <- ((pr2 X0) X2). rewrite <- (pr1 (pr2 h)).
exact (abgr_epi_cokernel_out_data_hfiber_eq
f isE h H (b1 * b2)%multmonoid (hfiberbinop (f : monoidfun _ _) b1 b2 X1 X2) hfib).
use (squash_to_prop (abgr_epi_issurjective f isE b1) (setproperty C _ _)). intros X1.
use (squash_to_prop (abgr_epi_issurjective f isE b2) (setproperty C _ _)). intros X2.
rewrite <- ((pr2 X) X1). rewrite <- ((pr2 X0) X2). rewrite <- (pr1 (pr2 h)).
exact (abgr_epi_cokernel_out_data_hfiber_eq
f isE h H (b1 * b2)%multmonoid (hfiberbinop (f : monoidfun _ _) b1 b2 X1 X2) hfib).
Definition abgr_epi_cokernel_out_data_mult {A B C : abgr} (b1 b2 : B)
(f : abgr_category⟦A, B⟧) (isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) :
(∑ x : C, ∏ (hfib : hfiber (pr1 f) b1), pr1 h (pr1 hfib) = x) ->
(∑ x : C, ∏ (hfib : hfiber (pr1 f) b2), pr1 h (pr1 hfib) = x) ->
(∑ x : C, ∏ (hfib : hfiber (pr1 f) (b1 * b2)%multmonoid), pr1 h (pr1 hfib) = x).
Show proof.
intros X X0.
exact (tpair _ ((pr1 X) * (pr1 X0))%multmonoid
(abgr_epi_CokernelOut_mult_eq b1 b2 f isE h H X X0)).
exact (tpair _ ((pr1 X) * (pr1 X0))%multmonoid
(abgr_epi_CokernelOut_mult_eq b1 b2 f isE h H X X0)).
Definition abgr_epi_cokernel_out_data_unel_eq {A B C : abgr}
(f : abgr_category⟦A, B⟧) (isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) :
∏ hfib : hfiber (pr1 f) 1%multmonoid, pr1 h (pr1 hfib) = 1%multmonoid.
Show proof.
intros hfib.
set (hfib_unel := make_hfiber (pr1 f) 1%multmonoid (pr2 (pr2 f))).
rewrite (abgr_epi_cokernel_out_data_hfiber_eq f isE h H 1%multmonoid hfib_unel hfib).
exact (monoidfununel h).
set (hfib_unel := make_hfiber (pr1 f) 1%multmonoid (pr2 (pr2 f))).
rewrite (abgr_epi_cokernel_out_data_hfiber_eq f isE h H 1%multmonoid hfib_unel hfib).
exact (monoidfununel h).
Definition abgr_epi_cokernel_out_data_unel {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) :
( ∑ x : C, ∏ (hfib : hfiber (pr1 f) 1%multmonoid), pr1 h (pr1 hfib) = x) :=
tpair _ 1%multmonoid (abgr_epi_cokernel_out_data_unel_eq f isE h H).
Lemma abgr_epi_cokernel_out_ismonoidfun {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) :
ismonoidfun (λ b : B, (pr1 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H b)))).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'.
set (HH0 := abgr_epi_cokernel_out_data_mult
x x' f isE h H
(iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x))
(iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x'))).
assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid) = HH0).
{
set (tmp := abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid).
rewrite (pr2 tmp). use pathsinv0. rewrite (pr2 tmp).
use idpath.
}
exact (base_paths _ _ HH).
- assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)
= abgr_epi_cokernel_out_data_unel f isE h H).
{
rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)).
use pathsinv0.
rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)).
use idpath.
}
exact (base_paths _ _ HH).
- use make_isbinopfun. intros x x'.
set (HH0 := abgr_epi_cokernel_out_data_mult
x x' f isE h H
(iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x))
(iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x'))).
assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid) = HH0).
{
set (tmp := abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid).
rewrite (pr2 tmp). use pathsinv0. rewrite (pr2 tmp).
use idpath.
}
exact (base_paths _ _ HH).
- assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)
= abgr_epi_cokernel_out_data_unel f isE h H).
{
rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)).
use pathsinv0.
rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)).
use idpath.
}
exact (base_paths _ _ HH).
Definition abgr_epi_cokernel_out_monoidfun {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) :
monoidfun B C := monoidfunconstr (abgr_epi_cokernel_out_ismonoidfun f isE h H).
Definition abgr_epi_cokernel_eq {A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) :
KernelArrow (abgr_Kernel f) · f = ZeroArrow abgr_Zero _ _.
Show proof.
Lemma abgr_epi_cokernel_isCokernel_comm {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero (abgr_Kernel f) C) :
f · abgr_epi_cokernel_out_monoidfun f isE h H = h.
Show proof.
use total2_paths_f.
- use funextfun. intros x. use pathsinv0.
exact (pr2 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (pr1 f x)))
(@make_hfiber _ _ (pr1 f) (pr1 f x) x (idpath _))).
- use proofirrelevance. use isapropismonoidfun.
- use funextfun. intros x. use pathsinv0.
exact (pr2 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (pr1 f x)))
(@make_hfiber _ _ (pr1 f) (pr1 f x) x (idpath _))).
- use proofirrelevance. use isapropismonoidfun.
Definition make_abgr_epi_cokernel_isCokernel {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero (abgr_Kernel f) C) :
∑ ψ : abgr_category ⟦B, C⟧, f · ψ = h.
Show proof.
use tpair.
- exact (abgr_epi_cokernel_out_monoidfun f isE h H).
- exact (abgr_epi_cokernel_isCokernel_comm f isE h H).
- exact (abgr_epi_cokernel_out_monoidfun f isE h H).
- exact (abgr_epi_cokernel_isCokernel_comm f isE h H).
Lemma abgr_epi_cokernel_isCokernel_uniqueness {A B C : abgr} (f : abgr_category⟦A, B⟧)
(isE : isEpi f) (h : abgr_category⟦A, C⟧)
(H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero (abgr_Kernel f) C)
(t : ∑ ψ : abgr_category ⟦B, C⟧, f · ψ = h) :
t = make_abgr_epi_cokernel_isCokernel f isE h H.
Show proof.
use total2_paths_f.
- use isE. use (pathscomp0 (pr2 t)). use monoidfun_paths. use funextfun. intros x.
exact (pr2 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (pr1 f x)))
(@make_hfiber _ _ (pr1 f) (pr1 f x) x (idpath _))).
- use proofirrelevance. use setproperty.
- use isE. use (pathscomp0 (pr2 t)). use monoidfun_paths. use funextfun. intros x.
exact (pr2 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (pr1 f x)))
(@make_hfiber _ _ (pr1 f) (pr1 f x) x (idpath _))).
- use proofirrelevance. use setproperty.
Definition abgr_epi_cokernel_isCokernel {A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) :
isCokernel abgr_Zero (KernelArrow (abgr_Kernel f)) f (abgr_epi_cokernel_eq f isE).
Show proof.
use make_isCokernel.
- intros w h H. use make_iscontr.
+ exact (make_abgr_epi_cokernel_isCokernel f isE h H).
+ intros t. exact (abgr_epi_cokernel_isCokernel_uniqueness f isE h H t).
- intros w h H. use make_iscontr.
+ exact (make_abgr_epi_cokernel_isCokernel f isE h H).
+ intros t. exact (abgr_epi_cokernel_isCokernel_uniqueness f isE h H t).
Definition abgr_epi_cokernel {A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) :
Cokernel abgr_Zero (KernelArrow (abgr_Kernel f)) :=
make_Cokernel abgr_Zero (KernelArrow (abgr_Kernel f)) f _ (abgr_epi_cokernel_isCokernel f isE).
Definition abgr_epi_cokernel_comp {A B : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) :
CokernelArrow (abgr_epi_cokernel f isE) = f.
Show proof.
End abgr_monic_kernels_epi_cokernels.
Section abgr_abelian.
Definition abgr_Abelian : AbelianPreCat.
Show proof.
End abgr_abelian.
Definition abgr_Abelian : AbelianPreCat.
Show proof.
set (BinDS := to_BinDirectSums abgr_Additive).
use (make_Abelian abgr_category).
- use make_Data1.
+ exact abgr_Zero.
+ intros X Y. exact (BinDirectSum_BinProduct abgr_Additive (BinDS X Y)).
+ intros X Y. exact (BinDirectSum_BinCoproduct abgr_Additive (BinDS X Y)).
- use make_AbelianData.
+ use make_Data2.
* intros A B f. exact (abgr_Kernel f).
* intros A B f. exact (abgr_Cokernel f).
+ use make_MonicsAreKernels.
intros x y M.
exact (KernelisKernel abgr_Zero (abgr_monic_kernel M (MonicisMonic abgr_category M))).
+ use make_EpisAreCokernels.
intros x y E.
exact (CokernelisCokernel abgr_Zero (abgr_epi_cokernel E (EpiisEpi abgr_category E))).
use (make_Abelian abgr_category).
- use make_Data1.
+ exact abgr_Zero.
+ intros X Y. exact (BinDirectSum_BinProduct abgr_Additive (BinDS X Y)).
+ intros X Y. exact (BinDirectSum_BinCoproduct abgr_Additive (BinDS X Y)).
- use make_AbelianData.
+ use make_Data2.
* intros A B f. exact (abgr_Kernel f).
* intros A B f. exact (abgr_Cokernel f).
+ use make_MonicsAreKernels.
intros x y M.
exact (KernelisKernel abgr_Zero (abgr_monic_kernel M (MonicisMonic abgr_category M))).
+ use make_EpisAreCokernels.
intros x y E.
exact (CokernelisCokernel abgr_Zero (abgr_epi_cokernel E (EpiisEpi abgr_category E))).
End abgr_abelian.
Corollaries to additive categories
In an additive category the homsets are abelian groups and pre- and postcompositions are morphisms of abelian groups. In this section we prove the following lemmas about additive categories using the theory of abelian groups developed above- A morphism φ in an additive category which gives isomorphisms (φ · _) and (_ · φ) is an isomorphism, abgr_Additive_premor_postmor_is_iso.
- A criteria of being a kernel in the category of abelian groups which uses only elements of abelian groups, abgr_isKernel_Criteria.
Lemma AdditiveZeroArrow_postmor_Abelian {Add : CategoryWithAdditiveStructure} (x y z : Add) :
to_postmor_monoidfun Add x y z (ZeroArrow (Additive.to_Zero Add) y z) =
ZeroArrow (to_Zero abgr_Abelian) (@to_abgr Add x y) (@to_abgr Add x z).
Show proof.
rewrite <- PreAdditive_unel_zero.
use monoidfun_paths. use funextfun. intros f. exact (to_premor_unel Add z f).
use monoidfun_paths. use funextfun. intros f. exact (to_premor_unel Add z f).
Lemma AdditiveZeroArrow_premor_Abelian {Add : CategoryWithAdditiveStructure} (x y z : Add) :
to_premor_monoidfun Add x y z (ZeroArrow (Additive.to_Zero Add) x y) =
ZeroArrow (to_Zero abgr_Abelian) (@to_abgr Add y z) (@to_abgr Add x z).
Show proof.
rewrite <- PreAdditive_unel_zero.
use monoidfun_paths. use funextfun. intros f. exact (to_postmor_unel Add x f).
use monoidfun_paths. use funextfun. intros f. exact (to_postmor_unel Add x f).
Local Lemma abgr_Additive_is_iso_premor_inverses {Add : CategoryWithAdditiveStructure} (x y z : Add) {f : x --> y}
(H : is_z_isomorphism f) :
is_inverse_in_precat ((to_premor_monoidfun Add x y z f) : abgr_Abelian⟦_, _⟧)
(to_premor_monoidfun Add y x z (is_z_isomorphism_mor H)).
Show proof.
use make_is_inverse_in_precat.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_premor. rewrite assoc.
rewrite (is_inverse_in_precat2 H). use id_left.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_premor. rewrite assoc.
rewrite (is_inverse_in_precat1 H). use id_left.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_premor. rewrite assoc.
rewrite (is_inverse_in_precat2 H). use id_left.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_premor. rewrite assoc.
rewrite (is_inverse_in_precat1 H). use id_left.
Lemma abgr_Additive_is_iso_premor {Add : CategoryWithAdditiveStructure} (x y z : Add) {f : x --> y}
(H : is_z_isomorphism f) :
@is_z_isomorphism abgr_Abelian _ _ (to_premor_monoidfun Add x y z f).
Show proof.
use make_is_z_isomorphism.
- exact (to_premor_monoidfun Add _ _ z (is_z_isomorphism_mor H)).
- exact (abgr_Additive_is_iso_premor_inverses _ _ z H).
- exact (to_premor_monoidfun Add _ _ z (is_z_isomorphism_mor H)).
- exact (abgr_Additive_is_iso_premor_inverses _ _ z H).
Local Lemma abgr_Additive_is_iso_postmor_inverses {Add : CategoryWithAdditiveStructure} (x y z : Add) {f : y --> z}
(H : is_z_isomorphism f) :
is_inverse_in_precat ((to_postmor_monoidfun Add x y z f) : abgr_Abelian⟦_, _⟧)
(to_postmor_monoidfun Add x z y (is_z_isomorphism_mor H)).
Show proof.
use make_is_inverse_in_precat.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_postmor. rewrite <- assoc.
rewrite (is_inverse_in_precat1 H). use id_right.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_postmor. rewrite <- assoc.
rewrite (is_inverse_in_precat2 H). use id_right.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_postmor. rewrite <- assoc.
rewrite (is_inverse_in_precat1 H). use id_right.
- use monoidfun_paths. use funextfun.
intros x0. cbn. unfold to_postmor. rewrite <- assoc.
rewrite (is_inverse_in_precat2 H). use id_right.
Lemma abgr_Additive_is_iso_postmor {Add : CategoryWithAdditiveStructure} (x y z : Add) {f : y --> z}
(H : is_z_isomorphism f) :
@is_z_isomorphism abgr_Abelian _ _ (to_postmor_monoidfun Add x y z f).
Show proof.
use make_is_z_isomorphism.
- exact (to_postmor_monoidfun Add x _ _ (is_z_isomorphism_mor H)).
- exact (abgr_Additive_is_iso_postmor_inverses x _ _ H).
- exact (to_postmor_monoidfun Add x _ _ (is_z_isomorphism_mor H)).
- exact (abgr_Additive_is_iso_postmor_inverses x _ _ H).
Local Lemma abgr_Additive_premor_postmor_is_iso_inverses {Add : CategoryWithAdditiveStructure} (x y : Add)
{f : x --> y}
(H1 : @is_z_isomorphism abgr_Abelian _ _ (to_premor_monoidfun Add x y x f))
(H2 : @is_z_isomorphism abgr_Abelian _ _ (to_postmor_monoidfun Add y x y f)) :
is_inverse_in_precat f ((is_z_isomorphism_mor H1 : monoidfun (to_abgr x x) (to_abgr y x))
(identity x : to_abgr x x)).
Show proof.
set (mor1 := ((is_z_isomorphism_mor H1) : (monoidfun (to_abgr x x) (to_abgr y x)))
((identity x) : to_abgr x x)).
set (mor2 := ((is_z_isomorphism_mor H2) : (monoidfun (to_abgr y y) (to_abgr y x)))
((identity y) : to_abgr y y)).
assert (Hx : f · mor1 = identity x).
{
exact (toforallpaths _ _ _ (base_paths _ _ (is_inverse_in_precat2 H1)) (identity x)).
}
assert (Hy : mor2 · f = identity y).
{
exact (toforallpaths _ _ _ (base_paths _ _ (is_inverse_in_precat2 H2)) (identity y)).
}
assert (H : mor1 = mor2).
{
rewrite <- (id_right mor2).
rewrite <- Hx.
rewrite assoc.
rewrite Hy.
rewrite id_left.
use idpath.
}
use make_is_inverse_in_precat.
- exact Hx.
- rewrite H. exact Hy.
((identity x) : to_abgr x x)).
set (mor2 := ((is_z_isomorphism_mor H2) : (monoidfun (to_abgr y y) (to_abgr y x)))
((identity y) : to_abgr y y)).
assert (Hx : f · mor1 = identity x).
{
exact (toforallpaths _ _ _ (base_paths _ _ (is_inverse_in_precat2 H1)) (identity x)).
}
assert (Hy : mor2 · f = identity y).
{
exact (toforallpaths _ _ _ (base_paths _ _ (is_inverse_in_precat2 H2)) (identity y)).
}
assert (H : mor1 = mor2).
{
rewrite <- (id_right mor2).
rewrite <- Hx.
rewrite assoc.
rewrite Hy.
rewrite id_left.
use idpath.
}
use make_is_inverse_in_precat.
- exact Hx.
- rewrite H. exact Hy.
Lemma abgr_Additive_premor_postmor_is_iso {Add : CategoryWithAdditiveStructure} (x y : Add) {f : x --> y}
(H1 : @is_z_isomorphism abgr_Abelian _ _ (to_premor_monoidfun Add x y x f))
(H2 : @is_z_isomorphism abgr_Abelian _ _ (to_postmor_monoidfun Add y x y f)) :
is_z_isomorphism f.
Show proof.
use make_is_z_isomorphism.
- exact (((is_z_isomorphism_mor H1) : (monoidfun (to_abgr x x) (to_abgr y x)))
((identity x) : to_abgr x x)).
- exact (abgr_Additive_premor_postmor_is_iso_inverses _ _ H1 H2).
- exact (((is_z_isomorphism_mor H1) : (monoidfun (to_abgr x x) (to_abgr y x)))
((identity x) : to_abgr x x)).
- exact (abgr_Additive_premor_postmor_is_iso_inverses _ _ H1 H2).
Local Opaque ZeroArrow.
Definition abgr_isKernel_iscontr {X Y Z W : abgr_Abelian} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = @ZeroArrow abgr_Abelian (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥)
(isM : @isMonic abgr_Abelian _ _ f) (h : W --> Y)
(H' : h · g = @ZeroArrow abgr_Abelian (to_Zero abgr_Abelian) W Z) (w' : pr1 W) :
iscontr (∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = pr1 h w').
Show proof.
cbn in H'. rewrite <- (@PreAdditive_unel_zero (abgr_PreAdditive)) in H'.
unfold to_unel in H'.
set (e := toforallpaths _ _ _ (base_paths _ _ H') w').
set (H'' := H (tpair _ (pr1 h w') e)).
use (squash_to_prop H'' (isapropiscontr _)). intros HH.
induction HH as [H1 H2]. cbn in H2.
use tpair.
- use tpair.
+ exact H1.
+ exact H2.
- cbn. intros T. induction T as [T1 T2].
use total2_paths_f.
+ use (abgr_monic_paths f isM T1 H1). cbn in H2. cbn.
rewrite H2. rewrite T2. use idpath.
+ use proofirrelevance. use setproperty.
unfold to_unel in H'.
set (e := toforallpaths _ _ _ (base_paths _ _ H') w').
set (H'' := H (tpair _ (pr1 h w') e)).
use (squash_to_prop H'' (isapropiscontr _)). intros HH.
induction HH as [H1 H2]. cbn in H2.
use tpair.
- use tpair.
+ exact H1.
+ exact H2.
- cbn. intros T. induction T as [T1 T2].
use total2_paths_f.
+ use (abgr_monic_paths f isM T1 H1). cbn in H2. cbn.
rewrite H2. rewrite T2. use idpath.
+ use proofirrelevance. use setproperty.
Lemma abgr_isKernel_Criteria_ismonoidfun {X Y Z W : abgr_category} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D)∥)
(isM : @isMonic abgr_category _ _ f) (h : abgr_Abelian ⟦W, Y⟧)
(H' : h · g = ZeroArrow (to_Zero abgr_Abelian) W Z) :
ismonoidfun (λ w' : (W : abgr), pr1 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' w'))).
Show proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x y. use (abgr_monic_paths f isM).
use (pathscomp0 _ (! binopfunisbinopfun (f : monoidfun _ _) _ _)).
use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr
f g ZA H isM h H' ((x * y)%multmonoid))))).
use (pathscomp0 (binopfunisbinopfun (h : monoidfun _ _) _ _)).
use pathsinv0.
use two_arg_paths.
+ exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
+ exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (y%multmonoid)))).
- use (abgr_monic_paths f isM).
use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr
f g ZA H isM h H' (unel (W : abgr)))))).
use (pathscomp0 (monoidfununel h)). exact (! monoidfununel f).
- use make_isbinopfun. intros x y. use (abgr_monic_paths f isM).
use (pathscomp0 _ (! binopfunisbinopfun (f : monoidfun _ _) _ _)).
use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr
f g ZA H isM h H' ((x * y)%multmonoid))))).
use (pathscomp0 (binopfunisbinopfun (h : monoidfun _ _) _ _)).
use pathsinv0.
use two_arg_paths.
+ exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
+ exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (y%multmonoid)))).
- use (abgr_monic_paths f isM).
use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr
f g ZA H isM h H' (unel (W : abgr)))))).
use (pathscomp0 (monoidfununel h)). exact (! monoidfununel f).
Lemma abgr_isKernel_Criteria_comm {X Y Z W : abgr_category} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥)
(isM : @isMonic abgr_category _ _ f) (h : abgr_Abelian ⟦W, Y⟧)
(H' : h · g = ZeroArrow (to_Zero abgr_Abelian) W Z) :
monoidfuncomp (monoidfunconstr (abgr_isKernel_Criteria_ismonoidfun f g ZA H isM h H')) f = h.
Show proof.
use monoidfun_paths. use funextfun. intros x.
exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
Definition make_abgr_isKernel_Criteria {X Y Z W : abgr_category} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥)
(isM : @isMonic abgr_category _ _ f) (h : abgr_Abelian ⟦W, Y⟧)
(H' : h · g = ZeroArrow (to_Zero abgr_Abelian) W Z) :
∑ ψ : abgr_Abelian ⟦W, X⟧, ψ · f = h.
Show proof.
use tpair.
- use monoidfunconstr.
+ intros w'. exact (pr1 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' w'))).
+ exact (abgr_isKernel_Criteria_ismonoidfun f g ZA H isM h H').
- exact (abgr_isKernel_Criteria_comm f g ZA H isM h H').
- use monoidfunconstr.
+ intros w'. exact (pr1 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' w'))).
+ exact (abgr_isKernel_Criteria_ismonoidfun f g ZA H isM h H').
- exact (abgr_isKernel_Criteria_comm f g ZA H isM h H').
Lemma abgr_isKernel_Criteria_uniqueness {X Y Z W : abgr_category} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥)
(isM : @isMonic abgr_category _ _ f) (h : abgr_Abelian ⟦W, Y⟧)
(H' : h · g = ZeroArrow (to_Zero abgr_Abelian) W Z)
(t : ∑ ψ : abgr_Abelian ⟦W, X⟧, ψ · f = h) :
t = make_abgr_isKernel_Criteria f g ZA H isM h H'.
Show proof.
use total2_paths_f.
- use monoidfun_paths. use funextfun. intros x.
use (abgr_monic_paths f isM).
use (pathscomp0 (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x)). use pathsinv0.
exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
- use proofirrelevance. use setproperty.
- use monoidfun_paths. use funextfun. intros x.
use (abgr_monic_paths f isM).
use (pathscomp0 (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x)). use pathsinv0.
exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))).
- use proofirrelevance. use setproperty.
Definition abgr_isKernel_Criteria {X Y Z : abgr_category} (f : X --> Y) (g : Y --> Z)
(ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _)
(H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)),
∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥)
(isM : @isMonic abgr_category _ _ f) : isKernel (to_Zero abgr_Abelian) f g ZA.
Show proof.
use make_isKernel.
- intros w h H'. use make_iscontr.
+ exact (make_abgr_isKernel_Criteria f g ZA H isM h H').
+ intros t. exact (abgr_isKernel_Criteria_uniqueness f g ZA H isM h H' t).
- intros w h H'. use make_iscontr.
+ exact (make_abgr_isKernel_Criteria f g ZA H isM h H').
+ intros t. exact (abgr_isKernel_Criteria_uniqueness f g ZA H isM h H' t).
End abgr_corollaries.