refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)

This PR makes a distinction between the class `is_split_epi f` which is a `Prop` and `split_epi f` which contains the datum of a section of `f`.

src/category_theory/adjunction/reflective.lean

@@ -89,8 +89,8 @@ lemma mem_ess_image_of_unit_is_iso [is_right_adjoint i] (A : C)
 ⟨(left_adjoint i).obj A, ⟨(as_iso ((of_right_adjoint i).unit.app A)).symm⟩⟩
 
 /-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/
-lemma mem_ess_image_of_unit_split_mono [reflective i] {A : C}
-  [split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image :=
+lemma mem_ess_image_of_unit_is_split_mono [reflective i] {A : C}
+  [is_split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image :=
 begin
   let η : 𝟭 C ⟶ left_adjoint i ⋙ i := (of_right_adjoint i).unit,
   haveI : is_iso (η.app (i.obj ((left_adjoint i).obj A))) := (i.obj_mem_ess_image _).unit_is_iso,
@@ -99,7 +99,7 @@ begin
     rw (show retraction _ ≫ η.app A = _, from η.naturality (retraction (η.app A))),
     apply epi_comp (η.app (i.obj ((left_adjoint i).obj A))) },
   resetI,
-  haveI := is_iso_of_epi_of_split_mono (η.app A),
+  haveI := is_iso_of_epi_of_is_split_mono (η.app A),
   exact mem_ess_image_of_unit_is_iso A,
 end
 

src/category_theory/closed/cartesian.lean

@@ -306,8 +306,8 @@ lemma strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
 begin
   haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _,
   rw [zero_mul_hom, prod.lift_snd] at _inst,
-  haveI: split_epi f := ⟨t.to _, t.hom_ext _ _⟩,
-  apply is_iso_of_mono_of_split_epi
+  haveI: is_split_epi f := is_split_epi.mk' ⟨t.to _, t.hom_ext _ _⟩,
+  apply is_iso_of_mono_of_is_split_epi
 end
 
 instance to_initial_is_iso [has_initial C] (f : A ⟶ ⊥_ C) : is_iso f :=

src/category_theory/closed/ideal.lean

@@ -143,8 +143,8 @@ begin
         ir.hom_equiv_apply_eq, assoc, assoc, prod_comparison_natural_assoc, L.map_id,
         ← prod.map_id_comp_assoc, ir.left_triangle_components, prod.map_id_id, id_comp],
     apply is_iso.hom_inv_id_assoc },
-  haveI : split_mono (η.app (A ⟹ i.obj B)) := ⟨_, this⟩,
-  apply mem_ess_image_of_unit_split_mono,
+  haveI : is_split_mono (η.app (A ⟹ i.obj B)) := is_split_mono.mk' ⟨_, this⟩,
+  apply mem_ess_image_of_unit_is_split_mono,
 end
 
 variables [exponential_ideal i]

src/category_theory/epi_mono.lean

@@ -33,94 +33,146 @@ instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
 ⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩
 
 /--
-A split monomorphism is a morphism `f : X ⟶ Y` admitting a retraction `retraction f : Y ⟶ X`
+A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X`
 such that `f ≫ retraction f = 𝟙 X`.
 
 Every split monomorphism is a monomorphism.
 -/
-@[ext]
-class split_mono {X Y : C} (f : X ⟶ Y) :=
+@[ext, nolint has_nonempty_instance]
+structure split_mono {X Y : C} (f : X ⟶ Y) :=
 (retraction : Y ⟶ X)
 (id' : f ≫ retraction = 𝟙 X . obviously)
 
+restate_axiom split_mono.id'
+attribute [simp, reassoc] split_mono.id
+
+/-- `is_split_mono f` is the assertion that `f` admits a retraction -/
+class is_split_mono {X Y : C} (f : X ⟶ Y) : Prop :=
+(exists_split_mono : nonempty (split_mono f))
+
+/-- A constructor for `is_split_mono f` taking a `split_mono f` as an argument -/
+lemma is_split_mono.mk' {X Y : C} {f : X ⟶ Y} (sm : split_mono f) :
+  is_split_mono f := ⟨nonempty.intro sm⟩
+
 /--
-A split epimorphism is a morphism `f : X ⟶ Y` admitting a section `section_ f : Y ⟶ X`
+A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X`
 such that `section_ f ≫ f = 𝟙 Y`.
 (Note that `section` is a reserved keyword, so we append an underscore.)
 
 Every split epimorphism is an epimorphism.
 -/
