feat(category_theory): a hierarchy of balanced categories (#11856)

src/algebra/category/Group/abelian.lean

@@ -40,8 +40,8 @@ end
 /-- The category of abelian groups is abelian. -/
 instance : abelian AddCommGroup.{u} :=
 { has_finite_products := ⟨by apply_instance⟩,
-  normal_mono := λ X Y, normal_mono,
-  normal_epi := λ X Y, normal_epi,
+  normal_mono_of_mono := λ X Y, normal_mono,
+  normal_epi_of_epi := λ X Y, normal_epi,
   add_comp' := by { intros, simp only [preadditive.add_comp] },
   comp_add' := by { intros, simp only [preadditive.comp_add] } }
 

src/algebra/category/Module/abelian.lean

@@ -72,8 +72,8 @@ instance : abelian (Module R) :=
 { has_finite_products := ⟨by apply_instance⟩,
   has_kernels := by apply_instance,
   has_cokernels := has_cokernels_Module,
-  normal_mono := λ X Y, normal_mono,
-  normal_epi := λ X Y, normal_epi }
+  normal_mono_of_mono := λ X Y, normal_mono,
+  normal_epi_of_epi := λ X Y, normal_epi }
 
 variables {O : Module.{v} R} (g : N ⟶ O)
 

src/category_theory/abelian/basic.lean

@@ -101,12 +101,10 @@ and every epimorphism is the cokernel of some morphism.
 finite products give a terminal object, and in a preadditive category
 any terminal object is a zero object.)
 -/
-class abelian extends preadditive C :=
+class abelian extends preadditive C, normal_mono_category C, normal_epi_category C :=
 [has_finite_products : has_finite_products C]
 [has_kernels : has_kernels C]
 [has_cokernels : has_cokernels C]
-(normal_mono : Π {X Y : C} (f : X ⟶ Y) [mono f], normal_mono f)
-(normal_epi : Π {X Y : C} (f : X ⟶ Y) [epi f], normal_epi f)
 
 attribute [instance, priority 100] abelian.has_finite_products
 attribute [instance, priority 100] abelian.has_kernels abelian.has_cokernels
@@ -138,28 +136,6 @@ def non_preadditive_abelian : non_preadditive_abelian C := { ..‹abelian C› }
 
 end to_non_preadditive_abelian
 
-section strong
-local attribute [instance] abelian.normal_epi abelian.normal_mono
-
-/-- In an abelian category, every epimorphism is strong. -/
-lemma strong_epi_of_epi {P Q : C} (f : P ⟶ Q) [epi f] : strong_epi f := by apply_instance
-
-/-- In an abelian category, every monomorphism is strong. -/
-lemma strong_mono_of_mono {P Q : C} (f : P ⟶ Q) [mono f] : strong_mono f := by apply_instance
-
-end strong
-
-section mono_epi_iso
-variables {X Y : C} (f : X ⟶ Y)
-
-local attribute [instance] strong_epi_of_epi
-
-/-- In an abelian category, a monomorphism which is also an epimorphism is an isomorphism. -/
-lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
-is_iso_of_mono_of_strong_epi _
-
-end mono_epi_iso
-
 section factor
 local attribute [instance] non_preadditive_abelian
 
@@ -624,8 +600,8 @@ def abelian : abelian C :=
    the goal it creates for the two instances of `has_zero_morphisms`, and the proof is complete. -/
   has_kernels := by convert (by apply_instance : limits.has_kernels C),
   has_cokernels := by convert (by apply_instance : limits.has_cokernels C),
-  normal_mono := by { introsI, convert normal_mono f },
-  normal_epi := by { introsI, convert normal_epi f },
+  normal_mono_of_mono := by { introsI, convert normal_mono_of_mono f },
+  normal_epi_of_epi := by { introsI, convert normal_epi_of_epi f },
   ..non_preadditive_abelian.preadditive }
 
 end category_theory.non_preadditive_abelian

src/category_theory/abelian/non_preadditive.lean

