From 3b48f7a5ba669c18386e66af10931d8d0bb8078b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 30 Sep 2021 11:12:32 +0000 Subject: [PATCH] docs(category_theory): provide missing module docs (#9352) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Scott Morrison Co-authored-by: Yaël Dillies --- src/category_theory/endomorphism.lean | 11 +++++-- src/category_theory/epi_mono.lean | 10 ++++--- src/category_theory/eq_to_hom.lean | 21 ++++++++++++- src/category_theory/functor.lean | 17 ++++++----- src/category_theory/functor_category.lean | 13 ++++++++ src/category_theory/groupoid.lean | 20 +++++++++++++ .../natural_transformation.lean | 30 ++++++++++++++----- src/category_theory/opposites.lean | 16 ++++++++++ src/category_theory/whiskering.lean | 21 +++++++++++++ 9 files changed, 137 insertions(+), 22 deletions(-) diff --git a/src/category_theory/endomorphism.lean b/src/category_theory/endomorphism.lean index 4d2508d2968d2..cf9ad16917d5a 100644 --- a/src/category_theory/endomorphism.lean +++ b/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 diff --git a/src/category_theory/epi_mono.lean b/src/category_theory/epi_mono.lean index 8ddac9bf1b113..1c35d84ebd2ff 100644 --- a/src/category_theory/epi_mono.lean +++ b/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₂ diff --git a/src/category_theory/eq_to_hom.lean b/src/category_theory/eq_to_hom.lean index c7a18834f100c..2bfea23606cb3 100644 --- a/src/category_theory/eq_to_hom.lean +++ b/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. diff --git a/src/category_theory/functor.lean b/src/category_theory/functor.lean index 1529907123051..a5f5e8881fcf2 100644 --- a/src/category_theory/functor.lean +++ b/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 diff --git a/src/category_theory/functor_category.lean b/src/category_theory/functor_category.lean index dd99f85fe09e5..0a4c61e546824 100644 --- a/src/category_theory/functor_category.lean +++ b/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 diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean index 77dab11b93718..9fc449faf434d 100644 --- a/src/category_theory/groupoid.lean +++ b/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]. diff --git a/src/category_theory/natural_transformation.lean b/src/category_theory/natural_transformation.lean index d91227e7ae15a..f79814846df4d 100644 --- a/src/category_theory/natural_transformation.lean +++ b/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 diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean index 67afd166e4053..d44a4cb43493a 100644 --- a/src/category_theory/opposites.lean +++ b/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 diff --git a/src/category_theory/whiskering.lean b/src/category_theory/whiskering.lean index d8d7b8591485e..022a089f0e375 100644 --- a/src/category_theory/whiskering.lean +++ b/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₄