lint(category_theory/whiskering): add doc-strings (#4417)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/whiskering.lean

@@ -14,16 +14,30 @@ variables {C : Type u₁} [category.{v₁} C]
           {D : Type u₂} [category.{v₂} D]
           {E : Type u₃} [category.{v₃} E]
 
+/--
+If `α : G ⟶ H` then
+`whisker_left F α : (F ⋙ G) ⟶ (F ⋙ H)` has components `α.app (F.obj X)`.
+-/
 @[simps] def whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : (F ⋙ G) ⟶ (F ⋙ H) :=
-{ app := λ c, α.app (F.obj c),
+{ app := λ X, α.app (F.obj X),
   naturality' := λ X Y f, by rw [functor.comp_map, functor.comp_map, α.naturality] }
 
+/--
+If `α : G ⟶ H` then
+`whisker_right α F : (G ⋙ F) ⟶ (G ⋙ F)` has components `F.map (α.app X)`.
+-/
 @[simps] def whisker_right {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : (G ⋙ F) ⟶ (H ⋙ F) :=
-{ app := λ c, F.map (α.app c),
+{ app := λ X, F.map (α.app X),
   naturality' := λ X Y f, by rw [functor.comp_map, functor.comp_map, ←F.map_comp, ←F.map_comp, α.naturality] }
 
 variables (C D E)
 
+/--
+Left-composition gives a functor `(C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E))`.
+
+`(whiskering_lift.obj F).obj G` is `F ⋙ G`, and
+`(whiskering_lift.obj F).map α` is `whisker_left F α`.
+-/
 @[simps] def whiskering_left : (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)) :=
 { obj := λ F,
   { obj := λ G, F ⋙ G,
@@ -34,6 +48,12 @@ variables (C D E)
       naturality' := λ X Y f, begin dsimp, rw [←H.map_comp, ←H.map_comp, ←τ.naturality] end },
     naturality' := λ X Y f, begin ext, dsimp, rw [f.naturality] end } }
 
+/--
+Right-composition gives a functor `(D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))`.
+
+`(whiskering_right.obj H).obj F` is `F ⋙ H`, and
+`(whiskering_right.obj H).map α` is `whisker_right α H`.
+-/
 @[simps] def whiskering_right : (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)) :=
 { obj := λ H,
   { obj := λ F, F ⋙ H,
@@ -68,6 +88,10 @@ rfl
   whisker_right (α ≫ β) F = (whisker_right α F) ≫ (whisker_right β F) :=
 ((whiskering_right C D E).obj F).map_comp α β
 
+/--
+If `α : G ≅ H` is a natural isomorphism then
+`iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H)` has components `α.app (F.obj X)`.
+-/
 def iso_whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : (F ⋙ G) ≅ (F ⋙ H) :=
 ((whiskering_left C D E).obj F).map_iso α
 @[simp] lemma iso_whisker_left_hom (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
@@ -77,6 +101,10 @@ rfl
   (iso_whisker_left F α).inv = whisker_left F α.inv :=
 rfl
 
+/--
+If `α : G ≅ H` then
+`iso_whisker_right α F : (G ⋙ F) ≅ (G ⋙ F)` has components `F.map_iso (α.app X)`.
+-/
 def iso_whisker_right {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : (G ⋙ F) ≅ (H ⋙ F) :=
 ((whiskering_right C D E).obj F).map_iso α
 @[simp] lemma iso_whisker_right_hom {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
@@ -115,17 +143,29 @@ universes u₅ v₅
 variables {A : Type u₁} [category.{v₁} A]
 variables {B : Type u₂} [category.{v₂} B]
 
-@[simps] def left_unitor (F : A ⥤ B) : ((𝟭 _) ⋙ F) ≅ F :=
+/--
+The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
+-/
+@[simps] def left_unitor (F : A ⥤ B) : ((𝟭 A) ⋙ F) ≅ F :=
 { hom := { app := λ X, 𝟙 (F.obj X) },
   inv := { app := λ X, 𝟙 (F.obj X) } }
 
-@[simps] def right_unitor (F : A ⥤ B) : (F ⋙ (𝟭 _)) ≅ F :=
+/--
+The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
+-/
+@[simps] def right_unitor (F : A ⥤ B) : (F ⋙ (𝟭 B)) ≅ F :=
 { hom := { app := λ X, 𝟙 (F.obj X) },
   inv := { app := λ X, 𝟙 (F.obj X) } }
 
 variables {C : Type u₃} [category.{v₃} C]
 variables {D : Type u₄} [category.{v₄} D]
 
+/--
+The associator for functors, a natural isomorphism `((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H))`.
+
+(In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
+and it's usually best to insert explicit associators.)
+-/
 @[simps] def associator (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) : ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)) :=
 { hom := { app := λ _, 𝟙 _ },
   inv := { app := λ _, 𝟙 _ } }