feat(category_theory): full_of_surjective (#14974)

src/category_theory/functor/fully_faithful.lean

@@ -11,13 +11,18 @@ import logic.equiv.basic
 
 We define typeclasses `full` and `faithful`, decorating functors.
 
-Use `F.map_injective` to retrieve the fact that `F.map` is injective when `[faithful F]`,
-and `F.preimage` to obtain preimages of morphisms when `[full F]`.
-
-We prove some basic "cancellation" lemmas for full and/or faithful functors.
-
-See `category_theory.equivalence` for the fact that a functor is an equivalence if and only if
-it is fully faithful and essentially surjective.
+## Main definitions and results
+* Use `F.map_injective` to retrieve the fact that `F.map` is injective when `[faithful F]`.
+* Similarly, `F.map_surjective` states that `F.map` is surjective when `[full F]`.
+* Use `F.preimage` to obtain preimages of morphisms when `[full F]`.
+* We prove some basic "cancellation" lemmas for full and/or faithful functors, as well as a
+  construction for "dividing" a functor by a faithful functor, see `faithful.div`.
+* `full F` carries data, so definitional properties of the preimage can be used when using
+  `F.preimage`. To obtain an instance of `full F` non-constructively, you can use `full_of_exists`
+  and `full_of_surjective`.
+
+See `category_theory.equivalence.of_fully_faithful_ess_surj` for the fact that a functor is an
+equivalence if and only if it is fully faithful and essentially surjective.
 
 -/
 
@@ -55,8 +60,7 @@ restate_axiom faithful.map_injective'
 namespace functor
 variables {X Y : C}
 
-lemma map_injective (F : C ⥤ D) [faithful F] :
-  function.injective $ @functor.map _ _ _ _ F X Y :=
+lemma map_injective (F : C ⥤ D) [faithful F] : function.injective $ @functor.map _ _ _ _ F X Y :=
 faithful.map_injective F
 
 lemma map_iso_injective (F : C ⥤ D) [faithful F] :
@@ -70,6 +74,19 @@ full.preimage.{v₁ v₂} f
   F.map (preimage F f) = f :=
 by unfold preimage; obviously
 
+lemma map_surjective (F : C ⥤ D) [full F] : function.surjective (@functor.map _ _ _ _ F X Y) :=
+λ f, ⟨F.preimage f, F.image_preimage f⟩
+
+/-- Deduce that `F` is full from the existence of preimages, using choice. -/
+noncomputable def full_of_exists (F : C ⥤ D)
+  (h : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) : full F :=
+by { choose p hp using h, exact ⟨p, hp⟩ }
+
+/-- Deduce that `F` is full from surjectivity of `F.map`, using choice. -/
+noncomputable def full_of_surjective (F : C ⥤ D)
+  (h : ∀ (X Y : C), function.surjective (@functor.map _ _ _ _ F X Y)) : full F :=
+full_of_exists _ h
+
 end functor
 
 section