feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715)

Also some minor cleanup to the same file.

Author: rwbarton

src/category_theory/full_subcategory.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Reid Barton
 -/
 import category_theory.fully_faithful
+import category_theory.groupoid
 
 namespace category_theory
 
@@ -55,18 +56,22 @@ instance induced_category.category : category.{v} (induced_category D F) :=
   id   := λ X, 𝟙 (F X),
   comp := λ _ _ _ f g, f ≫ g }
 
-def induced_functor : induced_category D F ⥤ D :=
+@[simps] def induced_functor : induced_category D F ⥤ D :=
 { obj := F, map := λ x y f, f }
 
-@[simp] lemma induced_functor.obj {X} : (induced_functor F).obj X = F X := rfl
-@[simp] lemma induced_functor.hom {X Y} {f : X ⟶ Y} : (induced_functor F).map f = f := rfl
-
 instance induced_category.full : full (induced_functor F) :=
 { preimage := λ x y f, f }
 instance induced_category.faithful : faithful (induced_functor F) := {}
 
 end induced
 
+instance induced_category.groupoid {C : Type u₁} (D : Type u₂) [groupoid.{v} D] (F : C → D) :
+   groupoid.{v} (induced_category D F) :=
+{ inv       := λ X Y f, groupoid.inv f,
+  inv_comp' := λ X Y f, groupoid.inv_comp f,
+  comp_inv' := λ X Y f, groupoid.comp_inv f,
+  .. induced_category.category F }
+
 section full_subcategory
 /- A full subcategory is the special case of an induced category with F = subtype.val. -/
 
@@ -84,7 +89,7 @@ induced_functor subtype.val
 @[simp] lemma full_subcategory_inclusion.map {X Y} {f : X ⟶ Y} :
   (full_subcategory_inclusion Z).map f = f := rfl
 
-instance full_subcategory.ful : full (full_subcategory_inclusion Z) :=
+instance full_subcategory.full : full (full_subcategory_inclusion Z) :=
 induced_category.full subtype.val
 instance full_subcategory.faithful : faithful (full_subcategory_inclusion Z) :=
 induced_category.faithful subtype.val