feat(category_theory/epi_mono): preserves/reflects properties for epi/split_epi (#15857)

This PR shows that split epi/mono are preserved by any functor, and reflected by fully faithful functors. Moreover, `iff` lemmas are obtained for functors which both preserve and reflect epimorphisms (resp. monomorphisms).



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

src/category_theory/epi_mono.lean

@@ -38,6 +38,7 @@ such that `f ≫ retraction f = 𝟙 X`.
 
 Every split monomorphism is a monomorphism.
 -/
+@[ext]
 class split_mono {X Y : C} (f : X ⟶ Y) :=
 (retraction : Y ⟶ X)
 (id' : f ≫ retraction = 𝟙 X . obviously)
@@ -49,6 +50,7 @@ such that `section_ f ≫ f = 𝟙 Y`.
 
 Every split epimorphism is an epimorphism.
 -/
+@[ext]
 class split_epi {X Y : C} (f : X ⟶ Y) :=
 (section_ : Y ⟶ X)
 (id' : section_ ≫ f = 𝟙 Y . obviously)

src/category_theory/functor/epi_mono.lean

@@ -167,4 +167,64 @@ instance reflects_epimorphisms_of_faithful (F : C ⥤ D) [faithful F] : reflects
 { reflects := λ X Y f hf, ⟨λ Z g h hgh, by exactI F.map_injective ((cancel_epi (F.map f)).1
     (by rw [← F.map_comp, hgh, F.map_comp]))⟩ }
 
+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,
+  inv_fun := λ s, begin
+    refine ⟨F.preimage s.section_, _⟩,
+    apply F.map_injective,
+    simp only [map_comp, image_preimage, map_id],
+    apply split_epi.id,
+  end,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+/-- 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,
+  inv_fun := λ s, begin
+    refine ⟨F.preimage s.retraction, _⟩,
+    apply F.map_injective,
+    simp only [map_comp, image_preimage, map_id],
+    apply split_mono.id,
+  end,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+@[simp]
+lemma epi_map_iff_epi [hF₁ : preserves_epimorphisms F] [hF₂ : reflects_epimorphisms F] :
+  epi (F.map f) ↔ epi f :=
+begin
+  split,
+  { exact F.epi_of_epi_map, },
+  { introI h,
+    exact F.map_epi f, },
+end
+
+@[simp]
+lemma mono_map_iff_mono [hF₁ : preserves_monomorphisms F] [hF₂ : reflects_monomorphisms F] :
+  mono (F.map f) ↔ mono f :=
+begin
+  split,
+  { exact F.mono_of_mono_map, },
+  { introI h,
+    exact F.map_mono f, },
+end
+
+end
+
 end category_theory.functor