feat(category_theory/*): define Cat and a fully faithful functor Mon ⥤ Cat

src/category_theory/Cat.lean

@@ -0,0 +1,51 @@
+import category_theory.concrete_category
+
+/-!
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+# Category of categories
+
+This file contains definition of category `Cat` of all categories.  In
+this category objects are categories and morphisms are functors
+between these categories.
+
+## Implementation notes
+
+Though `Cat` is not a concrete category, we use `bundled` to define
+its carrier type.
+-/
+
+universes v u
+
+namespace category_theory
+
+/-- Category of categories. -/
+def Cat := bundled category.{v u}
+
+namespace Cat
+
+instance str (C : Cat.{v u}) : category.{v u} C.α := C.str
+
+def of (C : Type u) [category.{v} C] : Cat.{v u} := mk_ob C
+
+/-- Category structure on `Cat` -/
+instance category : category.{(max u v)+1 (max v (u+1))} Cat.{v u} :=
+{ hom := λ C D, C.α ⥤ D.α,
+  id := λ C, 𝟭 C.α,
+  comp := λ C D E F G, F ⋙ G,
+  id_comp' := λ C D F, by cases F; refl,
+  comp_id' := λ C D F, by cases F; refl,
+  assoc' := by intros; refl }
+
+/-- Functor that gets the set of objects of a category. It is not
+called `forget`, because it is not a faithful functor. -/
+def objects : Cat.{v u} ⥤ Type u :=
+{ obj := bundled.α,
+  map := λ C D F, F.obj }
+
+end Cat
+
+end category_theory
+

src/category_theory/functor.lean

@@ -80,6 +80,7 @@ infixr ` ⋙ `:80 := comp
 @[simp] lemma comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F ⋙ G).obj X = G.obj (F.obj X) := rfl
 @[simp] lemma comp_map (F : C ⥤ D) (G : D ⥤ E) (X Y : C) (f : X ⟶ Y) :
   (F ⋙ G).map f = G.map (F.map f) := rfl
+
 end
 
 section

src/category_theory/single_obj.lean

@@ -0,0 +1,124 @@
+import category_theory.endomorphism category_theory.groupoid category_theory.Cat
+import data.equiv.algebra algebra.Mon.basic
+import tactic.find
+
+/-!
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+# Single-object category
+
+Single object category with a given monoid of endomorphisms.  It is defined to faciliate transfering
+some definitions and lemmas (e.g., conjugacy etc.) from category theory to monoids and groups.
+
+## Main definitions
+
+Given a type `α` with a monoid structure, `single_obj α` is `unit` type with `category` structure
+such that `End (single_obj α).star` is the monoid `α`.  This can be extended to a functor `Mon ⥤
+Cat`.
+
+If `α` is a group, then `single_obj α` is a groupoid.
+
+An element `x : α` can be reinterpreted as an element of `End (single_obj.star α)` using
+`single_obj.to_End`.
+
+## Implementation notes
+
+- `category_struct.comp` on `End (single_obj.star α)` is `flip (*)`, not `(*)`. This way
+  multiplication on `End` agrees with the multiplication on `α`.
+
+- By default, Lean puts instances into `category_theory` namespace instead of
+  `category_theory.single_obj`, so we give all names explicitly.
+-/
+
+universes u v w
+
+namespace category_theory
+/-- Type tag on `unit` used to define single-object categories and groupoids. -/
+def single_obj (α : Type u) : Type := unit
+
+namespace single_obj
+
+variables (α : Type u)
+
+/-- One and `flip (*)` become `id` and `comp` for morphisms of the single object category. -/
+instance category_struct [has_one α] [has_mul α] : category_struct (single_obj α) :=
+{ hom := λ _ _, α,
+  comp := λ _ _ _ x y, y * x,
+  id := λ _, 1 }
+
+/-- Monoid laws become category laws for the single object category. -/
+instance category [monoid α] : category (single_obj α) :=
+{ comp_id' := λ _ _, one_mul,
+  id_comp' := λ _ _, mul_one,
+  assoc' := λ _ _ _ _ x y z, (mul_assoc z y x).symm }
+
+/-- Groupoid structure on `single_obj α` -/
+instance groupoid [group α] : groupoid (single_obj α) :=
+{ inv := λ _ _ x, x⁻¹,
+  inv_comp' := λ _ _, mul_right_inv,
+  comp_inv' := λ _ _, mul_left_inv }
+
+protected def star : single_obj α := unit.star
+
+/-- The endomorphisms monoid of the only object in `single_obj α` is equivalent to the original
+     monoid α. -/
+def to_End_equiv [monoid α] : End (single_obj.star α) ≃* α := mul_equiv.refl α
+
+/-- Reinterpret an element of a monoid as an element of the endomorphisms monoid of the only object
+    in the `single_obj α` category. -/
+def to_End {α} [monoid α] (x : α) : End (single_obj.star α) := x
+
+lemma to_End_def [monoid α] (x : α) : to_End x = x := rfl
+
+/-- There is a 1-1 correspondence between monoid homomorphisms `α → β` and functors between the
+    corresponding single-object categories. It means that `single_obj` is a fully faithful
+    functor. -/
+def map_hom_equiv (α : Type u) (β : Type v) [monoid α] [monoid β] :
+  { f : α → β // is_monoid_hom f } ≃ (single_obj α) ⥤ (single_obj β) :=
+{ to_fun := λ f,
+  { obj := id,
+    map := λ _ _, f.1,
+    map_id' := λ _, f.2.map_one,
+    map_comp' := λ _ _ _ x y, @is_mul_hom.map_mul _ _ _ _ _ f.2.1 y x },
+  inv_fun := λ f, ⟨@functor.map _ _ _ _ f (single_obj.star α) (single_obj.star α),
+    { map_mul := λ x y, f.map_comp y x, map_one := f.map_id _ }⟩,
+  left_inv := λ ⟨f, hf⟩, rfl,
+  right_inv := assume f, by rcases f; obviously }
+
+/-- Reinterpret a monoid homomorphism `f : α → β` as a functor `(single_obj α) ⥤ (single_obj β)`.
+See also `map_hom_equiv` for an equivalence between these types. -/
+@[reducible] def map_hom {α : Type u} {β : Type v} [monoid α] [monoid β]
+  (f : α → β) [hf : is_monoid_hom f] :
+  (single_obj α) ⥤ (single_obj β) :=
+map_hom_equiv α β ⟨f, hf⟩
+
+lemma map_hom_id {α : Type u} [monoid α] : map_hom (@id α) = 𝟭 _ := rfl
+
+lemma map_hom_comp {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
+  {γ : Type w} [monoid γ] (g : β → γ) [is_monoid_hom g] :
+  map_hom f ⋙ map_hom g = map_hom (g ∘ f) :=
+rfl
+
+end single_obj
+
+end category_theory
+
+namespace Mon
+
+open category_theory
+
+/-- The fully faithful functor from `Mon` to `Cat`. -/
+def to_Cat : Mon ⥤ Cat :=
+{ obj := λ x, Cat.of (single_obj x),
+  map := λ x y f, single_obj.map_hom f }
+
+instance to_Cat_full : full to_Cat :=
+{ preimage := λ x y, (single_obj.map_hom_equiv x y).inv_fun,
+  witness' := λ x y, (single_obj.map_hom_equiv x y).right_inv }
+
+instance to_Cat_faithful : faithful to_Cat :=
+{ injectivity' := λ x y, (single_obj.map_hom_equiv x y).injective }
+
+end Mon