feat(category_theory/quotient): the quotient functor is full and esse…

…ntially surjective (#7465)





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/category_theory/quotient.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
 -/
 import category_theory.natural_isomorphism
+import category_theory.equivalence
+import category_theory.eq_to_hom
 
 /-!
 # Quotient category
@@ -23,7 +25,8 @@ variables {C : Type u} [category.{v} C]
           (r : Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop)
 include r
 
-/-- A type synonom for `C`, thought of as the objects of the quotient category. -/
+/-- A type synonym for `C`, thought of as the objects of the quotient category. -/
+@[ext]
 structure quotient := (as : C)
 
 instance [inhabited C] : inhabited (quotient r) := ⟨ { as := default C } ⟩
@@ -69,6 +72,12 @@ def functor : C ⥤ quotient r :=
 { obj := λ a, { as := a },
   map := λ _ _ f, quot.mk _ f }
 
+noncomputable instance : full (functor r) :=
+{ preimage := λ X Y f, quot.out f, }
+
+instance : ess_surj (functor r) :=
+{ mem_ess_image := λ Y, ⟨Y.as, ⟨eq_to_iso (by { ext, refl, })⟩⟩ }
+
 protected lemma induction {P : Π {a b : quotient r}, (a ⟶ b) → Prop}
   (h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)) :
   ∀ {a b : quotient r} (f : a ⟶ b), P f :=
@@ -103,6 +112,10 @@ rfl
 lemma lift.is_lift_inv (X : C) : (lift.is_lift r F H).inv.app X = 𝟙 (F.obj X) :=
 rfl
 
+lemma lift_map_functor_map {X Y : C} (f : X ⟶ Y) :
+  (lift r F H).map ((functor r).map f) = F.map f :=
+by { rw ←(nat_iso.naturality_1 (lift.is_lift r F H)), dsimp, simp, }
+
 end quotient
 
 end category_theory