[Merged by Bors] - doc(category_theory): add doc-strings and links to the stacks project

src/category_theory/adjunction/basic.lean

@@ -25,6 +25,8 @@ there are also constructors `left_adjoint_of_equiv` and `adjunction_of_equiv_lef
 well as their duals) which can be simpler in practice.
 
 Uniqueness of adjoints is shown in `category_theory.adjunction.opposites`.
+
+See https://stacks.math.columbia.edu/tag/0037.
 -/
 structure adjunction (F : C ⥤ D) (G : D ⥤ C) :=
 (hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
@@ -293,7 +295,11 @@ def left_adjoint_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [r : is_left_adjoint F
 section
 variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
 
-/-- Show that adjunctions can be composed. -/
+/--
+Composition of adjunctions.
+
+See https://stacks.math.columbia.edu/tag/0DV0.
+-/
 def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
 { hom_equiv := λ X Z, equiv.trans (adj₂.hom_equiv _ _) (adj₁.hom_equiv _ _),
   unit := adj₁.unit ≫

src/category_theory/adjunction/fully_faithful.lean

@@ -19,9 +19,14 @@ variables {C : Type u₁} [category.{v₁} C]
 variables {D : Type u₂} [category.{v₂} D]
 variables {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R)
 
--- Lemma 4.5.13 from [Riehl][riehl2017]
--- Proof in <https://stacks.math.columbia.edu/tag/0036>
--- or at <https://math.stackexchange.com/a/2727177>
+/--
+If the left adjoint is fully faithful, then the unit is an isomorphism.
+
+See
+* Lemma 4.5.13 from [Riehl][riehl2017]
+* https://math.stackexchange.com/a/2727177
+* https://stacks.math.columbia.edu/tag/07RB (we only prove the forward direction!)
+-/
 instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunction.unit h) :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.unit h) $ λ X,
 @yoneda.is_iso _ _ _ _ ((adjunction.unit h).app X)
@@ -40,6 +45,11 @@ instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunct
     simp,
   end }.
 
+/--
+If the right adjoint is fully faithful, then the counit is an isomorphism.
+
+See https://stacks.math.columbia.edu/tag/07RB (we only prove the forward direction!)
+-/
 instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjunction.counit h) :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.counit h) $ λ X,
 @is_iso_of_op _ _ _ _ _ $

src/category_theory/adjunction/limits.lean

@@ -42,7 +42,11 @@ def functoriality_is_left_adjoint :
   { unit := functoriality_unit adj K,
     counit := functoriality_counit adj K } }
 
-/-- A left adjoint preserves colimits. -/
+/--
+A left adjoint preserves colimits.
+
+See https://stacks.math.columbia.edu/tag/0038.
+-/
 def left_adjoint_preserves_colimits : preserves_colimits F :=
 { preserves_colimits_of_shape := λ J 𝒥,
   { preserves_colimit := λ F,
@@ -97,7 +101,11 @@ def functoriality_is_right_adjoint :
   { unit := functoriality_unit' adj K,
     counit := functoriality_counit' adj K } }
 
-/-- A right adjoint preserves limits. -/
+/--
+A right adjoint preserves limits.
+
+See https://stacks.math.columbia.edu/tag/0038.
+-/
 def right_adjoint_preserves_limits : preserves_limits G :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K,

src/category_theory/category/default.lean

@@ -48,6 +48,8 @@ infixr ` ≫ `:80 := category_struct.comp -- type as \gg
 The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
+
+See https://stacks.math.columbia.edu/tag/0014.
 -/
 class category (obj : Type u)
 extends category_struct.{v} obj : Type (max u (v+1)) :=
@@ -119,13 +121,17 @@ by { split_ifs; refl }
 /--
 A morphism `f` is an epimorphism if it can be "cancelled" when precomposed:
 `f ≫ g = f ≫ h` implies `g = h`.
+
+See https://stacks.math.columbia.edu/tag/003B.
 -/
 class epi (f : X ⟶ Y) : Prop :=
 (left_cancellation : Π {Z : C} (g h : Y ⟶ Z) (w : f ≫ g = f ≫ h), g = h)
 
 /--
 A morphism `f` is a monomorphism if it can be "cancelled" when postcomposed:
 `g ≫ f = h ≫ f` implies `g = h`.
+
+See https://stacks.math.columbia.edu/tag/003B.
 -/
 class mono (f : X ⟶ Y) : Prop :=
 (right_cancellation : Π {Z : C} (g h : Z ⟶ X) (w : g ≫ f = h ≫ f), g = h)
@@ -218,6 +224,15 @@ namespace preorder
 
 variables (α : Type u)
 
+/--
+The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.
+
+Because we don't allow morphisms to live in `Prop`,
+we have to define `X ⟶ Y` as `ulift (plift (X ≤ Y))`.
+See `category_theory.hom_of_le` and `category_theory.le_of_hom`.
+
+See https://stacks.math.columbia.edu/tag/00D3.
+-/
 @[priority 100] -- see Note [lower instance priority]
 instance small_category [preorder α] : small_category α :=
 { hom  := λ U V, ulift (plift (U ≤ V)),

src/category_theory/connected.lean

@@ -53,6 +53,8 @@ We instead are interested in categories with exactly one 'connected
 component'.
 
 This allows us to show that the functor X ⨯ - preserves connected limits.
+
+See https://stacks.math.columbia.edu/tag/002S
 -/
 class connected (J : Type v₂) [category.{v₁} J] extends inhabited J :=
 (iso_constant : Π {α : Type v₂} (F : J ⥤ discrete α), F ≅ (functor.const J).obj (F.obj default))

src/category_theory/discrete_category.lean

@@ -15,6 +15,14 @@ with the only morphisms being equalities.
 -/
 def discrete (α : Type u₁) := α
 
+/--
+The "discrete" category on a type, whose morphisms are equalities.
+
+Because we do not allow morphisms in `Prop` (only in `Type`),
+somewhat annoyingly we have to define `X ⟶ Y` as `ulift (plift (X = Y))`.
+
+See https://stacks.math.columbia.edu/tag/001A
+-/
 instance discrete_category (α : Type u₁) : small_category (discrete α) :=
 { hom  := λ X Y, ulift (plift (X = Y)),
   id   := λ X, ulift.up (plift.up rfl),

src/category_theory/equivalence.lean

@@ -18,6 +18,8 @@ universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `categor
   The triangle equation is written as a family of equalities between morphisms, it is more
   complicated if we write it as an equality of natural transformations, because then we would have
   to insert natural transformations like `F ⟶ F1`.