-@[ext]
-class split_epi {X Y : C} (f : X ⟶ Y) :=
+@[ext, nolint has_nonempty_instance]
+structure split_epi {X Y : C} (f : X ⟶ Y) :=
 (section_ : Y ⟶ X)
 (id' : section_ ≫ f = 𝟙 Y . obviously)
 
+restate_axiom split_epi.id'
+attribute [simp, reassoc] split_epi.id
+
+/-- `is_split_epi f` is the assertion that `f` admits a section -/
+class is_split_epi {X Y : C} (f : X ⟶ Y) : Prop :=
+(exists_split_epi : nonempty (split_epi f))
+
+/-- A constructor for `is_split_epi f` taking a `split_epi f` as an argument -/
+lemma is_split_epi.mk' {X Y : C} {f : X ⟶ Y} (se : split_epi f) :
+  is_split_epi f := ⟨nonempty.intro se⟩
+
 /-- The chosen retraction of a split monomorphism. -/
-def retraction {X Y : C} (f : X ⟶ Y) [split_mono f] : Y ⟶ X := split_mono.retraction f
+noncomputable def retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : Y ⟶ X :=
+hf.exists_split_mono.some.retraction
+
 @[simp, reassoc]
-lemma split_mono.id {X Y : C} (f : X ⟶ Y) [split_mono f] : f ≫ retraction f = 𝟙 X :=
-split_mono.id'
+lemma is_split_mono.id {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : f ≫ retraction f = 𝟙 X :=
+hf.exists_split_mono.some.id
+
+/-- The retraction of a split monomorphism has an obvious section. -/
+def split_mono.split_epi {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : split_epi (sm.retraction) :=
+{ section_ := f, }
+
 /-- The retraction of a split monomorphism is itself a split epimorphism. -/
-instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi (retraction f) :=
-{ section_ := f }
+instance retraction_is_split_epi {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] :
+is_split_epi (retraction f) :=
+is_split_epi.mk' (split_mono.split_epi _)
 
 /-- A split mono which is epi is an iso. -/
-lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
+lemma is_iso_of_epi_of_is_split_mono {X Y : C} (f : X ⟶ Y) [is_split_mono f] [epi f] : is_iso f :=
 ⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩
 
 /--
 The chosen section of a split epimorphism.
 (Note that `section` is a reserved keyword, so we append an underscore.)
 -/
-def section_ {X Y : C} (f : X ⟶ Y) [split_epi f] : Y ⟶ X := split_epi.section_ f
+noncomputable def section_ {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : Y ⟶ X :=
+hf.exists_split_epi.some.section_
+
 @[simp, reassoc]
-lemma split_epi.id {X Y : C} (f : X ⟶ Y) [split_epi f] : section_ f ≫ f = 𝟙 Y :=
-split_epi.id'
+lemma is_split_epi.id {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : section_ f ≫ f = 𝟙 Y :=
+hf.exists_split_epi.some.id
+
+/-- The section of a split epimorphism has an obvious retraction. -/
+def split_epi.split_mono {X Y : C} {f : X ⟶ Y} (se : split_epi f) : split_mono (se.section_) :=
+{ retraction := f, }
+
 /-- The section of a split epimorphism is itself a split monomorphism. -/
-instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (section_ f) :=
-{ retraction := f }
+instance section_is_split_mono {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] :
+  is_split_mono (section_ f) :=
+is_split_mono.mk' (split_epi.split_mono _)
 
 /-- A split epi which is mono is an iso. -/
-lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
+lemma is_iso_of_mono_of_is_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [is_split_epi f] : is_iso f :=
 ⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩
 
 /-- Every iso is a split mono. -/
 @[priority 100]
-noncomputable
-instance split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_mono f :=
-{ retraction := inv f }
+instance is_split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_mono f :=
+is_split_mono.mk' { retraction := inv f }
 
 /-- Every iso is a split epi. -/
 @[priority 100]
-noncomputable
-instance split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_epi f :=
-{ section_ := inv f }
+instance is_split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_epi f :=
+is_split_epi.mk' { section_ := inv f }
+
+lemma split_mono.mono {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : mono f :=
+{ right_cancellation := λ Z g h w, begin replace w := w =≫ sm.retraction, simpa using w, end }
 
 /-- Every split mono is a mono. -/
 @[priority 100]
-instance split_mono.mono {X Y : C} (f : X ⟶ Y) [split_mono f] : mono f :=
-{ right_cancellation := λ Z g h w, begin replace w := w =≫ retraction f, simpa using w, end }
+instance is_split_mono.mono {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : mono f :=
+hf.exists_split_mono.some.mono
+
+lemma split_epi.epi {X Y : C} {f : X ⟶ Y} (se : split_epi f) : epi f :=
+{ left_cancellation := λ Z g h w, begin replace w := se.section_ ≫= w, simpa using w, end }
 
 /-- Every split epi is an epi. -/
 @[priority 100]
-instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
-{ left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end }
+instance is_split_epi.epi {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : epi f :=
+hf.exists_split_epi.some.epi
+
+/-- Every split mono whose retraction is mono is an iso. -/
+lemma is_iso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : split_mono f)
+  [mono $ hf.retraction] : is_iso f :=
+⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id $ hf.retraction).mp (by simp)⟩⟩⟩
 
 /-- Every split mono whose retraction is mono is an iso. -/
-lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
-  : is_iso f :=
-⟨⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩⟩
+lemma is_iso.of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f]
+  [hf' : mono $ retraction f] : is_iso f :=
+@is_iso.of_mono_retraction' _ _ _ _ _ hf.exists_split_mono.some hf'
 
 /-- Every split epi whose section is epi is an iso. -/
-lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
-  : is_iso f :=
-⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩
+lemma is_iso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : split_epi f)
+  [epi $ hf.section_] : is_iso f :=
+⟨⟨hf.section_, ⟨(cancel_epi_id $ hf.section_).mp (by simp), by simp⟩⟩⟩
+
+/-- Every split epi whose section is epi is an iso. -/
+lemma is_iso.of_epi_section {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f]
+  [hf' : epi $ section_ f] : is_iso f :=
+@is_iso.of_epi_section' _ _ _ _ _ hf.exists_split_epi.some hf'
 
 /-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
 -- FIXME this has unnecessarily become noncomputable!
 noncomputable
 def groupoid.of_trunc_split_mono
-  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
+  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (is_split_mono f)) :
   groupoid.{v₁} C :=
 begin
   apply groupoid.of_is_iso,
@@ -135,36 +187,48 @@ 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)
+(is_split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], is_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)
+(is_split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], is_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 _
+lemma is_split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] :
+  is_split_mono f :=
+split_mono_category.is_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 _
+lemma is_split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] :
+  is_split_epi f := split_epi_category.is_split_epi_of_epi _
 
 section
 variables {D : Type u₂} [category.{v₂} D]
 
 /-- Split monomorphisms are also absolute monomorphisms. -/
-instance {X Y : C} (f : X ⟶ Y) [split_mono f] (F : C ⥤ D) : split_mono (F.map f) :=
-{ retraction := F.map (retraction f),
+@[simps]
+def split_mono.map {X Y : C} {f : X ⟶ Y} (sm : split_mono f) (F : C ⥤ D ) :
+  split_mono (F.map f) :=
+{ retraction := F.map (sm.retraction),
   id' := by { rw [←functor.map_comp, split_mono.id, functor.map_id], } }
 
 /-- Split epimorphisms are also absolute epimorphisms. -/
-instance {X Y : C} (f : X ⟶ Y) [split_epi f] (F : C ⥤ D) : split_epi (F.map f) :=
-{ section_ := F.map (section_ f),
+@[simps]
+def split_epi.map {X Y : C} {f : X ⟶ Y} (se : split_epi f) (F : C ⥤ D ) :
+  split_epi (F.map f) :=
+{ section_ := F.map (se.section_),
   id' := by { rw [←functor.map_comp, split_epi.id, functor.map_id], } }
+
+instance {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] (F : C ⥤ D) : is_split_mono (F.map f) :=
+is_split_mono.mk' (hf.exists_split_mono.some.map F)
+
+instance {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] (F : C ⥤ D) : is_split_epi (F.map f) :=
+is_split_epi.mk' (hf.exists_split_epi.some.map F)
+
 end
 
 end category_theory

src/category_theory/functor/epi_mono.lean

@@ -171,19 +171,9 @@ section
 
 variables (F : C ⥤ D) {X Y : C} (f : X ⟶ Y)
 
-/-- Split epimorphisms are preserved by the application of any functor. -/
-@[simps]
-def map_split_epi (s : split_epi f) : split_epi (F.map f) :=
-⟨F.map s.section_, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_epi.id, }⟩
-
-/-- Split monomorphisms are preserved by the application of any functor. -/
-@[simps]
-def map_split_mono (s : split_mono f) : split_mono (F.map f) :=
-⟨F.map s.retraction, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_mono.id, }⟩
-
 /-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/
 def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f) :=
-{ to_fun := F.map_split_epi f,
+{ to_fun := λ f, f.map F,
   inv_fun := λ s, begin
     refine ⟨F.preimage s.section_, _⟩,
     apply F.map_injective,
@@ -195,7 +185,7 @@ def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f)
 
 /-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
 def split_mono_equiv [full F] [faithful F] : split_mono f ≃ split_mono (F.map f) :=
-{ to_fun := F.map_split_mono f,
+{ to_fun := λ f, f.map F,
   inv_fun := λ s, begin
     refine ⟨F.preimage s.retraction, _⟩,
     apply F.map_injective,

src/category_theory/generator.lean

@@ -278,9 +278,10 @@ begin
     haveI : mono t := (is_coseparating_iff_mono 𝒢).1 h𝒢 A,
     exact subobject.of_le_mk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd },
   { generalize : default = g,
-    suffices : split_epi (equalizer.ι f g),
+    suffices : is_split_epi (equalizer.ι f g),
     { exactI eq_of_epi_equalizer },
-    exact ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _) bot_le, by { ext, simp }⟩ }
+    exact is_split_epi.mk' ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _)
+      bot_le, by { ext, simp }⟩ }
 end
 
 /-- An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered

src/category_theory/limits/constructions/weakly_initial.lean

@@ -56,7 +56,7 @@ begin
     { rw [category.assoc, category.assoc],
       apply wide_equalizer.condition (id : endos → endos) (h ≫ e ≫ i) },
     rw [category.comp_id, cancel_mono_id i] at this,
-    haveI : split_epi e := ⟨i ≫ h, this⟩,
+    haveI : is_split_epi e := is_split_epi.mk' ⟨i ≫ h, this⟩,
     rw ←cancel_epi e,
     apply equalizer.condition },
   exactI has_initial_of_unique (wide_equalizer (id : endos → endos)),