From e1c649d5b9a722243796ab4286a427808e5d59ce Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 12 Jul 2021 07:00:28 +0000 Subject: [PATCH] feat(category_theory/abelian): the five lemma (#8265) --- src/algebra/homology/exact.lean | 6 + src/category_theory/abelian/basic.lean | 60 ++++++++- .../abelian/diagram_lemmas/four.lean | 124 +++++++++++++++--- src/category_theory/abelian/exact.lean | 23 ++++ .../limits/shapes/pullbacks.lean | 41 +++++- src/category_theory/limits/shapes/zero.lean | 4 + src/category_theory/subobject/limits.lean | 5 + 7 files changed, 243 insertions(+), 20 deletions(-) diff --git a/src/algebra/homology/exact.lean b/src/algebra/homology/exact.lean index 6f1b0154b59ec..086f111614d16 100644 --- a/src/algebra/homology/exact.lean +++ b/src/algebra/homology/exact.lean @@ -184,6 +184,12 @@ begin apply epi_comp, end +instance [exact f g] : epi (kernel.lift g f (by simp)) := +begin + rw ←factor_thru_kernel_subobject_comp_kernel_subobject_iso, + apply epi_comp +end + variables (A) lemma kernel_subobject_arrow_eq_zero_of_exact_zero_left [exact (0 : A ⟶ B) g] : diff --git a/src/category_theory/abelian/basic.lean b/src/category_theory/abelian/basic.lean index c8e7f0f589755..faa86294b7f38 100644 --- a/src/category_theory/abelian/basic.lean +++ b/src/category_theory/abelian/basic.lean @@ -246,6 +246,14 @@ cokernel.π_desc _ _ _ instance : mono (coimages.factor_thru_coimage f) := show mono (non_preadditive_abelian.factor_thru_coimage f), by apply_instance +section +variables {f} + +lemma comp_coimage_π_eq_zero {R : C} {g : Q ⟶ R} (h : f ≫ g = 0) : f ≫ coimages.coimage.π g = 0 := +zero_of_comp_mono (coimages.factor_thru_coimage g) $ by simp [h] + +end + instance epi_factor_thru_coimage [epi f] : epi (coimages.factor_thru_coimage f) := epi_of_epi_fac $ coimage.fac f @@ -386,7 +394,7 @@ fork.is_limit.mk _ end pullback_to_biproduct_is_kernel namespace biproduct_to_pushout_is_cokernel -variables [limits.has_pushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) +variables [limits.has_pushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) /-- The canonical map `Y ⊞ Z ⟶ pushout f g` -/ abbreviation biproduct_to_pushout : Y ⊞ Z ⟶ pushout f g := @@ -411,7 +419,7 @@ cofork.is_colimit.mk _ end biproduct_to_pushout_is_cokernel section epi_pullback -variables [limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) +variables [limits.has_pullbacks C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) /-- In an abelian category, the pullback of an epimorphism is an epimorphism. Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6] -/ @@ -482,10 +490,32 @@ begin ... = 0 : has_zero_morphisms.comp_zero _ _ end +lemma epi_snd_of_is_limit [epi f] {s : pullback_cone f g} (hs : is_limit s) : epi s.snd := +begin + convert epi_of_epi_fac (is_limit.cone_point_unique_up_to_iso_hom_comp (limit.is_limit _) hs _), + { refl }, + { exact abelian.epi_pullback_of_epi_f _ _ } +end + +lemma epi_fst_of_is_limit [epi g] {s : pullback_cone f g} (hs : is_limit s) : epi s.fst := +begin + convert epi_of_epi_fac (is_limit.cone_point_unique_up_to_iso_hom_comp (limit.is_limit _) hs _), + { refl }, + { exact abelian.epi_pullback_of_epi_g _ _ } +end + +/-- Suppose `f` and `g` are two morphisms with a common codomain and suppose we have written `g` as + an epimorphism followed by a monomorphism. If `f` factors through the mono part of this + factorization, then any pullback of `g` along `f` is an epimorphism. -/ +lemma epi_fst_of_factor_thru_epi_mono_factorization + (g₁ : Y ⟶ W) [epi g₁] (g₂ : W ⟶ Z) [mono g₂] (hg : g₁ ≫ g₂ = g) (f' : X ⟶ W) (hf : f' ≫ g₂ = f) + (t : pullback_cone f g) (ht : is_limit t) : epi t.fst := +by apply epi_fst_of_is_limit _ _ (pullback_cone.is_limit_of_factors f g g₂ f' g₁ hf hg t ht) + end epi_pullback section mono_pushout -variables [limits.has_pushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) +variables [limits.has_pushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) instance mono_pushout_of_mono_f [mono f] : mono (pushout.inr : Z ⟶ pushout f g) := mono_of_cancel_zero _ $ λ R e h, @@ -533,6 +563,30 @@ begin ... = 0 : zero_comp end +lemma mono_inr_of_is_colimit [mono f] {s : pushout_cocone f g} (hs : is_colimit s) : mono s.inr := +begin + convert mono_of_mono_fac + (is_colimit.comp_cocone_point_unique_up_to_iso_hom hs (colimit.is_colimit _) _), + { refl }, + { exact abelian.mono_pushout_of_mono_f _ _ } +end + +lemma mono_inl_of_is_colimit [mono g] {s : pushout_cocone f g} (hs : is_colimit s) : mono s.inl := +begin + convert mono_of_mono_fac + (is_colimit.comp_cocone_point_unique_up_to_iso_hom hs (colimit.is_colimit _) _), + { refl }, + { exact abelian.mono_pushout_of_mono_g _ _ } +end + +/-- Suppose `f` and `g` are two morphisms with a common domain and suppose we have written `g` as + an epimorphism followed by a monomorphism. If `f` factors through the epi part of this + factorization, then any pushout of `g` along `f` is a monomorphism. -/ +lemma mono_inl_of_factor_thru_epi_mono_factorization (f : X ⟶ Y) (g : X ⟶ Z) + (g₁ : X ⟶ W) [epi g₁] (g₂ : W ⟶ Z) [mono g₂] (hg : g₁ ≫ g₂ = g) (f' : W ⟶ Y) (hf : g₁ ≫ f' = f) + (t : pushout_cocone f g) (ht : is_colimit t) : mono t.inl := +by apply mono_inl_of_is_colimit _ _ (pushout_cocone.is_colimit_of_factors _ _ _ _ _ hf hg t ht) + end mono_pushout end category_theory.abelian diff --git a/src/category_theory/abelian/diagram_lemmas/four.lean b/src/category_theory/abelian/diagram_lemmas/four.lean index f0a67fd346d22..0bea6dcb0d2a4 100644 --- a/src/category_theory/abelian/diagram_lemmas/four.lean +++ b/src/category_theory/abelian/diagram_lemmas/four.lean @@ -6,32 +6,49 @@ Authors: Markus Himmel import category_theory.abelian.pseudoelements /-! -# The four lemma +# The four and five lemmas Consider the following commutative diagram with exact rows in an abelian category: ``` -A ---f--> B ---g--> C ---h--> D -| | | | -α β γ δ -| | | | -v v v v -A' --f'-> B' --g'-> C' --h'-> D' +A ---f--> B ---g--> C ---h--> D ---i--> E +| | | | | +α β γ δ ε +| | | | | +v v v v v +A' --f'-> B' --g'-> C' --h'-> D' --i'-> E' ``` -We prove the "mono" version of the four lemma: if α is an epimorphism and β and δ are monomorphisms, -then γ is a monomorphism. - -## Future work - -The "epi" four lemma and the five lemma, which is then an easy corollary. +We show: +- the "mono" version of the four lemma: if `α` is an epimorphism and `β` and `δ` are monomorphisms, + then `γ` is a monomorphism, +- the "epi" version of the four lemma: if `β` and `δ` are epimorphisms and `ε` is a monomorphism, + then `γ` is an epimorphism, +- the five lemma: if `α`, `β`, `δ` and `ε` are isomorphisms, then `γ` is an isomorphism. + +## Implementation details + +To show the mono version, we use pseudoelements. For the epi version, we use a completely different +arrow-theoretic proof. In theory, it should be sufficient to have one version and the other should +follow automatically by duality. In practice, mathlib's knowledge about duality isn't quite at the +point where this is doable easily. + +However, one key duality statement about exactness is needed in the proof of the epi version of the +four lemma: we need to know that exactness of a pair `(f, g)`, which we defined via the map from +the image of `f` to the kernel of `g`, is the same as "co-exactness", defined via the map from the +cokernel of `f` to the coimage of `g` (more precisely, we only need the consequence that if `(f, g)` +is exact, then the factorization of `g` through the cokernel of `f` is monomorphic). Luckily, in the +case of abelian categories, we have the characterization that `(f, g)` is exact if and only if +`f ≫ g = 0` and `kernel.ι g ≫ cokernel.π f = 0`, and the latter condition is self dual, so the +equivalence of exactness and co-exactness follows easily. ## Tags -four lemma, diagram lemma, diagram chase +four lemma, five lemma, diagram lemma, diagram chase -/ open category_theory (hiding comp_apply) open category_theory.abelian.pseudoelement +open category_theory.limits universes v u @@ -46,11 +63,14 @@ variables {A B C D A' B' C' D' : V} variables {f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} variables {f' : A' ⟶ B'} {g' : B' ⟶ C'} {h' : C' ⟶ D'} variables {α : A ⟶ A'} {β : B ⟶ B'} {γ : C ⟶ C'} {δ : D ⟶ D'} -variables [exact f g] [exact g h] [exact f' g'] variables (comm₁ : α ≫ f' = f ≫ β) (comm₂ : β ≫ g' = g ≫ γ) (comm₃ : γ ≫ h' = h ≫ δ) include comm₁ comm₂ comm₃ -/-- The four lemma, mono version. For names of objects and morphisms, consider the following +section +variables [exact f g] [exact g h] [exact f' g'] + + +/-- The four lemma, mono version. For names of objects and morphisms, refer to the following diagram: ``` @@ -85,4 +105,76 @@ mono_of_zero_of_map_zero _ $ λ c hc, ... = g (f a) : by rw this ... = 0 : pseudo_exact_of_exact.1 _ +end + +section +variables [exact g h] [exact f' g'] [exact g' h'] + +/-- The four lemma, epi version. For names of objects and morphisms, refer to the following + diagram: + +``` +A ---f--> B ---g--> C ---h--> D +| | | | +α β γ δ +| | | | +v v v v +A' --f'-> B' --g'-> C' --h'-> D' +``` +-/ +lemma epi_of_epi_of_epi_of_mono (hα : epi α) (hγ : epi γ) (hδ : mono δ) : epi β := +preadditive.epi_of_cancel_zero _ $ λ R r hβr, + have hf'r : f' ≫ r = 0, from limits.zero_of_epi_comp α $ + calc α ≫ f' ≫ r = f ≫ β ≫ r : by rw reassoc_of comm₁ + ... = f ≫ 0 : by rw hβr + ... = 0 : has_zero_morphisms.comp_zero _ _, + let y : R ⟶ pushout r g' := pushout.inl, z : C' ⟶ pushout r g' := pushout.inr in + have mono y, from mono_inl_of_factor_thru_epi_mono_factorization r g' (cokernel.π f') + (cokernel.desc f' g' (by simp)) (by simp) (cokernel.desc f' r hf'r) (by simp) _ + (colimit.is_colimit _), + have hz : g ≫ γ ≫ z = 0, from + calc g ≫ γ ≫ z = β ≫ g' ≫ z : by rw ←reassoc_of comm₂ + ... = β ≫ r ≫ y : by rw ←pushout.condition + ... = 0 ≫ y : by rw reassoc_of hβr + ... = 0 : has_zero_morphisms.zero_comp _ _, + let v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl, + w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr in + have mono v, from mono_inl_of_factor_thru_epi_mono_factorization _ _ (cokernel.π g) + (cokernel.desc g h (by simp) ≫ δ) (by simp) (cokernel.desc _ _ hz) (by simp) _ + (colimit.is_colimit _), + have hzv : z ≫ v = h' ≫ w, from (cancel_epi γ).1 $ + calc γ ≫ z ≫ v = h ≫ δ ≫ w : by rw [←category.assoc, pushout.condition, category.assoc] + ... = γ ≫ h' ≫ w : by rw reassoc_of comm₃, + suffices (r ≫ y) ≫ v = 0, by exactI zero_of_comp_mono _ (zero_of_comp_mono _ this), + calc (r ≫ y) ≫ v = g' ≫ z ≫ v : by rw [pushout.condition, category.assoc] + ... = g' ≫ h' ≫ w : by rw hzv + ... = 0 ≫ w : exact.w_assoc _ + ... = 0 : has_zero_morphisms.zero_comp _ _ + +end + +section five +variables {E E' : V} {i : D ⟶ E} {i' : D' ⟶ E'} {ε : E ⟶ E'} (comm₄ : δ ≫ i' = i ≫ ε) +variables [exact f g] [exact g h] [exact h i] [exact f' g'] [exact g' h'] [exact h' i'] +variables [is_iso α] [is_iso β] [is_iso δ] [is_iso ε] +include comm₄ + + +/-- The five lemma. For names of objects and morphisms, refer to the following diagram: + +``` +A ---f--> B ---g--> C ---h--> D ---i--> E +| | | | | +α β γ δ ε +| | | | | +v v v v v +A' --f'-> B' --g'-> C' --h'-> D' --i'-> E' +``` +-/ +lemma is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso : is_iso γ := +have mono γ, by apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃; apply_instance, +have epi γ, by apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄; apply_instance, +by exactI is_iso_of_mono_of_epi _ + +end five end category_theory.abelian diff --git a/src/category_theory/abelian/exact.lean b/src/category_theory/abelian/exact.lean index bb203f8df4f95..8db0a9c341379 100644 --- a/src/category_theory/abelian/exact.lean +++ b/src/category_theory/abelian/exact.lean @@ -117,9 +117,32 @@ def is_limit_image' [h : exact f g] : is_limit (kernel_fork.of_ι (image.ι f) (image_ι_comp_eq_zero h.1)) := is_kernel.iso_kernel _ _ (is_limit_image f g) (image_iso_image f).symm $ is_image.lift_fac _ _ +/-- If `(f, g)` is exact, then `coimages.coimage.π g` is a cokernel of `f`. -/ +def is_colimit_coimage [h : exact f g] : is_colimit (cokernel_cofork.of_π (coimages.coimage.π g) + (coimages.comp_coimage_π_eq_zero h.1) : cokernel_cofork f) := +begin + rw exact_iff at h, + refine is_colimit.of_π _ _ _ _ _, + { refine λ W u hu, cokernel.desc (kernel.ι g) u _, + rw [←cokernel.π_desc f u hu, ←category.assoc, h.2, has_zero_morphisms.zero_comp] }, + tidy +end + +/-- If `(f, g)` is exact, then `factor_thru_image g` is a cokernel of `f`. -/ +def is_colimit_image [h : exact f g] : + is_colimit (cokernel_cofork.of_π (factor_thru_image g) (comp_factor_thru_image_eq_zero h.1)) := +is_cokernel.cokernel_iso _ _ (is_colimit_coimage f g) (coimage_iso_image' g) $ + (cancel_mono (image.ι g)).1 $ by simp + lemma exact_cokernel : exact f (cokernel.π f) := by { rw exact_iff, tidy } +instance [exact f g] : mono (cokernel.desc f g (by simp)) := +suffices h : cokernel.desc f g (by simp) = + (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) (is_colimit_image f g)).hom + ≫ image.ι g, by { rw h, apply mono_comp }, +(cancel_epi (cokernel.π f)).1 $ by simp + section variables (Z) diff --git a/src/category_theory/limits/shapes/pullbacks.lean b/src/category_theory/limits/shapes/pullbacks.lean index 6a52b692c2abd..302f8c867766b 100644 --- a/src/category_theory/limits/shapes/pullbacks.lean +++ b/src/category_theory/limits/shapes/pullbacks.lean @@ -144,7 +144,7 @@ def diagram_iso_span (F : walking_span ⥤ C) : F ≅ span (F.map fst) (F.map snd) := nat_iso.of_components (λ j, eq_to_iso (by tidy)) (by tidy) -variables {X Y Z : C} +variables {W X Y Z : C} /-- A pullback cone is just a cone on the cospan formed by two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`.-/ @@ -278,6 +278,25 @@ lemma mono_of_is_limit_mk_id_id (f : X ⟶ Y) mono f := ⟨λ Z g h eq, by { rcases pullback_cone.is_limit.lift' t _ _ eq with ⟨_, rfl, rfl⟩, refl } ⟩ +/-- Suppose `f` and `g` are two morphisms with a common codomain and `s` is a limit cone over the + diagram formed by `f` and `g`. Suppose `f` and `g` both factor through a monomorphism `h` via + `x` and `y`, respectively. Then `s` is also a limit cone over the diagram formed by `x` and + `y`. -/ +def is_limit_of_factors (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [mono h] + (x : X ⟶ W) (y : Y ⟶ W) (hxh : x ≫ h = f) (hyh : y ≫ h = g) (s : pullback_cone f g) + (hs : is_limit s) : is_limit (pullback_cone.mk _ _ (show s.fst ≫ x = s.snd ≫ y, + from (cancel_mono h).1 $ by simp only [category.assoc, hxh, hyh, s.condition])) := +pullback_cone.is_limit_aux' _ $ λ t, + ⟨hs.lift (pullback_cone.mk t.fst t.snd $ by rw [←hxh, ←hyh, reassoc_of t.condition]), + ⟨hs.fac _ walking_cospan.left, hs.fac _ walking_cospan.right, λ r hr hr', + begin + apply pullback_cone.is_limit.hom_ext hs; + simp only [pullback_cone.mk_fst, pullback_cone.mk_snd] at ⊢ hr hr'; + simp only [hr, hr']; + symmetry, + exacts [hs.fac _ walking_cospan.left, hs.fac _ walking_cospan.right] + end⟩⟩ + end pullback_cone /-- A pushout cocone is just a cocone on the span formed by two morphisms `f : X ⟶ Y` and @@ -391,6 +410,26 @@ begin { rwa (is_colimit.desc' t _ _ _).2.2 }, end +/-- Suppose `f` and `g` are two morphisms with a common domain and `s` is a colimit cocone over the + diagram formed by `f` and `g`. Suppose `f` and `g` both factor through an epimorphism `h` via + `x` and `y`, respectively. Then `s` is also a colimit cocone over the diagram formed by `x` and + `y`. -/ +def is_colimit_of_factors (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) [epi h] + (x : W ⟶ Y) (y : W ⟶ Z) (hhx : h ≫ x = f) (hhy : h ≫ y = g) (s : pushout_cocone f g) + (hs : is_colimit s) : is_colimit (pushout_cocone.mk _ _ (show x ≫ s.inl = y ≫ s.inr, + from (cancel_epi h).1 $ by rw [reassoc_of hhx, reassoc_of hhy, s.condition])) := +pushout_cocone.is_colimit_aux' _ $ λ t, + ⟨hs.desc (pushout_cocone.mk t.inl t.inr $ + by rw [←hhx, ←hhy, category.assoc, category.assoc, t.condition]), + ⟨hs.fac _ walking_span.left, hs.fac _ walking_span.right, λ r hr hr', + begin + apply pushout_cocone.is_colimit.hom_ext hs; + simp only [pushout_cocone.mk_inl, pushout_cocone.mk_inr] at ⊢ hr hr'; + simp only [hr, hr']; + symmetry, + exacts [hs.fac _ walking_span.left, hs.fac _ walking_span.right] + end⟩⟩ + end pushout_cocone /-- This is a helper construction that can be useful when verifying that a category has all diff --git a/src/category_theory/limits/shapes/zero.lean b/src/category_theory/limits/shapes/zero.lean index 2a72af8c463bc..1dccd2226a856 100644 --- a/src/category_theory/limits/shapes/zero.lean +++ b/src/category_theory/limits/shapes/zero.lean @@ -415,6 +415,10 @@ lemma image_ι_comp_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [has_image f [epi (factor_thru_image f)] (h : f ≫ g = 0) : image.ι f ≫ g = 0 := zero_of_epi_comp (factor_thru_image f) $ by simp [h] +lemma comp_factor_thru_image_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [has_image g] + (h : f ≫ g = 0) : f ≫ factor_thru_image g = 0 := +zero_of_comp_mono (image.ι g) $ by simp [h] + variables [has_zero_object C] open_locale zero_object diff --git a/src/category_theory/subobject/limits.lean b/src/category_theory/subobject/limits.lean index 8e9f332322e92..1755019941592 100644 --- a/src/category_theory/subobject/limits.lean +++ b/src/category_theory/subobject/limits.lean @@ -115,6 +115,11 @@ def factor_thru_kernel_subobject {W : C} (h : W ⟶ X) (w : h ≫ f = 0) : factor_thru_kernel_subobject f h w ≫ (kernel_subobject f).arrow = h := by { dsimp [factor_thru_kernel_subobject], simp, } +@[simp] lemma factor_thru_kernel_subobject_comp_kernel_subobject_iso {W : C} (h : W ⟶ X) + (w : h ≫ f = 0) : + factor_thru_kernel_subobject f h w ≫ (kernel_subobject_iso f).hom = kernel.lift f h w := +(cancel_mono (kernel.ι f)).1 $ by simp + section variables {f} {X' Y' : C} {f' : X' ⟶ Y'} [has_kernel f']