feat(category_theory): full subcategories, preorders, Aut, and End

category_theory/category.lean

@@ -91,4 +91,20 @@ instance : large_category (ulift.{(u+1)} C) :=
   comp := λ _ _ _ f g, f ≫ g }
 end
 
+variables (α : Type u)
+
+instance [preorder α] : small_category α :=
+{ hom  := λ U V, ulift (plift (U ≤ V)),
+  id   := by tidy,
+  comp := begin tidy, transitivity Y; assumption end }
+
+section
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+
+def End (X : C) := X ⟶ X
+
+instance {X : C} : monoid (End X) := by refine { one := 𝟙 X, mul := λ x y, x ≫ y, .. } ; obviously
+end
+
 end category_theory

category_theory/full_subcategory.lean

@@ -0,0 +1,27 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+import category_theory.embedding
+
+namespace category_theory
+
+universes u v
+
+section
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞 
+
+instance full_subcategory (Z : C → Prop) : category.{u v} {X : C // Z X} := 
+{ hom  := λ X Y, X.1 ⟶ Y.1,
+  id   := λ X, 𝟙 X.1,
+  comp := λ _ _ _ f g, f ≫ g }
+
+def full_subcategory_embedding (Z : C → Prop) : {X : C // Z X} ⥤ C := 
+{ obj := λ X, X.1,
+  map' := λ _ _ f, f }
+
+instance full_subcategory_full     (Z : C → Prop) : full     (full_subcategory_embedding Z) := by obviously
+instance full_subcategory_faithful (Z : C → Prop) : faithful (full_subcategory_embedding Z) := by obviously
+end
+
+end category_theory

category_theory/isomorphism.lean

@@ -171,4 +171,11 @@ include 𝒟
 begin /- obviously says: -/ ext1, induction p, dsimp at *, simp at * end
 end functor
 
+def Aut (X : C) := X ≅ X
+
+instance {X : C} : group (Aut X) := 
+by refine { one := iso.refl X, 
+            inv := iso.symm,
+            mul := iso.trans, .. } ; obviously
+
 end category_theory