feat(category_theory): def is_isomorphic_setoid, `groupoid.iso_equi…

…v_hom` (#1506)

* feat(category_theory): def `is_isomorphic_setoid`, `groupoid.iso_equiv_hom`

* Move to a dedicated file, define `isomorphic_class_functor`

* explicit/implicit arguments

* Update src/category_theory/groupoid.lean

* Update src/category_theory/groupoid.lean

* Update src/category_theory/isomorphism_classes.lean

* Update src/category_theory/isomorphism_classes.lean

* Update src/category_theory/isomorphism_classes.lean

src/category_theory/groupoid.lean

@@ -6,11 +6,13 @@ Authors: Reid Barton
 
 import category_theory.category
 import category_theory.isomorphism
+import data.equiv.basic
 
 namespace category_theory
 
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
+/-- A `groupoid` is a category such that all morphisms are isomorphisms. -/
 class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=
 (inv       : Π {X Y : obj}, (X ⟶ Y) → (Y ⟶ X))
 (inv_comp' : ∀ {X Y : obj} (f : X ⟶ Y), comp (inv f) f = id Y . obviously)
@@ -24,7 +26,22 @@ attribute [simp] groupoid.inv_comp groupoid.comp_inv
 abbreviation large_groupoid (C : Type (u+1)) : Type (u+1) := groupoid.{u} C
 abbreviation small_groupoid (C : Type u) : Type (u+1) := groupoid.{u} C
 
-instance of_groupoid {C : Type u} [groupoid.{v} C] {X Y : C} (f : X ⟶ Y) : is_iso f :=
-{ inv := groupoid.inv f }
+section
+
+variables {C : Type u} [𝒞 : groupoid.{v} C] {X Y : C}
+include 𝒞
+
+instance is_iso.of_groupoid (f : X ⟶ Y) : is_iso f := { inv := groupoid.inv f }
+
+variables (X Y)
+
+/-- In a groupoid, isomorphisms are equivalent to morphisms. -/
+def groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) :=
+{ to_fun := iso.hom,
+  inv_fun := λ f, as_iso f,
+  left_inv := λ i, iso.ext rfl,
+  right_inv := λ f, rfl }
+
+end
 
 end category_theory

src/category_theory/isomorphism_classes.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import category_theory.category.Cat category_theory.groupoid data.quot
+
+/-!
+# Objects of a category up to an isomorphism
+
+`is_isomorphic X Y := nonempty (X ≅ Y)` is an equivalence relation on the objects of a category.
+The quotient with respect to this relation defines a functor from our category to `Type`.
+-/
+
+universes v u
+
+namespace category_theory
+
+section category
+
+variables {C : Type u} [𝒞 : category.{v} C]
+include 𝒞
+
+/-- An object `X` is isomorphic to an object `Y`, if `X ≅ Y` is not empty. -/
+def is_isomorphic : C → C → Prop := λ X Y, nonempty (X ≅ Y)
+
+variable (C)
+
+/-- `is_isomorphic` defines a setoid. -/
+def is_isomorphic_setoid : setoid C :=
+{ r := is_isomorphic,
+  iseqv := ⟨λ X, ⟨iso.refl X⟩, λ X Y ⟨α⟩, ⟨α.symm⟩, λ X Y Z ⟨α⟩ ⟨β⟩, ⟨α.trans β⟩⟩ }
+
+end category
+
+/--
+The functor that sends each category to the quotient space of its objects up to an isomorphism.
+-/
+def isomorphism_classes : Cat.{v u} ⥤ Type u :=
+{ obj := λ C, quotient (is_isomorphic_setoid C.α),
+  map := λ C D F, quot.map F.obj $ λ X Y ⟨f⟩, ⟨F.map_iso f⟩ }
+
+lemma groupoid.is_isomorphic_iff_nonempty_hom {C : Type u} [groupoid.{v} C] {X Y : C} :
+  is_isomorphic X Y ↔ nonempty (X ⟶ Y) :=
+(groupoid.iso_equiv_hom X Y).nonempty_iff_nonempty
+
+-- PROJECT: define `skeletal`, and show every category is equivalent to a skeletal category,
+-- using the axiom of choice to pick a representative of every isomorphism class.
+end category_theory