@@ -60,20 +60,17 @@ variables (C : Type u) [category.{v} C]
 
 /-- We call a category `non_preadditive_abelian` if it has a zero object, kernels, cokernels, binary
     products and coproducts, and every monomorphism and every epimorphism is normal. -/
-class non_preadditive_abelian :=
+class non_preadditive_abelian extends has_zero_morphisms C, normal_mono_category C,
+  normal_epi_category C :=
 [has_zero_object : has_zero_object C]
-[has_zero_morphisms : has_zero_morphisms C]
 [has_kernels : has_kernels C]
 [has_cokernels : has_cokernels C]
 [has_finite_products : has_finite_products C]
 [has_finite_coproducts : has_finite_coproducts C]
-(normal_mono : Π {X Y : C} (f : X ⟶ Y) [mono f], normal_mono f)
-(normal_epi : Π {X Y : C} (f : X ⟶ Y) [epi f], normal_epi f)
 
 set_option default_priority 100
 
 attribute [instance] non_preadditive_abelian.has_zero_object
-attribute [instance] non_preadditive_abelian.has_zero_morphisms
 attribute [instance] non_preadditive_abelian.has_kernels
 attribute [instance] non_preadditive_abelian.has_cokernels
 attribute [instance] non_preadditive_abelian.has_finite_products
@@ -94,32 +91,12 @@ variables {C : Type u} [category.{v} C]
 section
 variables [non_preadditive_abelian C]
 
