From d9941afd5ce299d7947b47c2ff463795e0e3057e Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 20 Apr 2020 07:17:35 +0000 Subject: [PATCH] fix(category_theory/limits): avoid a rewrite in a definition (#2458) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The proof that every equalizer of `f` and `g` is an isomorphism if `f = g` had an ugly rewrite in a definition (introduced by yours truly). This PR reformulates the proof in a cleaner way by working with two morphisms `f` and `g` and a proof of `f = g` right from the start, which is easy to specialze to the case `(f, f)`, instead of trying to reduce the `(f, g)` case to the `(f, f)` case by rewriting. This also lets us get rid of `fork.eq_of_ι_ι`, unless someone wants to keep it, but personally I don't think that using it is ever a good idea. --- .../limits/shapes/equalizers.lean | 182 ++++++------------ .../limits/shapes/kernels.lean | 6 +- 2 files changed, 60 insertions(+), 128 deletions(-) diff --git a/src/category_theory/limits/shapes/equalizers.lean b/src/category_theory/limits/shapes/equalizers.lean index f5a13b0cbe195..a6b353716764f 100644 --- a/src/category_theory/limits/shapes/equalizers.lean +++ b/src/category_theory/limits/shapes/equalizers.lean @@ -284,21 +284,6 @@ def cofork.is_colimit.mk (t : cofork f g) (by erw [←s.w left, ←t.w left, category.assoc, fac]; refl) (fac s), uniq' := uniq } -section -local attribute [ext] cone - -/-- The fork induced by the ι map of some fork `t` is the same as `t` -/ -lemma fork.eq_of_ι_ι (t : fork f g) : t = fork.of_ι (fork.ι t) (fork.condition t) := -begin - have h : t.π = (fork.of_ι (fork.ι t) (fork.condition t)).π, - { ext j, cases j, - { refl }, - { rw ←fork.app_zero_left, refl } }, - tidy -end - -end - /-- This is a helper construction that can be useful when verifying that a category has all equalizers. Given `F : walking_parallel_pair ⥤ C`, which is really the same as `parallel_pair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`, @@ -313,21 +298,6 @@ def cone.of_fork { app := λ X, t.π.app X ≫ eq_to_hom (by tidy), naturality' := λ j j' g, by { cases j; cases j'; cases g; dsimp; simp } } } -section -local attribute [ext] cocone - -/-- The cofork induced by the π map of some fork `t` is the same as `t` -/ -lemma cofork.eq_of_π_π (t : cofork f g) : t = cofork.of_π (cofork.π t) (cofork.condition t) := -begin - have h : t.ι = (cofork.of_π (cofork.π t) (cofork.condition t)).ι, - { ext j, cases j, - { rw ←cofork.left_app_one, refl }, - { refl } }, - tidy -end - -end - /-- This is a helper construction that can be useful when verifying that a category has all coequalizers. Given `F : walking_parallel_pair ⥤ C`, which is really the same as `parallel_pair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`, @@ -435,59 +405,44 @@ lemma mono_of_is_limit_parallel_pair {c : cone (parallel_pair f g)} (i : is_limi end section -/-- The identity determines a cone on the equalizer diagram of f and f -/ -def cone_parallel_pair_self : cone (parallel_pair f f) := -{ X := X, - π := - { app := λ j, match j with | zero := 𝟙 X | one := f end } } - -@[simp] lemma cone_parallel_pair_self_π_app_zero : (cone_parallel_pair_self f).π.app zero = 𝟙 X := -rfl +variables {f g} -@[simp] lemma cone_parallel_pair_self_X : (cone_parallel_pair_self f).X = X := rfl +/-- The identity determines a cone on the equalizer diagram of `f` and `g` if `f = g`. -/ +def id_fork (h : f = g) : fork f g := +fork.of_ι (𝟙 X) $ h ▸ rfl -/-- The identity on X is an equalizer of (f, f) -/ -def is_limit_cone_parallel_pair_self : is_limit (cone_parallel_pair_self f) := -{ lift := λ s, s.π.app zero, - fac' := λ s j, - match j with - | zero := category.comp_id _ - | one := fork.app_zero_left _ - end, - uniq' := λ s m w, by { convert w zero, erw category.comp_id } } +/-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`. -/ +def is_limit_id_fork (h : f = g) : is_limit (id_fork h) := +fork.is_limit.mk _ + (λ s, fork.ι s) + (λ s, category.comp_id _) + (λ s m h, by { convert h zero, exact (category.comp_id _).symm }) -/-- Every equalizer of (f, f) is an isomorphism -/ -def limit_cone_parallel_pair_self_is_iso (c : cone (parallel_pair f f)) (h : is_limit c) : - is_iso (c.π.app zero) := - let c' := cone_parallel_pair_self f, - z : c ≅ c' := is_limit.unique_up_to_iso h (is_limit_cone_parallel_pair_self f) in - is_iso.of_iso (functor.map_iso (cones.forget _) z) +/-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ +def is_iso_limit_cone_parallel_pair_of_eq (h₀ : f = g) {c : cone (parallel_pair f g)} + (h : is_limit c) : is_iso (c.π.app zero) := +is_iso.of_iso $ is_limit.cone_point_unique_up_to_iso h $ is_limit_id_fork h₀ -/-- The equalizer of (f, f) is an isomorphism -/ -def equalizer.ι_of_self [has_limit (parallel_pair f f)] : is_iso (equalizer.ι f f) := -limit_cone_parallel_pair_self_is_iso _ _ $ limit.is_limit _ +/-- The equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ +def equalizer.ι_of_eq [has_limit (parallel_pair f g)] (h : f = g) : is_iso (equalizer.ι f g) := +is_iso_limit_cone_parallel_pair_of_eq h $ limit.is_limit _ -/-- Every equalizer of (f, g), where f = g, is an isomorphism -/ -def limit_cone_parallel_pair_self_is_iso' (c : cone (parallel_pair f g)) (h₀ : is_limit c) - (h₁ : f = g) : is_iso (c.π.app zero) := -begin - rw fork.eq_of_ι_ι c at *, - have h₂ : is_limit (fork.of_ι (c.π.app zero) rfl : fork f f), by convert h₀, - exact limit_cone_parallel_pair_self_is_iso f (fork.of_ι (c.π.app zero) rfl) h₂ -end - -/-- The equalizer of (f, g), where f = g, is an isomorphism -/ -def equalizer.ι_of_self' [has_limit (parallel_pair f g)] (h : f = g) : is_iso (equalizer.ι f g) := -limit_cone_parallel_pair_self_is_iso' _ _ _ (limit.is_limit _) h +/-- Every equalizer of `(f, f)` is an isomorphism. -/ +def is_iso_limit_cone_parallel_pair_of_self {c : cone (parallel_pair f f)} (h : is_limit c) : + is_iso (c.π.app zero) := +is_iso_limit_cone_parallel_pair_of_eq rfl h -/-- An equalizer that is an epimorphism is an isomorphism -/ -def epi_limit_cone_parallel_pair_is_iso (c : cone (parallel_pair f g)) +/-- An equalizer that is an epimorphism is an isomorphism. -/ +def is_iso_limit_cone_parallel_pair_of_epi {c : cone (parallel_pair f g)} (h : is_limit c) [epi (c.π.app zero)] : is_iso (c.π.app zero) := -limit_cone_parallel_pair_self_is_iso' f g c h $ - (cancel_epi (c.π.app zero)).1 (fork.condition c) +is_iso_limit_cone_parallel_pair_of_eq ((cancel_epi _).1 (fork.condition c)) h end +/-- The equalizer of `(f, f)` is an isomorphism. -/ +def equalizer.ι_of_self [has_limit (parallel_pair f f)] : is_iso (equalizer.ι f f) := +equalizer.ι_of_eq rfl + section variables [has_colimit (parallel_pair f g)] @@ -550,68 +505,45 @@ lemma epi_of_is_colimit_parallel_pair {c : cocone (parallel_pair f g)} (i : is_c end section +variables {f g} -/-- The identity determines a cocone on the coequalizer diagram of f and f -/ -def cocone_parallel_pair_self : cocone (parallel_pair f f) := -{ X := Y, - ι := - { app := λ j, match j with | zero := f | one := 𝟙 Y end, - naturality' := λ j j' g, - begin - cases g, - { refl }, - { erw category.comp_id f }, - { dsimp, simp } - end } } - -@[simp] lemma cocone_parallel_pair_self_ι_app_one : (cocone_parallel_pair_self f).ι.app one = 𝟙 Y := -rfl - -@[simp] lemma cocone_parallel_pair_self_X : (cocone_parallel_pair_self f).X = Y := rfl - -/-- The identity on Y is a colimit of (f, f) -/ -def is_colimit_cocone_parallel_pair_self : is_colimit (cocone_parallel_pair_self f) := -{ desc := λ s, s.ι.app one, - fac' := λ s j, - match j with - | zero := cofork.left_app_one _ - | one := category.id_comp _ - end, - uniq' := λ s m w, by { convert w one, erw category.id_comp } } - -/-- Every coequalizer of (f, f) is an isomorphism -/ -def colimit_cocone_parallel_pair_self_is_iso (c : cocone (parallel_pair f f)) (h : is_colimit c) : - is_iso (c.ι.app one) := - let c' := cocone_parallel_pair_self f, - z : c' ≅ c := is_colimit.unique_up_to_iso (is_colimit_cocone_parallel_pair_self f) h in - is_iso.of_iso $ functor.map_iso (cocones.forget _) z +/-- The identity determines a cocone on the coequalizer diagram of `f` and `g`, if `f = g`. -/ +def id_cofork (h : f = g) : cofork f g := +cofork.of_π (𝟙 Y) $ h ▸ rfl -/-- The coequalizer of (f, f) is an isomorphism -/ -def coequalizer.π_of_self [has_colimit (parallel_pair f f)] : is_iso (coequalizer.π f f) := -colimit_cocone_parallel_pair_self_is_iso _ _ $ colimit.is_colimit _ +/-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`. -/ +def is_colimit_id_cofork (h : f = g) : is_colimit (id_cofork h) := +cofork.is_colimit.mk _ + (λ s, cofork.π s) + (λ s, category.id_comp _) + (λ s m h, by { convert h one, exact (category.id_comp _).symm }) -/-- Every coequalizer of (f, g), where f = g, is an isomorphism -/ -def colimit_cocone_parallel_pair_self_is_iso' (c : cocone (parallel_pair f g)) (h₀ : is_colimit c) - (h₁ : f = g) : is_iso (c.ι.app one) := -begin - rw cofork.eq_of_π_π c at *, - have h₂ : is_colimit (cofork.of_π (c.ι.app one) rfl : cofork f f), by convert h₀, - exact colimit_cocone_parallel_pair_self_is_iso f (cofork.of_π (c.ι.app one) rfl) h₂ -end +/-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ +def is_iso_colimit_cocone_parallel_pair_of_eq (h₀ : f = g) {c : cocone (parallel_pair f g)} + (h : is_colimit c) : is_iso (c.ι.app one) := +is_iso.of_iso $ is_colimit.cone_point_unique_up_to_iso (is_colimit_id_cofork h₀) h -/-- The coequalizer of (f, g), where f = g, is an isomorphism -/ -def coequalizer.π_of_self' [has_colimit (parallel_pair f g)] (h : f = g) : +/-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ +def coequalizer.π_of_eq [has_colimit (parallel_pair f g)] (h : f = g) : is_iso (coequalizer.π f g) := -colimit_cocone_parallel_pair_self_is_iso' _ _ _ (colimit.is_colimit _) h +is_iso_colimit_cocone_parallel_pair_of_eq h $ colimit.is_colimit _ + +/-- Every coequalizer of `(f, f)` is an isomorphism. -/ +def is_iso_colimit_cocone_parallel_pair_of_self {c : cocone (parallel_pair f f)} + (h : is_colimit c) : is_iso (c.ι.app one) := +is_iso_colimit_cocone_parallel_pair_of_eq rfl h -/-- A coequalizer that is a monomorphism is an isomorphism -/ -def mono_limit_cocone_parallel_pair_is_iso (c : cocone (parallel_pair f g)) +/-- A coequalizer that is a monomorphism is an isomorphism. -/ +def is_iso_limit_cocone_parallel_pair_of_epi {c : cocone (parallel_pair f g)} (h : is_colimit c) [mono (c.ι.app one)] : is_iso (c.ι.app one) := -colimit_cocone_parallel_pair_self_is_iso' f g c h $ - (cancel_mono (c.ι.app one)).1 (cofork.condition c) +is_iso_colimit_cocone_parallel_pair_of_eq ((cancel_mono _).1 (cofork.condition c)) h end +/-- The coequalizer of `(f, f)` is an isomorphism. -/ +def coequalizer.π_of_self [has_colimit (parallel_pair f f)] : is_iso (coequalizer.π f f) := +coequalizer.π_of_eq rfl + variables (C) /-- `has_equalizers` represents a choice of equalizer for every pair of morphisms -/ diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean index 8d27af7476b88..8e2f8eaeb32aa 100644 --- a/src/category_theory/limits/shapes/kernels.lean +++ b/src/category_theory/limits/shapes/kernels.lean @@ -106,7 +106,7 @@ def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : {l : W ⟶ kernel f / /-- Every kernel of the zero morphism is an isomorphism -/ def kernel.ι_zero_is_iso [has_limit (parallel_pair (0 : X ⟶ Y) 0)] : is_iso (kernel.ι (0 : X ⟶ Y)) := -limit_cone_parallel_pair_self_is_iso _ _ (limit.is_limit _) +equalizer.ι_of_self _ end @@ -258,12 +258,12 @@ variables [has_zero_morphisms.{v} C] /-- The kernel of the cokernel of an epimorphism is an isomorphism -/ instance kernel.of_cokernel_of_epi [has_colimit (parallel_pair f 0)] [has_limit (parallel_pair (cokernel.π f) 0)] [epi f] : is_iso (kernel.ι (cokernel.π f)) := -equalizer.ι_of_self' _ _ $ cokernel.π_of_epi f +equalizer.ι_of_eq $ cokernel.π_of_epi f /-- The cokernel of the kernel of a monomorphism is an isomorphism -/ instance cokernel.of_kernel_of_mono [has_limit (parallel_pair f 0)] [has_colimit (parallel_pair (kernel.ι f) 0)] [mono f] : is_iso (cokernel.π (kernel.ι f)) := -coequalizer.π_of_self' _ _ $ kernel.ι_of_mono f +coequalizer.π_of_eq $ kernel.ι_of_mono f end has_zero_object