From bd74baa1952b1851d8d036ff6767b83872534e6b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 11 Sep 2020 14:46:48 +0000 Subject: [PATCH] feat(algebra/homology/exact): lemmas about exactness (#4106) These are a few lemmas on the way to showing how `exact` changes under isomorphisms applied to the objects. It's not everthing one might want; I'm salvaging this from an old branch and unlikely to do more in the near future, but hopefully this is mergeable progress as is. Co-authored-by: Scott Morrison --- src/algebra/homology/exact.lean | 34 +++++++++++++++++++ src/algebra/homology/image_to_kernel_map.lean | 14 ++++++++ src/category_theory/limits/shapes/images.lean | 20 +++++++++++ .../limits/shapes/kernels.lean | 33 +++++++++++------- 4 files changed, 88 insertions(+), 13 deletions(-) diff --git a/src/algebra/homology/exact.lean b/src/algebra/homology/exact.lean index afe608390ef10..0690e82632060 100644 --- a/src/algebra/homology/exact.lean +++ b/src/algebra/homology/exact.lean @@ -11,6 +11,11 @@ import algebra.homology.image_to_kernel_map In a category with zero morphisms, images, and equalizers we say that `f : A ⟶ B` and `g : B ⟶ C` are exact if `f ≫ g = 0` and the natural map `image f ⟶ kernel g` is an epimorphism. +(We say epimorphism rather than isomorphism because, at least for preadditive categories, +this is exactly equivalent to the homology at `i` vanishing. +In an abelian category, this is the same as asking for it to be an isomorphism, +because the inclusion map is always a monomorphism.) + # Main results * Suppose that cokernels exist and that `f` and `g` are exact. If `s` is any kernel fork over `g` and `t` is any cokernel cofork over `f`, then `fork.ι s ≫ cofork.π t = 0`. @@ -43,6 +48,20 @@ class exact {A B C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop := attribute [instance] exact.epi +lemma exact.w_assoc {A B C D : V} {f : A ⟶ B} {g : B ⟶ C} [exact f g] {h : C ⟶ D} : + f ≫ g ≫ h = 0 := +by rw [←category.assoc, @exact.w _ _ _ _ _ _ _ _ _ f g, has_zero_morphisms.zero_comp] + +instance exact_comp_iso {A B C C' : V} (f : A ⟶ B) (g : B ⟶ C) (h : C ≅ C') [exact f g] : + exact f (g ≫ h.hom) := +{ w := exact.w_assoc, + epi := by { simp only [image_to_kernel_map_comp_iso], apply epi_comp, } } + +instance exact_iso_comp {A A' B C : V} (h : A' ≅ A) (f : A ⟶ B) (g : B ⟶ C) [exact f g] : + exact (h.hom ≫ f) g := +{ w := by rw [category.assoc, @exact.w _ _ _ _ _ _ _ _ _ f g, has_zero_morphisms.comp_zero], + epi := by { simp only [image_to_kernel_map_iso_comp], apply epi_comp, } } + section variables [has_cokernels V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) @@ -60,4 +79,19 @@ by rw [←kernel.lift_ι _ _ hι, ←cokernel.π_desc _ _ hπ, category.assoc, k comp_eq_zero_of_exact f g (kernel_fork.condition s) (cokernel_cofork.condition t) end + +section +local attribute [instance] has_zero_object.has_zero + +lemma exact_of_zero [has_zero_object V] {A C : V} (f : A ⟶ 0) (g : 0 ⟶ C) : exact f g := +begin + obtain rfl : f = 0 := by ext, + obtain rfl : g = 0 := by ext, + fsplit, + { simp, }, + { exact image_to_kernel_map_epi_of_zero_of_mono 0, }, +end + +end + end category_theory diff --git a/src/algebra/homology/image_to_kernel_map.lean b/src/algebra/homology/image_to_kernel_map.lean index eb7e41007fd7b..ab626118717cb 100644 --- a/src/algebra/homology/image_to_kernel_map.lean +++ b/src/algebra/homology/image_to_kernel_map.lean @@ -53,6 +53,20 @@ lemma image_to_kernel_map_zero_right {w} : image_to_kernel_map f (0 : B ⟶ C) w = image.ι f ≫ inv (kernel.ι (0 : B ⟶ C)) := by { ext, simp } +@[simp] +lemma image_to_kernel_map_comp_iso {D : V} (h : C ⟶ D) [is_iso h] (w) : + image_to_kernel_map f (g ≫ h) w = + image_to_kernel_map f g ((cancel_mono h).mp (by simpa using w : (f ≫ g) ≫ h = 0 ≫ h)) ≫ + (kernel_comp_is_iso g h).inv := +by { ext, simp, } + +@[simp] +lemma image_to_kernel_map_iso_comp {Z : V} (h : Z ⟶ A) [is_iso h] (w) : + image_to_kernel_map (h ≫ f) g w = + image.pre_comp h f ≫ + image_to_kernel_map f g ((cancel_epi h).mp (by simpa using w : h ≫ f ≫ g = h ≫ 0)) := +by { ext, simp, } + local attribute [instance] has_zero_object.has_zero /-- diff --git a/src/category_theory/limits/shapes/images.lean b/src/category_theory/limits/shapes/images.lean index ef61f57f9c364..753eb6e029376 100644 --- a/src/category_theory/limits/shapes/images.lean +++ b/src/category_theory/limits/shapes/images.lean @@ -317,6 +317,11 @@ image.lift m := image.ι g, e := f ≫ factor_thru_image g } +@[simp, reassoc] +lemma image.factor_thru_image_pre_comp [has_image g] [has_image (f ≫ g)] : + factor_thru_image (f ≫ g) ≫ image.pre_comp f g = f ≫ factor_thru_image g := +by simp [image.pre_comp] + /-- The two step comparison map `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h` @@ -333,6 +338,21 @@ begin simp [image.pre_comp, image.eq_to_hom], end +variables [has_equalizers C] + +/-- +`image.pre_comp f g` is an isomorphism when `f` is an isomorphism +(we need `C` to have equalizers to prove this). +-/ +instance image.is_iso_precomp_iso (f : X ≅ Y) [has_image g] [has_image (f.hom ≫ g)] : + is_iso (image.pre_comp f.hom g) := +{ inv := image.lift + { I := image (f.hom ≫ g), + m := image.ι (f.hom ≫ g), + e := f.inv ≫ factor_thru_image (f.hom ≫ g) }, + hom_inv_id' := by { ext, simp [image.pre_comp], }, + inv_hom_id' := by { ext, simp [image.pre_comp], }, } + -- Note that in general we don't have the other comparison map you might expect -- `image f ⟶ image (f ≫ g)`. diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean index e42686a2f3920..e2158a48ddc95 100644 --- a/src/category_theory/limits/shapes/kernels.lean +++ b/src/category_theory/limits/shapes/kernels.lean @@ -143,6 +143,8 @@ abbreviation kernel : C := equalizer f 0 /-- The map from `kernel f` into the source of `f`. -/ abbreviation kernel.ι : kernel f ⟶ X := equalizer.ι f 0 +@[simp] lemma equalizer_as_kernel : equalizer.ι f 0 = kernel.ι f := rfl + @[simp, reassoc] lemma kernel.condition : kernel.ι f ≫ f = 0 := kernel_fork.condition _ @@ -216,42 +218,44 @@ lemma kernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (kernel.ι f)) → false /-- When `g` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`. -/ -@[simps] def kernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] : kernel (f ≫ g) ≅ kernel f := { hom := kernel.lift _ (kernel.ι _) (by { rw [←cancel_mono g], simp, }), inv := kernel.lift _ (kernel.ι _) (by simp), } +@[simp] lemma kernel_comp_is_iso_hom_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] : (kernel_comp_is_iso f g).hom ≫ kernel.ι f = kernel.ι (f ≫ g) := -by simp +by simp [kernel_comp_is_iso] +@[simp] lemma kernel_comp_is_iso_inv_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] : (kernel_comp_is_iso f g).inv ≫ kernel.ι (f ≫ g) = kernel.ι f := -by simp +by simp [kernel_comp_is_iso] /-- When `f` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `g`. -/ -@[simps] def kernel_is_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] : kernel (f ≫ g) ≅ kernel g := { hom := kernel.lift _ (kernel.ι _ ≫ f) (by simp), inv := kernel.lift _ (kernel.ι _ ≫ inv f) (by simp), } +@[simp] lemma kernel_is_iso_comp_hom_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] : (kernel_is_iso_comp f g).hom ≫ kernel.ι g = kernel.ι (f ≫ g) ≫ f := -by simp +by simp [kernel_is_iso_comp] +@[simp] lemma kernel_is_iso_comp_inv_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] : (kernel_is_iso_comp f g).inv ≫ kernel.ι (f ≫ g) = kernel.ι g ≫ (inv f) := -by simp +by simp [kernel_is_iso_comp] end @@ -396,6 +400,8 @@ abbreviation cokernel : C := coequalizer f 0 /-- The map from the target of `f` to `cokernel f`. -/ abbreviation cokernel.π : Y ⟶ cokernel f := coequalizer.π f 0 +@[simp] lemma coequalizer_as_cokernel : coequalizer.π f 0 = cokernel.π f := rfl + @[simp, reassoc] lemma cokernel.condition : f ≫ cokernel.π f = 0 := cokernel_cofork.condition _ @@ -471,43 +477,44 @@ lemma cokernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (cokernel.π f)) → f /-- When `g` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `f`. -/ -@[simps] def cokernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] : cokernel (f ≫ g) ≅ cokernel f := { hom := cokernel.desc _ (inv g ≫ cokernel.π f) (by simp), inv := cokernel.desc _ (g ≫ cokernel.π (f ≫ g)) (by rw [←category.assoc, cokernel.condition]), } +@[simp] lemma cokernel_π_comp_cokernel_comp_is_iso_hom {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] : cokernel.π (f ≫ g) ≫ (cokernel_comp_is_iso f g).hom = inv g ≫ cokernel.π f := -by simp +by simp [cokernel_comp_is_iso] +@[simp] lemma cokernel_π_comp_cokernel_comp_is_iso_inv {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] : cokernel.π f ≫ (cokernel_comp_is_iso f g).inv = g ≫ cokernel.π (f ≫ g) := -by simp +by simp [cokernel_comp_is_iso] /-- When `f` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`. -/ -@[simps] def cokernel_is_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] : cokernel (f ≫ g) ≅ cokernel g := { hom := cokernel.desc _ (cokernel.π g) (by simp), inv := cokernel.desc _ (cokernel.π (f ≫ g)) (by { rw [←cancel_epi f, ←category.assoc], simp, }), } - +@[simp] lemma cokernel_π_comp_cokernel_is_iso_comp_hom {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] : cokernel.π (f ≫ g) ≫ (cokernel_is_iso_comp f g).hom = cokernel.π g := -by simp +by simp [cokernel_is_iso_comp] +@[simp] lemma cokernel_π_comp_cokernel_is_iso_comp_inv {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] : cokernel.π g ≫ (cokernel_is_iso_comp f g).inv = cokernel.π (f ≫ g) := -by simp +by simp [cokernel_is_iso_comp] end