Definition ComplexPreCatAbelianMonicKernelsData_isKernel {x y : Complex (AbelianToAdditive A)} (M : Monic (ComplexCat (AbelianToAdditive A)) x y) (Z := Additive.
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. 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.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. 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.AbelianToAdditive. Local Lemma MorphismFromZero_comm (C : Complex) (i : hz) : Definition MorphismFromZero (C : Complex) : Morphism ZeroComplex C. - intros i. exact (MorphismFromZero_comm C i). ZeroMorphism C1 C2 = MorphismComp (MorphismToZero C1) (MorphismFromZero C2). Arguments MorphismFromZero [A] _. Definition ComplexFromObject_obs (X : ob A) (i : hz) : hz -> A. Definition ComplexFromObject_mors (X : ob A) (i : hz) : ∏ i0 : hz, A ⟦ComplexFromObject_obs X i i0, ComplexFromObject_obs X i (i0 + 1)⟧. exact (ZeroArrow (Additive.to_Zero A) (ComplexFromObject_obs X i i0) (ComplexFromObject_obs X i (i0 + 1))). Local Lemma ComplexFromObject_comm (X : ob A) (i : hz) : ∏ i0 : hz, (ComplexFromObject_mors X i i0) · (ComplexFromObject_mors X i (i0 + 1)) = Definition ComplexFromObject (X : ob A) (i : hz) : Complex A. - exact (ComplexFromObject_obs X i). - exact (ComplexFromObject_mors X i). - exact (ComplexFromObject_comm X i). ∏ i0 : hz, A ⟦(ComplexFromObject a i) i0, (ComplexFromObject b i) i0⟧. unfold ComplexFromObject. cbn. unfold ComplexFromObject_obs. cbn. unfold coprod_rect. ∏ i0 : hz, (ObjectMorToComplexMor_mors f i i0) · (Diff (ComplexFromObject b i) i0) = (Diff (ComplexFromObject a i) i0) · (ObjectMorToComplexMor_mors f i (i0 + 1)). unfold ComplexFromObject. unfold ComplexFromObject_mors. unfold ComplexFromObject_obs. cbn. Morphism (ComplexFromObject a i) (ComplexFromObject b i). Definition AcyclicComplexFromObject_obs (a : ob A) (i : hz) : hz -> ob A. Definition AcyclicComplexFromObject_mors (a : ob A) (i : hz) : ∏ i0 : hz, A ⟦AcyclicComplexFromObject_obs a i i0, AcyclicComplexFromObject_obs a i (i0 + 1)⟧. intros i0. unfold AcyclicComplexFromObject_obs. cbn. unfold coprod_rect. Local Lemma AcyclicComplexFromObject_diff (a : ob A) (i : hz) : ∏ i0 : hz, (AcyclicComplexFromObject_mors a i i0) · (AcyclicComplexFromObject_mors a i (i0 + 1)) = intros i0. unfold AcyclicComplexFromObject_obs. unfold AcyclicComplexFromObject_mors. Definition AcyclicComplexFromObject (a : ob A) (i : hz) : Complex A. - exact (AcyclicComplexFromObject_obs a i). - exact (AcyclicComplexFromObject_mors a i). - exact (AcyclicComplexFromObject_diff a i). Definition FromAcyclicComplexFromObject_mors {a : ob A} {C : Complex A} {i : hz} (f : a --> (C i)) : ∏ i0 : hz, A ⟦(AcyclicComplexFromObject a i) i0, C i0⟧. unfold AcyclicComplexFromObject. unfold AcyclicComplexFromObject_obs. unfold AcyclicComplexFromObject_mors. cbn. Local Lemma FromAcyclicComplexFromObject_comm_eq1 {a : ob A} {C : Complex A} {i : hz} Local Lemma FromAcyclicComplexFromObject_comm_eq2 {a : ob A} {C : Complex A} {i : hz} Local Lemma FromAcyclicComplexFromObject_comm {a : ob A} {C : Complex A} {i : hz} ∏ i0 : hz, (FromAcyclicComplexFromObject_mors f i0) · (Diff C i0) = (Diff (AcyclicComplexFromObject a i) i0) · (FromAcyclicComplexFromObject_mors f (i0 + 1)). unfold AcyclicComplexFromObject. unfold AcyclicComplexFromObject_obs. unfold AcyclicComplexFromObject_mors. unfold FromAcyclicComplexFromObject_mors. -- exact (FromAcyclicComplexFromObject_comm_eq1 f i0 e e''). ++ exact (FromAcyclicComplexFromObject_comm_eq2 f i0 e'). Definition FromAcyclicComplexFromObject {a : ob A} {C : Complex A} {i : hz} (f : a --> (C i)) : Morphism (AcyclicComplexFromObject a i) C. - exact (FromAcyclicComplexFromObject_mors f). - exact (FromAcyclicComplexFromObject_comm f). Definition ToAcyclicComplexFromObject_mors {a : ob A} {C : Complex A} {i : hz} (f : (C i) --> a) : ∏ i0 : hz, A ⟦C i0, (AcyclicComplexFromObject a (i - 1)) i0⟧. unfold AcyclicComplexFromObject. unfold AcyclicComplexFromObject_obs. unfold AcyclicComplexFromObject_mors. cbn. Local Lemma ToAcyclicComplexFromObject_mors_comm_eq1 {a : ob A} {C : Complex A} {i : hz} Local Lemma ToAcyclicComplexFromObject_mors_comm_eq2 {a : ob A} {C : Complex A} {i : hz} Local Lemma ToAcyclicComplexFromObject_mors_comm {a : ob A} {C : Complex A} {i : hz} ∏ i0 : hz, (ToAcyclicComplexFromObject_mors f i0) · (Diff (AcyclicComplexFromObject a (i - 1)) i0) = (Diff C i0) · (ToAcyclicComplexFromObject_mors f (i0 + 1)). unfold AcyclicComplexFromObject. unfold AcyclicComplexFromObject_obs. unfold AcyclicComplexFromObject_mors. cbn. unfold ToAcyclicComplexFromObject_mors. unfold coprod_rect. cbn. * exact (ToAcyclicComplexFromObject_mors_comm_eq1 f i0 e e''). -- exact (ToAcyclicComplexFromObject_mors_comm_eq2 f i0 e'). -- exact (ToAcyclicComplexFromObject_mors_comm_eq2 f i0 e'). Definition ToAcyclicComplexFromObject {a : ob A} {C : Complex A} {i : hz} (f : (C i) --> a) : Morphism C (AcyclicComplexFromObject a (i - 1)). - exact (ToAcyclicComplexFromObject_mors f). - exact (ToAcyclicComplexFromObject_mors_comm f). Lemma FromAcyclicComplexFromObject_Eq {a : ob A} {C : Complex A} (i0 : hz) {i : hz} FromAcyclicComplexFromObject f i0 = FromAcyclicComplexFromObject_mors f i0. Lemma ToAcyclicComplexFromObject_Eq {a : ob A} {C : Complex A} (i0 : hz) {i : hz} ToAcyclicComplexFromObject f i0 = ToAcyclicComplexFromObject_mors f i0. FromAcyclicComplexFromObject_mors A g i = FromAcyclicComplexFromObject_mors A h i. use (pathscomp0 (! (FromAcyclicComplexFromObject_Eq A i g))). use (pathscomp0 _ (FromAcyclicComplexFromObject_Eq A i h)). unfold FromAcyclicComplexFromObject_mors. unfold coprod_rect. unfold AcyclicComplexFromObject_obs. cbn. unfold FromAcyclicComplexFromObject_mors in tmp. cbn in tmp. unfold coprod_rect in tmp. unfold AcyclicComplexFromObject_obs in tmp. ToAcyclicComplexFromObject_mors A g i = ToAcyclicComplexFromObject_mors A h i. use (pathscomp0 (! (ToAcyclicComplexFromObject_Eq A i g))). use (pathscomp0 _ (ToAcyclicComplexFromObject_Eq A i h)). unfold ToAcyclicComplexFromObject_mors. unfold coprod_rect. unfold AcyclicComplexFromObject_obs. cbn. unfold ToAcyclicComplexFromObject_mors in tmp. cbn in tmp. unfold coprod_rect in tmp. unfold AcyclicComplexFromObject_obs in tmp. cbn in tmp. + exact (MorphismFromZero C). apply ArrowsFromZero. MorphismComp (ZeroArrowTo (ComplexPreCat_Kernel g)) (@ZeroArrowFrom _ Z Y). MorphismComp (@ZeroArrowTo _ Z0 Y) (@ZeroArrowFrom _ Z0 (ComplexPreCat_Cokernel g)).