feat(category_theory): full and faithful functors, switching products

also the evaluation functor, and replace the ↝ arrow with ⥤, by request

Author: Scott Morrison

category_theory/category.lean

@@ -66,6 +66,7 @@ A `small_category` has objects and morphisms in the same universe level.
 -/
 abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C
 
+section
 variables {C : Type u} [𝒞 : category.{u v} C] {X Y Z : C}
 include 𝒞
 
@@ -78,6 +79,16 @@ class mono (f : X ⟶ Y) : Prop :=
 ⟨ λ p, epi.left_cancellation g h p, begin intro a, subst a end ⟩
 @[simp] lemma cancel_mono (f : X ⟶ Y) [mono f] (g h : Z ⟶ X) : (g ≫ f = h ≫ f) ↔ g = h := 
 ⟨ λ p, mono.right_cancellation g h p, begin intro a, subst a end ⟩
+end
 
+section
+variable (C : Type u)
+variable [small_category C]
+
+instance : large_category (ulift.{(u+1)} C) := 
+{ hom  := λ X Y, (X.down ⟶ Y.down),
+  id   := λ X, 𝟙 X.down,
+  comp := λ _ _ _ f g, f ≫ g }
+end
 
 end category_theory

category_theory/embedding.lean

@@ -0,0 +1,55 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.isomorphism
+
+namespace category_theory
+
+universes u₁ v₁ u₂ v₂
+
+section
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒞 𝒟
+
+class full (F : C ⥤ D) :=
+(preimage : ∀ {X Y : C} (f : (F X) ⟶ (F Y)), X ⟶ Y)
+(witness'  : ∀ {X Y : C} (f : (F X) ⟶ (F Y)), F.map (preimage f) = f . obviously)
+
+restate_axiom full.witness'
+attribute [simp] full.witness
+
+def preimage (F : C ⥤ D) [full F] {X Y : C} (f : F X ⟶ F Y) : X ⟶ Y := full.preimage.{u₁ v₁ u₂ v₂}  f
+@[simp] lemma image_preimage (F : C ⥤ D) [full F] {X Y : C} (f : F X ⟶ F Y) : F.map (preimage F f) = f := begin unfold preimage, obviously end
+
+class faithful (F : C ⥤ D) : Prop :=
+(injectivity' : ∀ {X Y : C} {f g : X ⟶ Y} (p : F.map f = F.map g), f = g . obviously)
+
+restate_axiom faithful.injectivity'
+
+section
+variables  {F : C ⥤ D} [full F] [faithful F] {X Y : C}
+def preimage_iso (f : (F X) ≅ (F Y)) : X ≅ Y := 
+{ hom := preimage F (f : F X ⟶ F Y),
+  inv := preimage F (f.symm : F Y ⟶ F X),
+  hom_inv_id' := begin apply @faithful.injectivity _ _ _ _ F, obviously, end,
+  inv_hom_id' := begin apply @faithful.injectivity _ _ _ _ F, obviously, end, }
+
+@[simp] lemma preimage_iso_coe (f : (F X) ≅ (F Y)) : ((preimage_iso f) : X ⟶ Y) = preimage F (f : F X ⟶ F Y) := rfl
+@[simp] lemma preimage_iso_symm_coe (f : (F X) ≅ (F Y)) : ((preimage_iso f).symm : Y ⟶ X) = preimage F (f.symm : F Y ⟶ F X) := rfl
+end
+
+class embedding (F : C ⥤ D) extends (full F), (faithful F).
+end
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+instance : full (functor.id C) :=
+{ preimage := λ _ _ f, f }
+
+instance : faithful (functor.id C) := by obviously
+
+instance : embedding (functor.id C) := { ((by apply_instance) : full (functor.id C)) with }
+
+end category_theory

category_theory/functor.lean

@@ -9,7 +9,7 @@ Defines a functor between categories.
 by the underlying function on objects, the name is capitalised.)
 
 Introduces notations
-  `C ↝ D` for the type of all functors from `C` to `D`. 
+  `C ⥤ D` for the type of all functors from `C` to `D`. 
     (I would like a better arrow here, unfortunately ⇒ (`\functor`) is taken by core.)
   `F X` (a coercion) for a functor `F` acting on an object `X`.
 -/
@@ -39,31 +39,31 @@ structure functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [cate
 (map_id'   : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X) . obviously)
 (map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = (map' f) ≫ (map' g) . obviously)
 
-infixr ` ↝ `:70 := functor       -- type as \lea --
+infixr ` ⥤ `:70 := functor       -- type as \func --
 
 namespace functor
 
 section
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
-instance : has_coe_to_fun (C ↝ D) :=
+instance : has_coe_to_fun (C ⥤ D) :=
 { F   := λ F, C → D,
   coe := λ F, F.obj }
 
-def map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
+def map (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
 
-@[simp] lemma map_id (F : C ↝ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := 
+@[simp] lemma map_id (F : C ⥤ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := 
 begin unfold functor.map, erw F.map_id', refl end
-@[simp] lemma map_comp (F : C ↝ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : 
+@[simp] lemma map_comp (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : 
   F.map (f ≫ g) = F.map f ≫ F.map g := 
 begin unfold functor.map, erw F.map_comp' end
 
 -- We define a refl lemma 'refolding' the coercion,
 -- and two lemmas for the coercion applied to an explicit structure.
-@[simp] lemma obj_eq_coe {F : C ↝ D} (X : C) : F.obj X = F X := by unfold_coes
+@[simp] lemma obj_eq_coe {F : C ⥤ D} (X : C) : F.obj X = F X := by unfold_coes
 @[simp] lemma mk_obj (o : C → D) (m mi mc) (X : C) : 
-  ({ functor . obj := o, map' := m, map_id' := mi, map_comp' := mc } : C ↝ D) X = o X := rfl
+  ({ functor . obj := o, map' := m, map_id' := mi, map_comp' := mc } : C ⥤ D) X = o X := rfl
 @[simp] lemma mk_map (o : C → D) (m mi mc) {X Y : C} (f : X ⟶ Y) : 
   functor.map { functor . obj := o, map' := m, map_id' := mi, map_comp' := mc } f = m f := rfl
 end
@@ -73,7 +73,7 @@ variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C]
 include 𝒞
 
 /-- `functor.id C` is the identity functor on a category `C`. -/
-protected def id : C ↝ C :=
+protected def id : C ⥤ C :=
 { obj      := λ X, X,
   map'     := λ _ _ f, f }
 
@@ -92,14 +92,14 @@ include 𝒞 𝒟 ℰ
 /--
 `F ⋙ G` is the composition of a functor `F` and a functor `G` (`F` first, then `G`).
 -/
-def comp (F : C ↝ D) (G : D ↝ E) : C ↝ E :=
+def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E :=
 { obj      := λ X, G (F X),
   map'      := λ _ _ f, G.map (F.map f) }
 
 infixr ` ⋙ `:80 := comp
 
-@[simp] lemma comp_obj (F : C ↝ D) (G : D ↝ E) (X : C) : (F ⋙ G) X = G (F X) := rfl
-@[simp] lemma comp_map (F : C ↝ D) (G : D ↝ E) (X Y : C) (f : X ⟶ Y) : 
+@[simp] lemma comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F ⋙ G) X = G (F 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
 

category_theory/functor_category.lean

@@ -17,7 +17,7 @@ Notice that if `C` and `D` are both small categories at the same universe level,
 However if `C` and `D` are both large categories at the same universe level, this is a small category at the next higher level.
 -/
 instance functor.category (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : 
-  category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ↝ D) :=
+  category.{(max u₁ v₁ u₂ v₂) (max u₁ v₂)} (C ⥤ D) :=
 { hom     := λ F G, F ⟹ G,
   id      := λ F, nat_trans.id F,
   comp    := λ _ _ _ α β, α ⊟ β }
@@ -28,8 +28,8 @@ section
 variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 
-@[simp] lemma id_app (F : C ↝ D) (X : C) : (𝟙 F : F ⟹ F) X = 𝟙 (F X) := rfl
-@[simp] lemma comp_app {F G H : C ↝ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : 
+@[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟹ F) X = 𝟙 (F X) := rfl
+@[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : 
   ((α ≫ β) : F ⟹ H) X = (α : F ⟹ G) X ≫ (β : G ⟹ H) X := rfl
 end
 
@@ -42,10 +42,10 @@ variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
           {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include 𝒞 𝒟 ℰ
 
-lemma app_naturality {F G : C ↝ (D ↝ E)} (T : F ⟹ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : 
+lemma app_naturality {F G : C ⥤ (D ⥤ E)} (T : F ⟹ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : 
   ((F X).map f) ≫ ((T X) Z) = ((T X) Y) ≫ ((G X).map f) := (T X).naturality f
 
-lemma naturality_app {F G : C ↝ (D ↝ E)} (T : F ⟹ G) (Z : D) {X Y : C} (f : X ⟶ Y) : 
+lemma naturality_app {F G : C ⥤ (D ⥤ E)} (T : F ⟹ G) (Z : D) {X Y : C} (f : X ⟶ Y) : 
   ((F.map f) Z) ≫ ((T Y) Z) = ((T X) Z) ≫ ((G.map f) Z) := congr_fun (congr_arg app (T.naturality f)) Z
 
 end nat_trans

category_theory/isomorphism.lean

@@ -121,16 +121,16 @@ variables {D : Type u₂}
 variables [𝒟 : category.{u₂ v₂} D]
 include 𝒟
 
-def on_iso (F : C ↝ D) {X Y : C} (i : X ≅ Y) : (F X) ≅ (F Y) :=
+def on_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F X) ≅ (F Y) :=
 { hom := F.map i.hom,
   inv := F.map i.inv,
   hom_inv_id' := by erw [←map_comp, iso.hom_inv_id, ←map_id],
   inv_hom_id' := by erw [←map_comp, iso.inv_hom_id, ←map_id] }
 
-@[simp] lemma on_iso_hom (F : C ↝ D) {X Y : C} (i : X ≅ Y) : ((F.on_iso i) : F X ⟶ F Y) = F.map (i : X ⟶ Y) := rfl
-@[simp] lemma on_iso_inv (F : C ↝ D) {X Y : C} (i : X ≅ Y) : ((F.on_iso i).symm : F Y ⟶ F X) = F.map (i.symm : Y ⟶ X) := rfl
+@[simp] lemma on_iso_hom (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : ((F.on_iso i) : F X ⟶ F Y) = F.map (i : X ⟶ Y) := rfl
+@[simp] lemma on_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : ((F.on_iso i).symm : F Y ⟶ F X) = F.map (i.symm : Y ⟶ X) := rfl
 
-instance (F : C ↝ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
+instance (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
 { inv := F.map (inv f),
   hom_inv_id' := begin rw ← F.map_comp, erw is_iso.hom_inv_id, rw map_id, end,
   inv_hom_id' := begin rw ← F.map_comp, erw is_iso.inv_hom_id, rw map_id, end }
@@ -167,7 +167,7 @@ universes u₁ v₁ u₂ v₂
 variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒟
 
-@[simp] lemma eq_to_iso (F : C ↝ D) {X Y : C} (p : X = Y) : F.on_iso (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
+@[simp] lemma eq_to_iso (F : C ⥤ D) {X Y : C} (p : X = Y) : F.on_iso (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
 begin /- obviously says: -/ ext1, induction p, dsimp at *, simp at * end
 end functor
 

category_theory/natural_transformation.lean

@@ -29,40 +29,40 @@ coercion available so you can write `α X` for the component of a transformation
 
 Naturality is expressed by `α.naturality_lemma`.
 -/
-structure nat_trans (F G : C ↝ D) : Type (max u₁ v₂) :=
+structure nat_trans (F G : C ⥤ D) : Type (max u₁ v₂) :=
 (app : Π X : C, (F X) ⟶ (G X))
 (naturality' : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ (app Y) = (app X) ≫ (G.map f) . obviously)
 
 infixr ` ⟹ `:50  := nat_trans             -- type as \==> or ⟹
 
 namespace nat_trans
 
-instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
+instance {F G : C ⥤ D} : has_coe_to_fun (F ⟹ G) :=
 { F   := λ α, Π X : C, (F X) ⟶ (G X),
   coe := λ α, α.app }
 
-@[simp] lemma app_eq_coe {F G : C ↝ D} (α : F ⟹ G) (X : C) : α.app X = α X := by unfold_coes
-@[simp] lemma mk_app {F G : C ↝ D} (app : Π X : C, (F X) ⟶ (G X)) (naturality) (X : C) : 
+@[simp] lemma app_eq_coe {F G : C ⥤ D} (α : F ⟹ G) (X : C) : α.app X = α X := by unfold_coes
+@[simp] lemma mk_app {F G : C ⥤ D} (app : Π X : C, (F X) ⟶ (G X)) (naturality) (X : C) : 
   { nat_trans . app := app, naturality' := naturality } X = app X := rfl 
 
-lemma naturality {F G : C ↝ D} (α : F ⟹ G) {X Y : C} (f : X ⟶ Y) : 
+lemma naturality {F G : C ⥤ D} (α : F ⟹ G) {X Y : C} (f : X ⟶ Y) : 
   (F.map f) ≫ (α Y) = (α X) ≫ (G.map f) := 
 begin 
   /- `obviously'` says: -/ 
   erw nat_trans.naturality', refl
 end
 
 /-- `nat_trans.id F` is the identity natural transformation on a functor `F`. -/
-protected def id (F : C ↝ D) : F ⟹ F :=
-{ app        := λ X, 𝟙 (F X) }
+protected def id (F : C ⥤ D) : F ⟹ F :=
+{ app := λ X, 𝟙 (F X) }
 
-@[simp] lemma id_app (F : C ↝ D) (X : C) : (nat_trans.id F) X = 𝟙 (F X) := rfl
+@[simp] lemma id_app (F : C ⥤ D) (X : C) : (nat_trans.id F) X = 𝟙 (F X) := rfl
 
 open category
 open category_theory.functor
 
 section
-variables {F G H I : C ↝ D}
+variables {F G H I : C ⥤ D}
 
 -- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
 @[extensionality] lemma ext (α β : F ⟹ G) (w : ∀ X : C, α X = β X) : α = β :=
@@ -88,7 +88,7 @@ variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include ℰ
 
 /-- `hcomp α β` is the horizontal composition of natural transformations. -/
-def hcomp {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
+def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
 { app         := λ X : C, (β (F X)) ≫ (I.map (α X)),
   naturality' := begin
                    /- `obviously'` says: -/
@@ -102,12 +102,12 @@ def hcomp {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙
 
 notation α `◫` β:80 := hcomp α β
 
-@[simp] lemma hcomp_app {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) (X : C) : 
+@[simp] lemma hcomp_app {F G : C ⥤ D} {H I : D ⥤ E} (α : F ⟹ G) (β : H ⟹ I) (X : C) : 
   (α ◫ β) X = (β (F X)) ≫ (I.map (α X)) := rfl
 
 -- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we need to use associativity of functor composition
 
-lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : 
+lemma exchange {F G H : C ⥤ D} {I J K : D ⥤ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : 
   ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) :=
 begin
   -- `obviously'` says:

category_theory/opposites.lean

@@ -27,20 +27,20 @@ section
 variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
 include 𝒟
 
-protected definition op (F : C ↝ D) : (Cᵒᵖ) ↝ (Dᵒᵖ) := 
+protected definition op (F : C ⥤ D) : (Cᵒᵖ) ⥤ (Dᵒᵖ) := 
 { obj       := λ X, F X,
   map'      := λ X Y f, F.map f,
   map_id'   := begin /- `obviously'` says: -/ intros, erw [map_id], refl, end,
   map_comp' := begin /- `obviously'` says: -/ intros, erw [map_comp], refl end }
 
-@[simp] lemma opposite_obj (F : C ↝ D) (X : C) : (F.op) X = F X := rfl
-@[simp] lemma opposite_map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F.op).map f = F.map f := rfl
+@[simp] lemma opposite_obj (F : C ⥤ D) (X : C) : (F.op) X = F X := rfl
+@[simp] lemma opposite_map (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : (F.op).map f = F.map f := rfl
 end
 
 variable (C)
 
 /-- `functor.hom` is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y. -/
-definition hom : (Cᵒᵖ × C) ↝ (Type v₁) := 
+definition hom : (Cᵒᵖ × C) ⥤ (Type v₁) := 
 { obj       := λ p, @category.hom C _ p.1 p.2,
   map'      := λ X Y f, λ h, f.1 ≫ h ≫ f.2,
   map_id'   := begin /- `obviously'` says: -/ intros, ext, intros, cases X, dsimp at *, simp, erw [category.id_comp] end,