feat(category_theory): restating functor.map and nat_trans.app (#268)

Author: kim-em

category_theory/functor.lean

@@ -9,7 +9,8 @@ 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`. (I would like a better arrow here, unfortunately ⇒ (`\functor`) is taken by core.)
+  `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`.
 -/
 
@@ -22,20 +23,20 @@ universes u₁ v₁ u₂ v₂ u₃ v₃
 /--
 `functor C D` represents a functor between categories `C` and `D`.
 
-To apply a functor `F` to an object use `F X`, and to a morphism use `F.map f`.
+To apply a functor `F` to an object use `F X` (which uses a coercion), and to a morphism use `F.map f`.
 
 The axiom `map_id_lemma` expresses preservation of identities, and
 `map_comp_lemma` expresses functoriality.
+
+Implementation note: when constructing a `functor`, you need to define the
+`map'` field (which does not know about the coercion).
+When using a `functor`, use the `map` field (which makes use of the coercion).
 -/
 structure functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : Type (max u₁ v₁ u₂ v₂) :=
 (obj      : C → D)
-(map      : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
-(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)
-
-restate_axiom functor.map_id
-restate_axiom functor.map_comp
-attribute [simp,ematch] functor.map_id_lemma functor.map_comp_lemma
+(map'     : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
+(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 --
 
@@ -49,7 +50,20 @@ instance : has_coe_to_fun (C ↝ D) :=
 { F   := λ F, C → D,
   coe := λ F, F.obj }
 
-@[simp] lemma coe_def (F : C ↝ D) (X : C) : F X = F.obj X := rfl
+def map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
+
+@[simp,ematch] lemma map_id_lemma (F : C ↝ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := 
+begin unfold functor.map, erw F.map_id, refl end
+@[simp,ematch] lemma map_comp_lemma (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 do not define a refl lemma unfolding the coercion.
+-- However we do provide lemmas for the coercion applied to an explicit structure.
+@[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
+@[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
 
 section
@@ -59,7 +73,7 @@ include 𝒞
 /-- `functor.id C` is the identity functor on a category `C`. -/
 protected def id : C ↝ C :=
 { obj      := λ X, X,
-  map      := λ _ _ f, f,
+  map'     := λ _ _ f, f,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
@@ -70,22 +84,25 @@ variable {C}
 end
 
 section
-variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D] {E : Type u₃} [ℰ : category.{u₃ v₃} E]
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] 
+          {D : Type u₂} [𝒟 : category.{u₂ v₂} D] 
+          {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 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 :=
-{ obj      := λ X, G.obj (F.obj X),
-  map      := λ _ _ f, G.map (F.map f),
+{ obj      := λ X, G (F X),
+  map'      := λ _ _ f, G.map (F.map f),
   map_id   := begin /- `obviously'` says: -/ intros, simp end,
   map_comp := begin /- `obviously'` says: -/ intros, simp end }
 
 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) : (F ⋙ G).map f = G.map (F.map f) := 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
 
 end functor

category_theory/functor_category.lean

@@ -16,7 +16,8 @@ open nat_trans
 Notice that if `C` and `D` are both small categories at the same universe level, this is another small category at that 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) :=
+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) :=
 { hom     := λ F G, F ⟹ G,
   id      := λ F, nat_trans.id F,
   comp    := λ _ _ _ α β, α ⊟ β,
@@ -31,18 +32,24 @@ variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟
 include 𝒞 𝒟
 
 @[simp, ematch] lemma id_app (F : C ↝ D) (X : C) : (𝟙 F : F ⟹ F) X = 𝟙 (F X) := rfl
-@[simp, ematch] lemma comp_app {F G H : C ↝ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : ((α ≫ β) : F ⟹ H) X = (α : F ⟹ G) X ≫ (β : G ⟹ H) X := rfl
+@[simp, ematch] 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
 
 namespace nat_trans
--- This section gives two lemmas about natural transformations between functors into functor categories, spelling them out in components.
+-- This section gives two lemmas about natural transformations between functors into functor categories,
+-- spelling them out in components.
 
-variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D] {E : Type u₃} [ℰ : category.{u₃ v₃} E]
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] 
+          {D : Type u₂} [𝒟 : category.{u₂ v₂} D] 
+          {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include 𝒞 𝒟 ℰ
 
-@[ematch] 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
+@[ematch] 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
 
-@[ematch] 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
+@[ematch] 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/natural_transformation.lean

@@ -33,9 +33,6 @@ 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)
 
-restate_axiom nat_trans.naturality
-attribute [ematch] nat_trans.naturality_lemma
-
 infixr ` ⟹ `:50  := nat_trans             -- type as \==> or ⟹
 
 namespace nat_trans
@@ -44,12 +41,20 @@ instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
 { F   := λ α, Π X : C, (F X) ⟶ (G X),
   coe := λ α, α.app }
 
-@[simp] lemma coe_def {F G : C ↝ D} (α : F ⟹ G) (X : C) : α X = α.app X := rfl
+@[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 
+
+@[ematch] lemma naturality_lemma {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),
-  naturality := begin /- `obviously'` says: -/ intros, dsimp, simp end }
+  naturality := begin /- `obviously'` says: -/ intros, simp end }
 
 @[simp] lemma id_app (F : C ↝ D) (X : C) : (nat_trans.id F) X = 𝟙 (F X) := rfl
 
@@ -76,7 +81,8 @@ def vcomp (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H :=
 notation α `⊟` β:80 := vcomp α β
 
 @[simp] lemma vcomp_app (α : F ⟹ G) (β : G ⟹ H) (X : C) : (α ⊟ β) X = (α X) ≫ (β X) := rfl
-@[ematch] lemma vcomp_assoc (α : F ⟹ G) (β : G ⟹ H) (γ : H ⟹ I) : (α ⊟ β) ⊟ γ = (α ⊟ (β ⊟ γ)) := begin ext, intros, dsimp, rw [assoc] end
+@[ematch] lemma vcomp_assoc (α : F ⟹ G) (β : G ⟹ H) (γ : H ⟹ I) : (α ⊟ β) ⊟ γ = (α ⊟ (β ⊟ γ)) := 
+begin ext, intros, dsimp, rw [assoc] end
 end
 
 variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
@@ -97,11 +103,13 @@ 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) : (α ◫ β) X = (β (F X)) ≫ (I.map (α X)) := rfl
+@[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
 
-@[ematch] lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) :=
+@[ematch] lemma exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : 
+  ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) :=
 begin
   -- `obviously'` says:
   ext,

category_theory/opposites.lean

@@ -33,9 +33,9 @@ include 𝒟
 
 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 }
+  map'     := λ X Y f, F.map f,
+  map_id   := begin /- `obviously'` says: -/ intros, erw [map_id_lemma], refl, end,
+  map_comp := begin /- `obviously'` says: -/ intros, erw [map_comp_lemma], 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
@@ -46,7 +46,7 @@ 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₁) := 
 { obj      := λ p, @category.hom C _ p.1 p.2,
-  map      := λ X Y f, λ h, f.1 ≫ h ≫ f.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_lemma] end,
   map_comp := begin /- `obviously'` says: -/ intros, ext, intros, cases f, cases g, cases X, cases Y, cases Z, dsimp at *, simp, erw [category.assoc] end }
 

category_theory/products.lean

@@ -43,28 +43,28 @@ namespace prod
 /-- `inl C Z` is the functor `X ↦ (X, Z)`. -/
 def inl (C : Type u₁) [category.{u₁ v₁} C] {D : Type u₁} [category.{u₁ v₁} D] (Z : D) : C ↝ (C × D) :=
 { obj      := λ X, (X, Z),
-  map      := λ X Y f, (f, 𝟙 Z),
+  map'     := λ X Y f, (f, 𝟙 Z),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
 /-- `inr D Z` is the functor `X ↦ (Z, X)`. -/
 def inr {C : Type u₁} [category.{u₁ v₁} C] (D : Type u₁) [category.{u₁ v₁} D] (Z : C) : D ↝ (C × D) :=
 { obj      := λ X, (Z, X),
-  map      := λ X Y f, (𝟙 Z, f),
+  map'     := λ X Y f, (𝟙 Z, f),
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, dsimp, simp end }
 
 /-- `fst` is the functor `(X, Y) ↦ X`. -/
 def fst (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ C :=
 { obj      := λ X, X.1,
-  map      := λ X Y f, f.1,
+  map'     := λ X Y f, f.1,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
 /-- `snd` is the functor `(X, Y) ↦ Y`. -/
 def snd (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [category.{u₁ v₁} D] : (C × D) ↝ D :=
 { obj      := λ X, X.2,
-  map      := λ X Y f, f.2,
+  map'     := λ X Y f, f.2,
   map_id   := begin /- `obviously'` says: -/ intros, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }
 
@@ -76,8 +76,8 @@ include 𝒜 ℬ 𝒞 𝒟
 namespace functor
 /-- The cartesian product of two functors. -/
 def prod (F : A ↝ B) (G : C ↝ D) : (A × C) ↝ (B × D) :=
-{ obj := λ X, (F X.1, G X.2),
-  map := λ _ _ f, (F.map f.1, G.map f.2),
+{ obj  := λ X, (F X.1, G X.2),
+  map' := λ _ _ f, (F.map f.1, G.map f.2),
   map_id   := begin /- `obviously'` says: -/ intros, cases X, dsimp, rw map_id_lemma, rw map_id_lemma end,
   map_comp := begin /- `obviously'` says: -/ intros, cases Z, cases Y, cases X, cases f, cases g, dsimp at *, rw map_comp_lemma, rw map_comp_lemma end }
 

category_theory/types.lean

@@ -44,7 +44,7 @@ end functor_to_types
 
 definition ulift : (Type u) ↝ (Type (max u v)) := 
 { obj      := λ X, ulift.{v} X,
-  map      := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down),
+  map'     := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down),
   map_id   := begin /- `obviously'` says: -/ intros, ext, refl end,
   map_comp := begin /- `obviously'` says: -/ intros, refl end }