docs(category_theory): provide missing module docs (#9352)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/category_theory/endomorphism.lean

@@ -2,12 +2,19 @@
 Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
-
-Definition and basic properties of endomorphisms and automorphisms of an object in a category.
 -/
 import category_theory.groupoid
 import data.equiv.mul_add
 
+/-!
+# Endomorphisms
+
+Definition and basic properties of endomorphisms and automorphisms of an object in a category.
+
+For each `X : C`, we provide `End X := X ⟶ X` with a monoid structure,
+and `Aut X := X ≅ X ` with a group structure.
+-/
+
 universes v v' u u'
 
 namespace category_theory

src/category_theory/epi_mono.lean

@@ -2,15 +2,17 @@
 Copyright (c) 2019 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Scott Morrison
+-/
+import category_theory.adjunction.basic
+import category_theory.opposites
+import category_theory.groupoid
 
-Facts about epimorphisms and monomorphisms.
+/-!
+# Facts about epimorphisms and monomorphisms.
 
 The definitions of `epi` and `mono` are in `category_theory.category`,
 since they are used by some lemmas for `iso`, which is used everywhere.
 -/
-import category_theory.adjunction.basic
-import category_theory.opposites
-import category_theory.groupoid
 
 universes v₁ v₂ u₁ u₂
 

src/category_theory/eq_to_hom.lean

@@ -5,6 +5,25 @@ Authors: Reid Barton, Scott Morrison
 -/
 import category_theory.opposites
 
+/-!
+# Morphisms from equations between objects.
+
+When working categorically, sometimes one encounters an equation `h : X = Y` between objects.
+
+Your initial aversion to this is natural and appropriate:
+you're in for some trouble, and if there is another way to approach the problem that won't
+rely on this equality, it may be worth pursuing.
+
+You have two options:
+1. Use the equality `h` as one normally would in Lean (e.g. using `rw` and `subst`).
+   This may immediately cause difficulties, because in category theory everything is dependently
+   typed, and equations between objects quickly lead to nasty goals with `eq.rec`.
+2. Promote `h` to a morphism using `eq_to_hom h : X ⟶ Y`, or `eq_to_iso h : X ≅ Y`.
+
+This file introduces various `simp` lemmas which in favourable circumstances
+result in the various `eq_to_hom` morphisms to drop out at the appropriate moment!
+-/
+
 universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
@@ -52,7 +71,7 @@ lemma congr_arg_mpr_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
 by { cases q, simp, }
 
 /--
-An equality `X = Y` gives us a morphism `X ⟶ Y`.
+An equality `X = Y` gives us an isomorphism `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.

src/category_theory/functor.lean

@@ -2,18 +2,19 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison
+-/
+import tactic.reassoc_axiom
+import tactic.monotonicity
 
-Defines a functor between categories.
+/-!
+# Functors
 
-(As it is a 'bundled' object rather than the `is_functorial` typeclass parametrised
-by the underlying function on objects, the name is capitalised.)
+Defines a functor between categories, extending a `prefunctor` between quivers.
 
-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.)
+Introduces notation `C ⥤ D` for the type of all functors from `C` to `D`.
+(Unfortunately the `⇒` arrow (`\functor`) is taken by core, 
+but in mathlib4 we should switch to this.)
 -/
-import tactic.reassoc_axiom
-import tactic.monotonicity
 
 namespace category_theory
 

src/category_theory/functor_category.lean

@@ -5,6 +5,19 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.natural_transformation
 
+/-!
+# The category of functors and natural transformations between two fixed categories.
+
+We provide the category instance on `C ⥤ D`, with morphisms the natural transformations.
+
+## Universes
+
+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.
+-/
+
 namespace category_theory
 
 -- declare the `v`'s first; see `category_theory.category` for an explanation

src/category_theory/groupoid.lean

@@ -5,6 +5,26 @@ Authors: Reid Barton, Scott Morrison, David Wärn
 -/
 import category_theory.full_subcategory
 
+/-!
+# Groupoids
+
+We define `groupoid` as a typeclass extending `category`,
+asserting that all morphisms have inverses.
+
+The instance `is_iso.of_groupoid (f : X ⟶ Y) : is_iso f` means that you can then write
+`inv f` to access the inverse of any morphism `f`.
+
+`groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y)` provides the equivalence between
+isomorphisms and morphisms in a groupoid.
+
+We provide a (non-instance) constructor `groupoid.of_is_iso` from an existing category
+with `is_iso f` for every `f`.
+
+## See also
+
+See also `category_theory.core` for the groupoid of isomorphisms in a category.
+-/
+
 namespace category_theory
 
 universes v v₂ u u₂ -- morphism levels before object levels. See note [category_theory universes].

src/category_theory/natural_transformation.lean

@@ -2,16 +2,32 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
+-/
+import category_theory.functor
+
+/-!
+# Natural transformations
 
 Defines natural transformations between functors.
 
+A natural transformation `α : nat_trans F G` consists of morphisms `α.app X : F.obj X ⟶ G.obj X`,
+and the naturality squares `α.naturality f : F.map f ≫ α.app Y = α.app X ≫ G.map f`,
+where `f : X ⟶ Y`.
+
+Note that we make `nat_trans.naturality` a simp lemma, with the preferred simp normal form
+pushing components of natural transformations to the left.
+
+See also `category_theory.functor_category`, where we provide the category structure on
+functors and natural transformations.
+
 Introduces notations
-  `τ.app X` for the components of natural transformations,
-  `F ⟶ G` for the type of natural transformations between functors `F` and `G`,
-  `σ ≫ τ` for vertical compositions, and
-  `σ ◫ τ` for horizontal compositions.
+* `τ.app X` for the components of natural transformations,
+* `F ⟶ G` for the type of natural transformations between functors `F` and `G`
+  (this and the next require `category_theory.functor_category`),
+* `σ ≫ τ` for vertical compositions, and
+* `σ ◫ τ` for horizontal compositions.
+
 -/
-import category_theory.functor
 
 namespace category_theory
 
@@ -29,8 +45,8 @@ Naturality is expressed by `α.naturality_lemma`.
 -/
 @[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)
+(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)
 
 restate_axiom nat_trans.naturality'
 -- Rather arbitrarily, we say that the 'simpler' form is

src/category_theory/opposites.lean

@@ -6,6 +6,22 @@ Authors: Stephen Morgan, Scott Morrison
 import category_theory.types
 import category_theory.equivalence
 
+/-!
+# Opposite categories
+
+We provide a category instance on `Cᵒᵖ`.
+The morphisms `X ⟶ Y` are defined to be the morphisms `unop Y ⟶ unop X` in `C`.
+
+Here `Cᵒᵖ` is an irreducible typeclass synonym for `C`
+(it is the same one used in the algebra library).
+
+We also provide various mechanisms for constructing opposite morphisms, functors,
+and natural transformations.
+
+Unfortunately, because we do not have a definitional equality `op (op X) = X`,
+there are quite a few variations that are needed in practice.
+-/
+
 universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 open opposite

src/category_theory/whiskering.lean

@@ -5,6 +5,27 @@ Authors: Scott Morrison
 -/
 import category_theory.natural_isomorphism
 
+/-!
+# Whiskering
+
+Given a functor `F  : C ⥤ D` and functors `G H : D ⥤ E` and a natural transformation `α : G ⟶ H`,
+we can construct a new natural transformation `F ⋙ G ⟶ F ⋙ H`,
+called `whisker_left F α`. This is the same as the horizontal composition of `𝟙 F` with `α`.
+
+This operation is functorial in `F`, and we package this as `whiskering_left`. Here
+`(whiskering_lift.obj F).obj G` is `F ⋙ G`, and
+`(whiskering_lift.obj F).map α` is `whisker_left F α`.
+(That is, we might have alternatively named this as the "left composition functor".)
+
+We also provide analogues for composition on the right, and for these operations on isomorphisms.
+
+At the end of the file, we provide the left and right unitors, and the associator,
+for functor composition.
+(In fact functor composition is definitionally associative, but very often relying on this causes
+extremely slow elaboration, so it is better to insert it explicitly.)
+We also show these natural isomorphisms satisfy the triangle and pentagon identities.
+-/
+
 namespace category_theory
 
 universes u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