feat(category_theory): regular monos (#2154)

* feat(category_theory): regular and normal monos

* fixes

* Apply suggestions from code review

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* shorter proofs

* typos, thanks

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* Update src/category_theory/limits/shapes/regular_mono.lean

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* linting

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/category_theory/epi_mono.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton
+Authors: Reid Barton, Scott Morrison
 
 Facts about epimorphisms and monomorphisms.
 
@@ -60,9 +60,6 @@ such that `f ≫ retraction f = 𝟙 X`.
 
 Every split monomorphism is a monomorphism.
 -/
--- TODO:
--- Every split monomorphism is also a regular monomorphism,
--- and this should be proved when they are introduced.
 class split_mono {X Y : C} (f : X ⟶ Y) :=
 (retraction : Y ⟶ X)
 (id' : f ≫ retraction = 𝟙 X . obviously)

src/category_theory/limits/shapes/constructions/pullbacks.lean

@@ -29,7 +29,7 @@ def has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair
 let π₁ : X ⨯ Y ⟶ X := prod.fst, π₂ : X ⨯ Y ⟶ Y := prod.snd, e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g) in
 { cone := pullback_cone.mk (e ≫ π₁) (e ≫ π₂) $ by simp only [category.assoc, equalizer.condition],
   is_limit := pullback_cone.is_limit.mk _
-    (λ s, equalizer.lift (π₁ ≫ f) (π₂ ≫ g) (prod.lift (s.π.app walking_cospan.left)
+    (λ s, equalizer.lift (prod.lift (s.π.app walking_cospan.left)
       (s.π.app walking_cospan.right)) $ by
         rw [←category.assoc, limit.lift_π, ←category.assoc, limit.lift_π];
         exact pullback_cone.condition _)
@@ -61,7 +61,7 @@ let ι₁ : Y ⟶ Y ⨿ Z := coprod.inl, ι₂ : Z ⟶ Y ⨿ Z := coprod.inr,
 { cocone := pushout_cocone.mk (ι₁ ≫ c) (ι₂ ≫ c) $
     by rw [←category.assoc, ←category.assoc, coequalizer.condition],
   is_colimit := pushout_cocone.is_colimit.mk _
-    (λ s, coequalizer.desc (f ≫ ι₁) (g ≫ ι₂) (coprod.desc (s.ι.app walking_span.left)
+    (λ s, coequalizer.desc (coprod.desc (s.ι.app walking_span.left)
       (s.ι.app walking_span.right)) $ by
         rw [category.assoc, colimit.ι_desc, category.assoc, colimit.ι_desc];
         exact pushout_cocone.condition _)

src/category_theory/limits/shapes/equalizers.lean

@@ -327,6 +327,8 @@ limit.π (parallel_pair f g) zero
 @[reassoc] lemma equalizer.condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g :=
 fork.condition $ limit.cone $ parallel_pair f g
 
+variables {f g}
+
 abbreviation equalizer.lift {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : W ⟶ equalizer f g :=
 limit.lift (parallel_pair f g) (fork.of_ι k h)
 
@@ -338,7 +340,15 @@ limit.hom_ext $ cone_parallel_pair_ext _ h
 
 /-- An equalizer morphism is a monomorphism -/
 instance equalizer.ι_mono : mono (equalizer.ι f g) :=
-{ right_cancellation := λ Z h k w, equalizer.hom_ext _ _ w }
+{ right_cancellation := λ Z h k w, equalizer.hom_ext w }
+
+end
+
+section
+variables {f g}
+/-- The equalizer morphism in any limit cone is a monomorphism. -/
+lemma mono_of_is_limit_parallel_pair {c : cone (parallel_pair f g)} (i : is_limit c) : mono (c.π.app zero) :=
+{ right_cancellation := λ Z h k w, i.hom_ext $ cone_parallel_pair_ext _ w }
 
 end
 
@@ -413,6 +423,8 @@ colimit.ι (parallel_pair f g) one
 @[reassoc] lemma coequalizer.condition : f ≫ coequalizer.π f g = g ≫ coequalizer.π f g :=
 cofork.condition $ colimit.cocone $ parallel_pair f g
 
+variables {f g}
+
 abbreviation coequalizer.desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : coequalizer f g ⟶ W :=
 colimit.desc (parallel_pair f g) (cofork.of_π k h)
 
@@ -424,7 +436,16 @@ colimit.hom_ext $ cocone_parallel_pair_ext _ h
 
 /-- A coequalizer morphism is an epimorphism -/
 instance coequalizer.π_epi : epi (coequalizer.π f g) :=
-{ left_cancellation := λ Z h k w, coequalizer.hom_ext _ _ w }
+{ left_cancellation := λ Z h k w, coequalizer.hom_ext w }
+
+end
+
+section
+variables {f g}
+
+/-- The coequalizer morphism in any colimit cocone is an epimorphism. -/
+lemma epi_of_is_colimit_parallel_pair {c : cocone (parallel_pair f g)} (i : is_colimit c) : epi (c.ι.app one) :=
+{ left_cancellation := λ Z h k w, i.hom_ext $ cocone_parallel_pair_ext _ w }
 
 end
 

src/category_theory/limits/shapes/images.lean

@@ -204,7 +204,7 @@ instance [Π {Z : C} (g h : image f ⟶ Z), has_limit.{v} (parallel_pair g h)] :
 ⟨λ Z g h w,
 begin
   let q := equalizer.ι g h,
-  let e' := equalizer.lift _ _ _ w, -- TODO make more of the arguments to equalizer.lift implicit?
+  let e' := equalizer.lift _ w,
   let F' : mono_factorisation f :=
   { I := equalizer g h,
     m := q ≫ image.ι f,

src/category_theory/limits/shapes/regular_mono.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.epi_mono
+import category_theory.limits.shapes.kernels
+
+/-!
+# Definitions and basic properties of regular and normal monomorphisms and epimorphisms.
+
+A regular monomorphism is a morphism that is the equalizer of some parallel pair.
+A normal monomorphism is a morphism that is the kernel of some other morphism.
+
+We give the constructions
+* `split_mono → regular_mono`
+* `normal_mono → regular_mono`, and
+* `regular_mono → mono`.
+-/
+
+namespace category_theory
+open category_theory.limits
+
+universes v₁ u₁
+
+variables {C : Type u₁} [𝒞 : category.{v₁} C]
+include 𝒞
+
+variables {X Y : C}
+
+/-- A regular monomorphism is a morphism which is the equalizer of some parallel pair. -/
+class regular_mono (f : X ⟶ Y) :=
+(Z : C)
+(left right : Y ⟶ Z)
+(w : f ≫ left = f ≫ right)
+(is_limit : is_limit (fork.of_ι f w))
+
+/-- Every regular monomorphism is a monomorphism. -/
+@[priority 100]
+instance regular_mono.mono (f : X ⟶ Y) [regular_mono f] : mono f :=
+mono_of_is_limit_parallel_pair (regular_mono.is_limit f)
+
+/-- Every split monomorphism is a regular monomorphism. -/
+@[priority 100]
+instance regular_mono.of_split_mono (f : X ⟶ Y) [split_mono f] : regular_mono f :=
+{ Z     := Y,
+  left  := 𝟙 Y,
+  right := retraction f ≫ f,
+  w     := by tidy,
+  is_limit := split_mono_equalizes f }
+
+section
+variables [has_zero_morphisms.{v₁} C]
+/-- A normal monomorphism is a morphism which is the kernel of some morphism. -/
+class normal_mono (f : X ⟶ Y) :=
+(Z : C)
+(g : Y ⟶ Z)
+(w : f ≫ g = 0)
+(is_limit : is_limit (kernel_fork.of_ι f w))
+
+/-- Every normal monomorphism is a regular monomorphism. -/
+@[priority 100]
+instance normal_mono.regular_mono (f : X ⟶ Y) [I : normal_mono f] : regular_mono f :=
+{ left := I.g,
+  right := 0,
+  w := (by simpa using I.w),
+  ..I }
+end
+
+/-- A regular epimorphism is a morphism which is the coequalizer of some parallel pair. -/
+class regular_epi (f : X ⟶ Y) :=
+(W : C)
+(left right : W ⟶ X)
+(w : left ≫ f = right ≫ f)
+(is_colimit : is_colimit (cofork.of_π f w))
+
+/-- Every regular epimorphism is an epimorphism. -/
+@[priority 100]
+instance regular_epi.epi (f : X ⟶ Y) [regular_epi f] : epi f :=
+epi_of_is_colimit_parallel_pair (regular_epi.is_colimit f)
+
+/-- Every split epimorphism is a regular epimorphism. -/
+@[priority 100]
+instance regular_epi.of_split_epi (f : X ⟶ Y) [split_epi f] : regular_epi f :=
+{ W     := X,
+  left  := 𝟙 X,
+  right := f ≫ section_ f,
+  w     := by tidy,
+  is_colimit := split_epi_coequalizes f }
+
+
+section
+variables [has_zero_morphisms.{v₁} C]
+/-- A normal epimorphism is a morphism which is the cokernel of some morphism. -/
+class normal_epi (f : X ⟶ Y) :=
+(W : C)
+(g : W ⟶ X)
+(w : g ≫ f = 0)
+(is_colimit : is_colimit (cokernel_cofork.of_π f w))
+
+/-- Every normal epimorphism is a regular epimorphism. -/
+@[priority 100]
+instance normal_epi.regular_epi (f : X ⟶ Y) [I : normal_epi f] : regular_epi f :=
+{ left := I.g,
+  right := 0,
+  w := (by simpa using I.w),
+  ..I }
+end
+
+end category_theory