refactor(category_theory): rename functor.on_iso to functor.map_iso (#893)

* feat(category_theory): functor.map_nat_iso

* define `functor.map_nat_iso`, and relate to whiskering
* rename `functor.on_iso` to `functor.map_iso`
* add some missing lemmas about whiskering

* some more missing whiskering lemmas, while we're at it

* removing map_nat_iso

Author: kim-em

src/category_theory/eq_to_hom.lean

@@ -68,7 +68,7 @@ end functor
 by cases p; simp
 
 @[simp] lemma eq_to_iso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
-  F.on_iso (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
+  F.map_iso (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
 by ext; cases p; simp
 
 @[simp] lemma eq_to_hom_app {F G : C ⥤ D} (h : F = G) (X : C) :

src/category_theory/equivalence.lean

@@ -61,14 +61,14 @@ include ℰ
   (e.inverse).obj ((f.inverse).obj ((f.functor).obj ((e.functor).obj X))) ≅ X :=
 calc
   (e.inverse).obj ((f.inverse).obj ((f.functor).obj ((e.functor).obj X)))
-    ≅ (e.inverse).obj ((e.functor).obj X) : e.inverse.on_iso (nat_iso.app f.fun_inv_id _)
+    ≅ (e.inverse).obj ((e.functor).obj X) : e.inverse.map_iso (nat_iso.app f.fun_inv_id _)
 ... ≅ X                                   : nat_iso.app e.fun_inv_id _
 
 @[simp] private def feef_iso_id (e : C ≌ D) (f : D ≌ E) (X : E) :
   (f.functor).obj ((e.functor).obj ((e.inverse).obj ((f.inverse).obj X))) ≅ X :=
 calc
   (f.functor).obj ((e.functor).obj ((e.inverse).obj ((f.inverse).obj X)))
-    ≅ (f.functor).obj ((f.inverse).obj X) : f.functor.on_iso (nat_iso.app e.inv_fun_id _)
+    ≅ (f.functor).obj ((f.inverse).obj X) : f.functor.map_iso (nat_iso.app e.inv_fun_id _)
 ... ≅ X                                   : nat_iso.app f.inv_fun_id _
 
 @[trans] def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E :=

src/category_theory/isomorphism.lean

@@ -48,6 +48,10 @@ calc α.inv
 @[simp] lemma symm_hom (α : X ≅ Y) : α.symm.hom = α.inv := rfl
 @[simp] lemma symm_inv (α : X ≅ Y) : α.symm.inv = α.hom := rfl
 
+@[simp] lemma symm_mk {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
+  iso.symm {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id} =
+    {hom := inv, inv := hom, hom_inv_id' := inv_hom_id, inv_hom_id' := hom_inv_id} := rfl
+
 @[refl] def refl (X : C) : X ≅ X :=
 { hom := 𝟙 X,
   inv := 𝟙 X }
@@ -64,6 +68,15 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
 @[simp] lemma trans_hom (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).hom = α.hom ≫ β.hom := rfl
 @[simp] lemma trans_inv (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
 
+@[simp] lemma trans_mk {X Y Z : C}
+  (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id)
+  (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id') (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
+  iso.trans
+    {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id}
+    {hom := hom', inv := inv', hom_inv_id' := hom_inv_id', inv_hom_id' := inv_hom_id'} =
+  {hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''} :=
+rfl
+
 @[simp] lemma refl_symm (X : C) : (iso.refl X).hom = 𝟙 X := rfl
 @[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
 
@@ -132,14 +145,14 @@ variables {D : Sort u₂}
 variables [𝒟 : category.{v₂} D]
 include 𝒟
 
-def on_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y :=
+def map_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y :=
 { hom := F.map i.hom,
   inv := F.map i.inv,
   hom_inv_id' := by rw [←map_comp, iso.hom_inv_id, ←map_id],
   inv_hom_id' := by rw [←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).hom = F.map i.hom := rfl
-@[simp] lemma on_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.on_iso i).inv = F.map i.inv := rfl
+@[simp] lemma map_iso_hom (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).hom = F.map i.hom := rfl
+@[simp] lemma map_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).inv = F.map i.inv := rfl
 
 instance (F : C ⥤ D) (f : X ⟶ Y) [is_iso f] : is_iso (F.map f) :=
 { inv := F.map (inv f),

src/category_theory/limits/preserves.lean

@@ -126,13 +126,13 @@ end
   then it preserves any limit cone for K. -/
 def preserves_limit_of_preserves_limit_cone {F : C ⥤ D} {t : cone K}
   (h : is_limit t) (hF : is_limit (F.map_cone t)) : preserves_limit K F :=
-⟨λ t' h', is_limit.of_iso_limit hF (functor.on_iso _ (is_limit.unique h h'))⟩
+⟨λ t' h', is_limit.of_iso_limit hF (functor.map_iso _ (is_limit.unique h h'))⟩
 
 /-- If F preserves one colimit cocone for the diagram K,
   then it preserves any colimit cocone for K. -/
 def preserves_colimit_of_preserves_colimit_cocone {F : C ⥤ D} {t : cocone K}
   (h : is_colimit t) (hF : is_colimit (F.map_cocone t)) : preserves_colimit K F :=
-⟨λ t' h', is_colimit.of_iso_colimit hF (functor.on_iso _ (is_colimit.unique h h'))⟩
+⟨λ t' h', is_colimit.of_iso_colimit hF (functor.map_iso _ (is_colimit.unique h h'))⟩
 
 /-
 A functor F : C → D reflects limits if whenever the image of a cone

src/category_theory/natural_isomorphism.lean

@@ -4,12 +4,13 @@
 
 import category_theory.isomorphism
 import category_theory.functor_category
+import category_theory.whiskering
 
 open category_theory
 
-namespace category_theory.nat_iso
+universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+namespace category_theory.nat_iso
 
 variables {C : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
@@ -92,9 +93,9 @@ by tidy
 
 end category_theory.nat_iso
 
-namespace category_theory.functor
+open category_theory
 
-universes u₁ u₂ v₁ v₂
+namespace category_theory.functor
 
 section
 variables {C : Sort u₁} [𝒞 : category.{v₁} C]
@@ -108,7 +109,7 @@ include 𝒞 𝒟
 { hom := { app := λ X, 𝟙 (F.obj X) },
   inv := { app := λ X, 𝟙 (F.obj X) } }
 
-universes u₃ v₃ u₄ v₄
+universes v₄ u₄
 
 variables {A : Sort u₃} [𝒜 : category.{v₃} A]
           {B : Sort u₄} [ℬ : category.{v₄} B]

src/category_theory/whiskering.lean

@@ -45,24 +45,50 @@ variables {C} {D} {E}
 def whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟹ H) : (F ⋙ G) ⟹ (F ⋙ H) :=
 ((whiskering_left C D E).obj F).map α
 
+@[simp] lemma whiskering_left_obj_obj (F : C ⥤ D) (G : D ⥤ E) :
+  ((whiskering_left C D E).obj F).obj G = F ⋙ G :=
+rfl
+@[simp] lemma whiskering_left_obj_map (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟹ H) :
+  ((whiskering_left C D E).obj F).map α = whisker_left F α :=
+rfl
+@[simp] lemma whiskering_left_map_app_app {F G : C ⥤ D} (τ : F ⟹ G) (H : D ⥤ E) (c) :
+  (((whiskering_left C D E).map τ).app H).app c = H.map (τ.app c) :=
+rfl
+
 @[simp] lemma whisker_left.app (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟹ H) (X : C) :
   (whisker_left F α).app X = α.app (F.obj X) :=
 rfl
 
 def whisker_right {G H : C ⥤ D} (α : G ⟹ H) (F : D ⥤ E) : (G ⋙ F) ⟹ (H ⋙ F) :=
 ((whiskering_right C D E).obj F).map α
 
+@[simp] lemma whiskering_right_obj_obj (G : C ⥤ D) (F : D ⥤ E) :
+  ((whiskering_right C D E).obj F).obj G = G ⋙ F :=
+rfl
+@[simp] lemma whiskering_right_obj_map {G H : C ⥤ D} (α : G ⟹ H) (F : D ⥤ E) :
+  ((whiskering_right C D E).obj F).map α = whisker_right α F :=
+rfl
+@[simp] lemma whiskering_right_map_app_app (F : C ⥤ D) {G H : D ⥤ E} (τ : G ⟹ H) (c) :
+  (((whiskering_right C D E).map τ).app F).app c = τ.app (F.obj c) :=
+rfl
+
 @[simp] lemma whisker_right.app {G H : C ⥤ D} (α : G ⟹ H) (F : D ⥤ E) (X : C) :
    (whisker_right α F).app X = F.map (α.app X) :=
 rfl
 
 @[simp] lemma whisker_left_id (F : C ⥤ D) {G : D ⥤ E} :
   whisker_left F (nat_trans.id G) = nat_trans.id (F.comp G) :=
 rfl
+@[simp] lemma whisker_left_id' (F : C ⥤ D) {G : D ⥤ E} :
+  whisker_left F (𝟙 G) = 𝟙 (F.comp G) :=
+rfl
 
 @[simp] lemma whisker_right_id {G : C ⥤ D} (F : D ⥤ E) :
   whisker_right (nat_trans.id G) F = nat_trans.id (G.comp F) :=
 ((whiskering_right C D E).obj F).map_id _
+@[simp] lemma whisker_right_id' {G : C ⥤ D} (F : D ⥤ E) :
+  whisker_right (𝟙 G) F = 𝟙 (G.comp F) :=
+((whiskering_right C D E).obj F).map_id _
 
 @[simp] lemma whisker_left_vcomp (F : C ⥤ D) {G H K : D ⥤ E} (α : G ⟹ H) (β : H ⟹ K) :
   whisker_left F (α ⊟ β) = (whisker_left F α) ⊟ (whisker_left F β) :=