-section strong
-local attribute [instance] non_preadditive_abelian.normal_epi
-
-/-- In a `non_preadditive_abelian` category, every epimorphism is strong. -/
-lemma strong_epi_of_epi {P Q : C} (f : P ⟶ Q) [epi f] : strong_epi f := by apply_instance
-
-end strong
-
-section mono_epi_iso
-variables {X Y : C} (f : X ⟶ Y)
-
-local attribute [instance] strong_epi_of_epi
-
-/-- In a `non_preadditive_abelian` category, a monomorphism which is also an epimorphism is an
-    isomorphism. -/
-lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
-is_iso_of_mono_of_strong_epi _
-
-end mono_epi_iso
-
 /-- The pullback of two monomorphisms exists. -/
 @[irreducible]
 lemma pullback_of_mono {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [mono a] [mono b] :
   has_limit (cospan a b) :=
-let ⟨P, f, haf, i⟩ := non_preadditive_abelian.normal_mono a in
-let ⟨Q, g, hbg, i'⟩ := non_preadditive_abelian.normal_mono b in
+let ⟨P, f, haf, i⟩ := normal_mono_of_mono a in
+let ⟨Q, g, hbg, i'⟩ := normal_mono_of_mono b in
 let ⟨a', ha'⟩ := kernel_fork.is_limit.lift' i (kernel.ι (prod.lift f g)) $
     calc kernel.ι (prod.lift f g) ≫ f
         = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ limits.prod.fst : by rw prod.lift_fst
@@ -159,8 +136,8 @@ has_limit.mk { cone := pullback_cone.mk a' b' $ by { simp at ha' hb', rw [ha', h
 @[irreducible]
 lemma pushout_of_epi {X Y Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [epi a] [epi b] :
   has_colimit (span a b) :=
-let ⟨P, f, hfa, i⟩ := non_preadditive_abelian.normal_epi a in
-let ⟨Q, g, hgb, i'⟩ := non_preadditive_abelian.normal_epi b in
+let ⟨P, f, hfa, i⟩ := normal_epi_of_epi a in
+let ⟨Q, g, hgb, i'⟩ := normal_epi_of_epi b in
 let ⟨a', ha'⟩ := cokernel_cofork.is_colimit.desc' i (cokernel.π (coprod.desc f g)) $
   calc f ≫ cokernel.π (coprod.desc f g)
       = coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) : by rw coprod.inl_desc_assoc
@@ -292,7 +269,7 @@ lemma mono_of_zero_kernel {X Y : C} (f : X ⟶ Y) (Z : C)
   (l : is_limit (kernel_fork.of_ι (0 : Z ⟶ X) (show 0 ≫ f = 0, by simp))) : mono f :=
 ⟨λ P u v huv,
  begin
-  obtain ⟨W, w, hw, hl⟩ := non_preadditive_abelian.normal_epi (coequalizer.π u v),
+  obtain ⟨W, w, hw, hl⟩ := normal_epi_of_epi (coequalizer.π u v),
   obtain ⟨m, hm⟩ := coequalizer.desc' f huv,
   have hwf : w ≫ f = 0,
   { rw [←hm, reassoc_of hw, zero_comp] },
@@ -309,7 +286,7 @@ lemma epi_of_zero_cokernel {X Y : C} (f : X ⟶ Y) (Z : C)
   (l : is_colimit (cokernel_cofork.of_π (0 : Y ⟶ Z) (show f ≫ 0 = 0, by simp))) : epi f :=
 ⟨λ P u v huv,
  begin
-  obtain ⟨W, w, hw, hl⟩ := non_preadditive_abelian.normal_mono (equalizer.ι u v),
+  obtain ⟨W, w, hw, hl⟩ := normal_mono_of_mono (equalizer.ι u v),
   obtain ⟨m, hm⟩ := equalizer.lift' f huv,
   have hwf : f ≫ w = 0,
   { rw [←hm, category.assoc, hw, comp_zero] },
@@ -381,7 +358,7 @@ begin
   -- Since C is abelian, u := ker g ≫ i is the kernel of some morphism h.
   let u := kernel.ι g ≫ i,
   haveI : mono u := mono_comp _ _,
-  haveI hu := non_preadditive_abelian.normal_mono u,
+  haveI hu := normal_mono_of_mono u,
   let h := hu.g,
   -- By hypothesis, p factors through the kernel of g via some t.
   obtain ⟨t, ht⟩ := kernel.lift' g p hpg,
@@ -435,7 +412,7 @@ begin
   -- Since C is abelian, u := p ≫ coker g is the cokernel of some morphism h.
   let u := p ≫ cokernel.π g,
   haveI : epi u := epi_comp _ _,
-  haveI hu := non_preadditive_abelian.normal_epi u,
+  haveI hu := normal_epi_of_epi u,
   let h := hu.g,
   -- By hypothesis, i factors through the cokernel of g via some t.
   obtain ⟨t, ht⟩ := cokernel.desc' g i hgi,

src/category_theory/abelian/opposite.lean

@@ -26,10 +26,10 @@ local attribute [instance]
   has_finite_limits_opposite has_finite_colimits_opposite has_finite_products_opposite
 
 instance : abelian Cᵒᵖ :=
-{ normal_mono := λ X Y f m, by exactI
-    normal_mono_of_normal_epi_unop _ (abelian.normal_epi f.unop),
-  normal_epi := λ X Y f m, by exactI
-    normal_epi_of_normal_mono_unop _ (abelian.normal_mono f.unop), }
+{ normal_mono_of_mono := λ X Y f m, by exactI
+    normal_mono_of_normal_epi_unop _ (normal_epi_of_epi f.unop),
+  normal_epi_of_epi := λ X Y f m, by exactI
+    normal_epi_of_normal_mono_unop _ (normal_mono_of_mono f.unop), }
 
 section
 

src/category_theory/balanced.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.isomorphism
+
+/-!
+# Balanced categories
+
+A category is called balanced if any morphism that is both monic and epic is an isomorphism.
+
+Balanced categories arise frequently. For example, categories in which every monomorphism
+(or epimorphism) is strong are balanced. Examples of this are abelian categories and toposes, such
+as the category of types.
+
+## TODO
+
+The opposite of a balanced category is again balanced.
+
+-/
+
+universes v u
+
+namespace category_theory
+variables {C : Type u} [category.{v} C]
+
+section
+variables (C)
+
+/-- A category is called balanced if any morphism that is both monic and epic is an isomorphism. -/
+class balanced : Prop :=
+(is_iso_of_mono_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [mono f] [epi f], is_iso f)
+
+end
+
+lemma is_iso_of_mono_of_epi [balanced C] {X Y : C} (f : X ⟶ Y) [mono f] [epi f] : is_iso f :=
+balanced.is_iso_of_mono_of_epi _
+
+lemma is_iso_iff_mono_and_epi [balanced C] {X Y : C} (f : X ⟶ Y) : is_iso f ↔ mono f ∧ epi f :=
+⟨λ _, by exactI ⟨infer_instance, infer_instance⟩, λ ⟨_, _⟩, by exactI is_iso_of_mono_of_epi _⟩
+
+end category_theory

src/category_theory/epi_mono.lean

@@ -170,6 +170,29 @@ begin
   apply is_iso.of_mono_retraction,
 end
 
+section
+variables (C)
+
+/-- A split mono category is a category in which every monomorphism is split. -/
+class split_mono_category :=
+(split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], split_mono f)
+
+/-- A split epi category is a category in which every epimorphism is split. -/
+class split_epi_category :=
+(split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], split_epi f)
+
+end
+
+/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
+    instance because it would create an instance loop. -/
+def split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] : split_mono f :=
+split_mono_category.split_mono_of_mono _
+
+/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
+    instance because it would create an instance loop. -/
+def split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] : split_epi f :=
+split_epi_category.split_epi_of_epi _
+
 section
 variables {D : Type u₂} [category.{v₂} D]
 

