chore(category/*): linting (#3178)

Some linting work on `category_theory/`.



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

src/algebra/category/Group/basic.lean

@@ -97,9 +97,12 @@ namespace CommGroup
 @[to_additive]
 instance : bundled_hom.parent_projection comm_group.to_group := ⟨⟩
 
-/-- Construct a bundled CommGroup from the underlying type and typeclass. -/
+/-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G
 
+/-- Construct a bundled `AddCommGroup` from the underlying type and typeclass. -/
+add_decl_doc AddCommGroup.of
+
 local attribute [reducible] CommGroup
 
 @[to_additive]

src/category_theory/category/Cat.lean

@@ -8,9 +8,9 @@ import category_theory.concrete_category
 /-!
 # 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.
+This file contains the definition of the category `Cat` of all categories.
+In this category objects are categories and
+morphisms are functors between these categories.
 
 ## Implementation notes
 
@@ -27,6 +27,8 @@ def Cat := bundled category.{v u}
 
 namespace Cat
 
+instance : inhabited Cat := ⟨⟨Type u, category_theory.types⟩⟩
+
 instance str (C : Cat.{v u}) : category.{v u} C.α := C.str
 
 /-- Construct a bundled `Cat` from the underlying type and the typeclass. -/

src/category_theory/concrete_category/bundled.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather
 Bundled types.
 -/
 import tactic.doc_commands
+import tactic.lint
 
 /-!
 `bundled c` provides a uniform structure for bundling a type equipped with a type class.
@@ -22,6 +23,7 @@ variables {c d : Type u → Type v} {α : Type u}
 
 /-- `bundled` is a type bundled with a type class instance for that type. Only
 the type class is exposed as a parameter. -/
+@[nolint has_inhabited_instance]
 structure bundled (c : Type u → Type v) : Type (max (u+1) v) :=
 (α : Type u)
 (str : c α . tactic.apply_instance)

src/category_theory/conj.lean

@@ -25,7 +25,7 @@ namespace iso
 variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
-/- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
+/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
 there is a natural bijection between `X ⟶ Y` and `X₁ ⟶ Y₁`. See also `equiv.arrow_congr`. -/
 def hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) :
   (X ⟶ Y) ≃ (X₁ ⟶ Y₁) :=

src/category_theory/const.lean

@@ -14,6 +14,9 @@ namespace category_theory.functor
 variables (J : Type u₁) [category.{v₁} J]
 variables {C : Type u₂} [category.{v₂} C]
 
+/--
+The functor sending `X : C` to the constant functor `J ⥤ C` sending everything to `X`.
+-/
 def const : C ⥤ (J ⥤ C) :=
 { obj := λ X,
   { obj := λ j, X,
@@ -29,6 +32,10 @@ variables {J}
 @[simp] lemma obj_map (X : C) {j j' : J} (f : j ⟶ j') : ((const J).obj X).map f = 𝟙 X := rfl
 @[simp] lemma map_app {X Y : C} (f : X ⟶ Y) (j : J) : ((const J).map f).app j = f := rfl
 
+/--
+The contant functor `Jᵒᵖ ⥤ Cᵒᵖ` sending everything to `op X`
+is (naturally isomorphic to) the opposite of the constant functor `J ⥤ C` sending everything to `X`.
+-/
 def op_obj_op (X : C) :
   (const Jᵒᵖ).obj (op X) ≅ ((const J).obj X).op :=
 { hom := { app := λ j, 𝟙 _ },
@@ -37,14 +44,21 @@ def op_obj_op (X : C) :
 @[simp] lemma op_obj_op_hom_app (X : C) (j : Jᵒᵖ) : (op_obj_op X).hom.app j = 𝟙 _ := rfl
 @[simp] lemma op_obj_op_inv_app (X : C) (j : Jᵒᵖ) : (op_obj_op X).inv.app j = 𝟙 _ := rfl
 
+/--
+The contant functor `Jᵒᵖ ⥤ C` sending everything to `unop X`
+is (naturally isomorphic to) the opposite of
+the constant functor `J ⥤ Cᵒᵖ` sending everything to `X`.
+-/
 def op_obj_unop (X : Cᵒᵖ) :
   (const Jᵒᵖ).obj (unop X) ≅ ((const J).obj X).left_op :=
 { hom := { app := λ j, 𝟙 _ },
   inv := { app := λ j, 𝟙 _ } }
 
 -- Lean needs some help with universes here.
-@[simp] lemma op_obj_unop_hom_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).hom.app j = 𝟙 _ := rfl
-@[simp] lemma op_obj_unop_inv_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).inv.app j = 𝟙 _ := rfl
+@[simp] lemma op_obj_unop_hom_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).hom.app j = 𝟙 _ :=
+rfl
+@[simp] lemma op_obj_unop_inv_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (op_obj_unop.{v₁ v₂} X).inv.app j = 𝟙 _ :=
+rfl
 
 @[simp] lemma unop_functor_op_obj_map (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) :
   (unop ((functor.op (const J)).obj X)).map f = 𝟙 (unop X) := rfl

src/category_theory/core.lean

@@ -13,6 +13,7 @@ universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.c
 
 /-- The core of a category C is the groupoid whose morphisms are all the
 isomorphisms of C. -/
+@[nolint has_inhabited_instance]
 def core (C : Type u₁) := C
 
 variables {C : Type u₁} [category.{v₁} C]
@@ -42,6 +43,10 @@ def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 { obj := λ X, F.obj X,
   map := λ X Y f, ⟨F.map f, F.map (inv f)⟩ }
 
+/--
+We can functorially associate to any functor from a groupoid to the core of a category `C`,
+a functor from the groupoid to `C`, simply by composing with the embedding `core C ⥤ C`.
+-/
 def forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj inclusion
 end core
 

src/category_theory/currying.lean

@@ -13,6 +13,9 @@ variables {C : Type u₁} [category.{v₁} C]
           {D : Type u₂} [category.{v₂} D]
           {E : Type u₃} [category.{v₃} E]
 
+/--
+The uncurrying functor, taking a functor `C ⥤ (D ⥤ E)` and producing a functor `(C × D) ⥤ E`.
+-/
 def uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E) :=
 { obj := λ F,
   { obj := λ X, (F.obj X.1).obj X.2,
@@ -38,12 +41,18 @@ def uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E) :=
       rw category.assoc,
     end } }.
 
+/--
+The object level part of the currying functor. (See `curry` for the functorial version.)
+-/
 def curry_obj (F : (C × D) ⥤ E) : C ⥤ (D ⥤ E) :=
 { obj := λ X,
     { obj := λ Y, F.obj (X, Y),
       map := λ Y Y' g, F.map (𝟙 X, g) },
     map := λ X X' f, { app := λ Y, F.map (f, 𝟙 Y) } }
 
+/--
+The currying functor, taking a functor `(C × D) ⥤ E` and producing a functor `C ⥤ (D ⥤ E)`.
+-/
 def curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) :=
 { obj := λ F, curry_obj F,
   map := λ F G T,
@@ -77,6 +86,9 @@ def curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) :=
 @[simp] lemma curry.map_app_app {F G : (C × D) ⥤ E} {α : F ⟶ G} {X} {Y} :
   ((curry.map α).app X).app Y = α.app (X, Y) := rfl
 
+/--
+The equivalence of functor categories given by currying/uncurrying.
+-/
 def currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E) :=
 equivalence.mk uncurry curry
   (nat_iso.of_components (λ F, nat_iso.of_components

src/category_theory/elements.lean

@@ -33,7 +33,11 @@ universes w v u
 variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
-/-- The type of objects for the category of elements of a functor `F : C ⥤ Type` is a pair `(X : C, x : F.obj X)`. -/
+/--
+The type of objects for the category of elements of a functor `F : C ⥤ Type`
+is a pair `(X : C, x : F.obj X)`.
+-/
+@[nolint has_inhabited_instance]
 def functor.elements (F : C ⥤ Type w) := (Σ c : C, F.obj c)
 
 /-- The category structure on `F.elements`, for `F : C ⥤ Type`.

src/category_theory/eq_to_hom.lean

@@ -12,13 +12,25 @@ open opposite
 
 variables {C : Type u} [category.{v} C]
 
+/--
+An equality `X = Y` gives us a morphism `X ⟶ Y`.
+
+It is typically better to use this, rather than rewriting by the equality then using `𝟙 _`
+which usually leads to dependent type theory hell.
+-/
 def eq_to_hom {X Y : C} (p : X = Y) : X ⟶ Y := by rw p; exact 𝟙 _
 
 @[simp] lemma eq_to_hom_refl (X : C) (p : X = X) : eq_to_hom p = 𝟙 X := rfl
 @[simp, reassoc] lemma eq_to_hom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
   eq_to_hom p ≫ eq_to_hom q = eq_to_hom (p.trans q) :=
 by cases p; cases q; simp
 
+/--
+An equality `X = Y` gives us a morphism `X ⟶ Y`.
+
+It is typically better to use this, rather than rewriting by the equality then using `iso.refl _`
+which usually leads to dependent type theory hell.
+-/
 def eq_to_iso {X Y : C} (p : X = Y) : X ≅ Y :=
 ⟨eq_to_hom p, eq_to_hom p.symm, by simp, by simp⟩
 

src/category_theory/full_subcategory.lean

@@ -43,6 +43,12 @@ variables {C : Type u₁} (D : Type u₂) [category.{v} D]
 variables (F : C → D)
 include F
 
+/--
+`induced_category D F`, where `F : C → D`, is a typeclass synonym for `C`,
+which provides a category structure so that the morphisms `X ⟶ Y` are the morphisms
+in `D` from `F X` to `F Y`.
+-/
+@[nolint has_inhabited_instance unused_arguments]
 def induced_category : Type u₁ := C
 
 variables {D}
@@ -56,6 +62,10 @@ instance induced_category.category : category.{v} (induced_category D F) :=
   id   := λ X, 𝟙 (F X),
   comp := λ _ _ _ f g, f ≫ g }
 
+/--
+The forgetful functor from an induced category to the original category,
+forgetting the extra data.
+-/
 @[simps] def induced_functor : induced_category D F ⥤ D :=
 { obj := F, map := λ x y f, f }
 
@@ -81,6 +91,10 @@ variables (Z : C → Prop)
 instance full_subcategory : category.{v} {X : C // Z X} :=
 induced_category.category subtype.val
 
+/--
+The forgetful functor from a full subcategory into the original category
+("forgetting" the condition).
+-/
 def full_subcategory_inclusion : {X : C // Z X} ⥤ C :=
 induced_functor subtype.val
 

src/category_theory/fully_faithful.lean

@@ -69,6 +69,11 @@ def preimage_iso (f : (F.obj X) ≅ (F.obj Y)) : X ≅ Y :=
 by tidy
 
 variables (F)
+
+/--
+If the image of a morphism under a fully faithful functor in an isomorphism,
+then the original morphisms is also an isomorphism.
+-/
 def is_iso_of_fully_faithful (f : X ⟶ Y) [is_iso (F.map f)] : is_iso f :=
 { inv := F.preimage (inv (F.map f)),
   hom_inv_id' := F.map_injective (by simp),

src/category_theory/functor.lean

@@ -55,6 +55,8 @@ protected def id : C ⥤ C :=
 
 notation `𝟭` := functor.id
 
+instance : inhabited (C ⥤ C) := ⟨functor.id C⟩
+
 variable {C}
 
 @[simp] lemma id_obj (X : C) : (𝟭 C).obj X = X := rfl
@@ -87,19 +89,6 @@ protected lemma id_comp (F : C ⥤ D) : (𝟭 C) ⋙ F = F := by cases F; refl
 
 end
 
-section
-variables (C : Type u₁) [category.{v₁} C]
-
-@[simp] def ulift_down : (ulift.{u₂} C) ⥤ C :=
-{ obj := λ X, X.down,
-  map := λ X Y f, f }
-
-@[simp] def ulift_up : C ⥤ (ulift.{u₂} C) :=
-{ obj := λ X, ⟨ X ⟩,
-  map := λ X Y f, f }
-
-end
-
 end functor
 
 end category_theory

src/category_theory/functor_category.lean

@@ -78,6 +78,7 @@ end nat_trans
 open nat_trans
 namespace functor
 
+/-- Flip the arguments of a bifunctor. See also `currying.lean`. -/
 protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
 { obj := λ k,
   { obj := λ j, (F.obj j).obj k,

src/category_theory/isomorphism.lean

@@ -88,6 +88,8 @@ by cases α; refl
 { hom := 𝟙 X,
   inv := 𝟙 X }
 
+instance : inhabited (X ≅ X) := ⟨iso.refl X⟩
+
 @[simp] lemma refl_symm (X : C) : (iso.refl X).symm = iso.refl X := rfl
 
 /-- Composition of two isomorphisms -/

src/category_theory/natural_isomorphism.lean

@@ -115,18 +115,4 @@ localized "infix ` ■ `:80 := category_theory.nat_iso.hcomp" in category
 
 end nat_iso
 
-namespace functor
-
-variables {C : Type u₁} [category.{v₁} C]
-
-def ulift_down_up : ulift_down.{v₁} C ⋙ ulift_up C ≅ 𝟭 (ulift.{u₂} C) :=
-{ hom := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X },
-  inv := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X } }
-
-def ulift_up_down : ulift_up.{v₁} C ⋙ ulift_down C ≅ 𝟭 C :=
-{ hom := { app := λ X, 𝟙 X },
-  inv := { app := λ X, 𝟙 X } }
-
-
-end functor
 end category_theory

src/category_theory/natural_transformation.lean

@@ -26,7 +26,8 @@ The field `app` provides the components of the natural transformation.
 
 Naturality is expressed by `α.naturality_lemma`.
 -/
-@[ext] structure nat_trans (F G : C ⥤ D) : Type (max u₁ v₂) :=
+@[ext]
+structure nat_trans (F G : C ⥤ D) : Type (max u₁ v₂) :=
 (app : Π X : C, (F.obj X) ⟶ (G.obj X))
 (naturality' : ∀ {{X Y : C}} (f : X ⟶ Y), (F.map f) ≫ (app Y) = (app X) ≫ (G.map f) . obviously)
 
@@ -43,6 +44,8 @@ protected def id (F : C ⥤ D) : nat_trans F F :=
 
 @[simp] lemma id_app' (F : C ⥤ D) (X : C) : (nat_trans.id F).app X = 𝟙 (F.obj X) := rfl
 
+instance (F : C ⥤ D) : inhabited (nat_trans F F) := ⟨nat_trans.id F⟩
+
 open category
 open category_theory.functor
 

src/category_theory/products/associator.lean

@@ -19,16 +19,25 @@ variables (C : Type u₁) [category.{v₁} C]
           (D : Type u₂) [category.{v₂} D]
           (E : Type u₃) [category.{v₃} E]
 
--- Here and below we specify explicitly the projections to generate `@[simp]` lemmas for, 
+/--
+The associator functor `(C × D) × E ⥤ C × (D × E)`.
+-/
+-- Here and below we specify explicitly the projections to generate `@[simp]` lemmas for,
 -- as the default behaviour of `@[simps]` will generate projections all the way down to components of pairs.
-@[simps obj map] def associator : ((C × D) × E) ⥤ (C × (D × E)) :=
+@[simps obj map] def associator : (C × D) × E ⥤ C × (D × E) :=
 { obj := λ X, (X.1.1, (X.1.2, X.2)),
   map := λ _ _ f, (f.1.1, (f.1.2, f.2)) }
 
-@[simps obj map] def inverse_associator : (C × (D × E)) ⥤ ((C × D) × E) :=
+/--
+The inverse associator functor `C × (D × E) ⥤ (C × D) × E `.
+-/
+@[simps obj map] def inverse_associator : C × (D × E) ⥤ (C × D) × E :=
 { obj := λ X, ((X.1, X.2.1), X.2.2),
   map := λ _ _ f, ((f.1, f.2.1), f.2.2) }
 
+/--
+The equivalence of categories expressing associativity of products of categories.
+-/
 def associativity : (C × D) × E ≌ C × (D × E) :=
 equivalence.mk (associator C D E) (inverse_associator C D E)
   (nat_iso.of_components (λ X, eq_to_iso (by simp)) (by tidy))

src/category_theory/punit.lean

@@ -17,6 +17,7 @@ instance punit_category : small_category punit :=
 namespace functor
 variables {C : Type u} [category.{v} C]
 
+/-- The constant functor sending everything to `punit.start`. -/
 def star : C ⥤ punit.{w+1} := (const C).obj punit.star
 @[simp] lemma star_obj (X : C) : star.obj X = punit.star := rfl
 @[simp] lemma star_map {X Y : C} (f : X ⟶ Y) : star.map f = 𝟙 _ := rfl

src/category_theory/single_obj.lean

@@ -37,6 +37,7 @@ universes u v w
 
 namespace category_theory
 /-- Type tag on `unit` used to define single-object categories and groupoids. -/
+@[nolint unused_arguments has_inhabited_instance]
 def single_obj (α : Type u) : Type := unit
 
 namespace single_obj
@@ -61,6 +62,7 @@ instance groupoid [group α] : groupoid (single_obj α) :=
   inv_comp' := λ _ _, mul_right_inv,
   comp_inv' := λ _ _, mul_left_inv }
 
+/-- The single object in `single_obj α`. -/
 protected def star : single_obj α := unit.star
 
 /-- The endomorphisms monoid of the only object in `single_obj α` is equivalent to the original