+
+See https://stacks.math.columbia.edu/tag/001J
 -/
 structure equivalence (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :=
 mk' ::
@@ -394,6 +396,14 @@ eq_of_inv_eq_inv (functor_unit_comp _ _)
 
 end is_equivalence
 
+/--
+A functor `F : C ⥤ D` is essentially surjective if for every `d : D`, there is some `c : C`
+so `F.obj c ≅ D`.
+
+See https://stacks.math.columbia.edu/tag/001C.
+-/
+-- TODO should we make this a `Prop` that merely asserts the existence of a preimage,
+-- rather than choosing one?
 class ess_surj (F : C ⥤ D) :=
 (obj_preimage (d : D) : C)
 (iso' (d : D) : F.obj (obj_preimage d) ≅ d . obviously)
@@ -408,9 +418,19 @@ end functor
 
 namespace equivalence
 
+/--
+An equivalence is essentially surjective.
+
+See https://stacks.math.columbia.edu/tag/02C3.
+-/
 def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
 ⟨ λ Y : D, F.inv.obj Y, λ Y : D, (F.inv_fun_id.app Y) ⟩
 
+/--
+An equivalence is faithful.
+
+See https://stacks.math.columbia.edu/tag/02C3.
+-/
 @[priority 100] -- see Note [lower instance priority]
 instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :=
 { map_injective' := λ X Y f g w,
@@ -419,6 +439,11 @@ instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :
     simpa only [cancel_epi, cancel_mono, is_equivalence.inv_fun_map] using p
   end }.
 
+/--
+An equivalence is full.
+
+See https://stacks.math.columbia.edu/tag/02C3.
+-/
 @[priority 100] -- see Note [lower instance priority]
 instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
 { preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y,
@@ -431,6 +456,11 @@ instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
   map_id' := λ X, begin apply F.map_injective, tidy end,
   map_comp' := λ X Y Z f g, by apply F.map_injective; simp }
 
+/--
+A functor which is full, faithful, and essentially surjective is an equivalence.
+
+See https://stacks.math.columbia.edu/tag/02C3.
+-/
 def equivalence_of_fully_faithfully_ess_surj
   (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : is_equivalence F :=
 is_equivalence.mk (equivalence_inverse F)

src/category_theory/filtered.lean

@@ -62,6 +62,8 @@ A category `is_filtered` if
 2. for every pair of parallel morphisms there exists a morphism to the right so the compositions
    are equal, and
 3. there exists some object.
+
+See https://stacks.math.columbia.edu/tag/002V. (They also define a diagram being filtered.)
 -/
 class is_filtered extends is_filtered_or_empty C : Prop :=
 [nonempty : nonempty C]

src/category_theory/full_subcategory.lean

@@ -87,6 +87,11 @@ section full_subcategory
 variables {C : Type u₂} [category.{v} C]
 variables (Z : C → Prop)
 
+/--
+The category structure on a subtype; morphisms just ignore the property.
+
+See https://stacks.math.columbia.edu/tag/001D. We do not define 'strictly full' subcategories.
+-/
 instance full_subcategory : category.{v} {X : C // Z X} :=
 induced_category.category subtype.val
 

src/category_theory/fully_faithful.lean

@@ -16,6 +16,8 @@ variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D
 A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective.
 In fact, we use a constructive definition, so the `full F` typeclass contains data,
 specifying a particular preimage of each `f : F.obj X ⟶ F.obj Y`.
+
+See https://stacks.math.columbia.edu/tag/001C.
 -/
 class full (F : C ⥤ D) :=
 (preimage : ∀ {X Y : C} (f : (F.obj X) ⟶ (F.obj Y)), X ⟶ Y)
@@ -24,7 +26,11 @@ class full (F : C ⥤ D) :=
 restate_axiom full.witness'
 attribute [simp] full.witness
 
-/-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective.-/
+/--
+A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective.
+
+See https://stacks.math.columbia.edu/tag/001C.
+-/
 class faithful (F : C ⥤ D) : Prop :=
 (map_injective' [] : ∀ {X Y : C}, function.injective (@functor.map _ _ _ _ F X Y) . obviously)
 

src/category_theory/functor.lean

@@ -25,6 +25,8 @@ To apply a functor `F` to an object use `F.obj X`, and to a morphism use `F.map
 
 The axiom `map_id` expresses preservation of identities, and
 `map_comp` expresses functoriality.
+
+See https://stacks.math.columbia.edu/tag/001B.
 -/
 structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
   Type (max v₁ v₂ u₁ u₂) :=

src/category_theory/isomorphism.lean

@@ -34,11 +34,15 @@ universes v u -- declare the `v`'s first; see `category_theory.category` for an
 namespace category_theory
 open category
 
-/-- An isomorphism (a.k.a. an invertible morphism) between two objects of a category.
+/--
+An isomorphism (a.k.a. an invertible morphism) between two objects of a category.
 The inverse morphism is bundled.
 
 See also `category_theory.core` for the category with the same objects and isomorphisms playing
-the role of morphisms. -/
+the role of morphisms.
+
+See https://stacks.math.columbia.edu/tag/0017.
+-/
 structure iso {C : Type u} [category.{v} C] (X Y : C) :=
 (hom : X ⟶ Y)
 (inv : Y ⟶ X)

src/category_theory/limits/fubini.lean

@@ -20,15 +20,19 @@ In the first part, given a coherent family `D` of limit cones over the functors
 and a cone `c` over `G`, we construct a cone over the cone points of `D`.
 We then show that if `c` is a limit cone, the constructed cone is also a limit cone.
 
-In the second part, we state the Fubini theorem in the setting where we have chosen limits
-provided by suitable `has_limit` classes.
+In the second part, we state the Fubini theorem in the setting where limits exist
+promised by `has_limit` classes.
 
 We construct
 `limit_uncurry_iso_limit_comp_lim F : limit (uncurry.obj F) ≅ limit (F ⋙ lim)`
 and give simp lemmas characterising it.
 For convenience, we also provide
 `limit_iso_limit_curry_comp_lim G : limit G ≅ limit ((curry.obj G) ⋙ lim)`
 in terms of the uncurried functor.
+
+## Future work
+
+The dual statement.
 -/
 
 universes v u

src/category_theory/limits/limits.lean

@@ -7,20 +7,60 @@ import category_theory.adjunction.basic
 import category_theory.limits.cones
 import category_theory.reflects_isomorphisms
 
+/-!
+# Limits and colimits
+
+We set up the general theory of limits and colimits in a category.
+In this introduction we only describe the setup for limits;
+it is repeated, with slightly different names, for colimits.
+
+The three main structures involved are
+* `is_limit c`, for `c : cone F`, `F : J ⥤ C`, expressing that `c` is a limit cone,
+* `limit_cone F`, which consists of a choice of cone for `F` and the fact it is a limit cone, and
+* `has_limit F`, asserting the mere existence of some limit cone for `F`.
+
+Typically there are two different ways one can use the limits library:
+1. working with particular cones, and terms of type `is_limit`
+2. working solely with `has_limit`.
+
+While `has_limit` only asserts the existence of a limit cone,
+we happily use the axiom of choice in mathlib,
+so there are convenience functions all depending on `has_limit F`:
+* `limit F : C`, producing some limit object
+* `limit.π F j : limit F ⟶ F.obj j`, the morphisms out of the limit,
+* `limit.lift F c : c.X ⟶ limit F`, the universal morphism from any other `c : cone F`, etc.
+
+There are abbreviations `has_limits_of_shape J C` and `has_limits C`
+asserting the existence of classes of limits.
+Later more are introduced, for finite limits, special shapes of limits, etc.
+
+## Implementation
+At present we simply say everything twice, in order to handle both limits and colimits.
+It would be highly desirable to have some automation support,
+e.g. a `@[dualize]` attribute that behaves similarly to `@[to_additive]`.
+
+## References
+* [Stacks: Limits and colimits](https://stacks.math.columbia.edu/tag/002D)
+
+-/
+
 open category_theory category_theory.category category_theory.functor opposite
 
 namespace category_theory.limits
 
 universes v u u' u'' w -- declare the `v`'s first; see `category_theory.category` for an explanation
 
--- See the notes at the top of cones.lean, explaining why we can't allow `J : Prop` here.
 variables {J K : Type v} [small_category J] [small_category K]
 variables {C : Type u} [category.{v} C]
 
 variables {F : J ⥤ C}
 
-/-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
-  cone morphism to `t`. -/
+/--
+A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
+cone morphism to `t`.
+
+See https://stacks.math.columbia.edu/tag/002E.
+  -/
 @[nolint has_inhabited_instance]
 structure is_limit (t : cone F) :=
 (lift  : Π (s : cone F), s.X ⟶ t.X)
@@ -371,8 +411,12 @@ end
 
 end is_limit
 
-/-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
-  cocone morphism from `t`. -/
+/--
+A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
+cocone morphism from `t`.
+
+See https://stacks.math.columbia.edu/tag/002F.
+-/
 @[nolint has_inhabited_instance]
 structure is_colimit (t : cocone F) :=
 (desc  : Π (s : cocone F), t.X ⟶ s.X)