src/category_theory/limits/shapes/normal_mono.lean

@@ -16,6 +16,11 @@ We give the construction `normal_mono → regular_mono` (`category_theory.normal
 as well as the dual construction for normal epimorphisms. We show equivalences reflect normal
 monomorphisms (`category_theory.equivalence_reflects_normal_mono`), and that the pullback of a
 normal monomorphism is normal (`category_theory.normal_of_is_pullback_snd_of_normal`).
+
+We also define classes `normal_mono_category` and `normal_epi_category` for classes in which
+every monomorphism or epimorphism is normal, and deduce that these categories are
+`regular_mono_category`s resp. `regular_epi_category`s.
+
 -/
 
 noncomputable theory
@@ -106,6 +111,26 @@ def normal_of_is_pullback_fst_of_normal
 normal_mono f :=
 normal_of_is_pullback_snd_of_normal comm.symm (pullback_cone.flip_is_limit t)
 
+section
+variables (C)
+
+/-- A normal mono category is a category in which every monomorphism is normal. -/
+class normal_mono_category :=
+(normal_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], normal_mono f)
+
+end
+
+/-- In a category in which every monomorphism is normal, we can express every monomorphism as
+    a kernel. This is not an instance because it would create an instance loop. -/
+def normal_mono_of_mono [normal_mono_category C] (f : X ⟶ Y) [mono f] : normal_mono f :=
+normal_mono_category.normal_mono_of_mono _
+
+@[priority 100]
+instance regular_mono_category_of_normal_mono_category [normal_mono_category C] :
+  regular_mono_category C :=
+{ regular_mono_of_mono := λ _ _ f _,
+    by { haveI := by exactI normal_mono_of_mono f, apply_instance } }
+
 end
 
 section
@@ -227,4 +252,24 @@ def normal_mono_of_normal_epi_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : normal_epi
       rintro (⟨⟩|⟨⟩); simp,
     end, }
 
+section
+variables (C)
+
+/-- A normal epi category is a category in which every epimorphism is normal. -/
+class normal_epi_category :=
+(normal_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], normal_epi f)
+
+end
+
+/-- In a category in which every epimorphism is normal, we can express every epimorphism as
+    a kernel. This is not an instance because it would create an instance loop. -/
+def normal_epi_of_epi [normal_epi_category C] (f : X ⟶ Y) [epi f] : normal_epi f :=
+normal_epi_category.normal_epi_of_epi _
+
+@[priority 100]
+instance regular_epi_category_of_normal_epi_category [normal_epi_category C] :
+  regular_epi_category C :=
+{ regular_epi_of_epi := λ _ _ f _,
+    by { haveI := by exactI normal_epi_of_epi f, apply_instance } }
+
 end category_theory