Port the theories folder (#505)

Co-authored-by: Johan Commelin <[email protected]>

data/menus.yaml

@@ -35,6 +35,14 @@
     - Undergraduate maths: undergrad.html
     - Wiedijk's 100 theorems: 100.html
 
+- title: Theories
+  items:
+    - Natural Numbers: theories/naturals.html
+    - Linear Algebra: theories/linear_algebra.html
+    - Sets and finite sets: theories/sets.html
+    - Topology: theories/topology.html
+    - Category Theory: theories/category_theory.html
+
 - title: Contributing
   items:
     - Pull request lifecycle: contribute/index.html

templates/theories/category_theory.md

@@ -1,39 +1,20 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: category theory
 
-The `category` typeclass is defined in [category_theory/category/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/category/basic.html).
-It depends on the type of the objects, so for example we might write `category (Type u)` if we're talking about a category whose objects are types (in universe `u`).
+The `Category` typeclass is defined in [`Mathlib.CategoryTheory.Category.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Basic.html).
+It depends on the type of the objects, so for example we might write `Category (Type u)` if we're talking about a category whose objects are types (in universe `u`).
 
-Functors (which are a structure, not a typeclass) are defined in [category_theory/functor/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/functor/basic.html),
+Functors (which are a structure, not a typeclass) are defined in [`Mathlib.CategoryTheory.Functor.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Basic.html),
 along with identity functors and functor composition.
 
-Natural transformations, and their compositions, are defined in [category_theory/natural_transformation.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/natural_transformation.html).
+Natural transformations, and their compositions, are defined in [`Mathlib.CategoryTheory.NatTrans`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/NatTrans.html).
 
 The category of functors and natural transformations between fixed categories `C` and `D`
-is defined in [category_theory/functor/category.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/functor/category.html).
+is defined in [`Mathlib.CategoryTheory.Functor.Category`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Category.html).
 
 Cartesian products of categories, functors, and natural transformations appear in
-[category_theory/products/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/products/basic.html). (Product in the sense of limits will appear elsewhere soon!)
+[`Mathlib.CategoryTheory.Products.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Products/Basic.html).
 
-The category of types, and the hom pairing functor, are defined in [category_theory/types.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/types.html).
+The category of types, and the hom pairing functor, are defined in [`Mathlib.CategoryTheory.Types`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Types.html).
 
 ## Notation
 
@@ -58,7 +39,6 @@ We use `≅` for isomorphisms.
 ### Functors
 
 We use `⥤` (`\func`) to denote functors, as in `C ⥤ D` for the type of functors from `C` to `D`.
-(Unfortunately `⇒` is reserved in [`logic.relator`](https://github.com/leanprover-community/mathlib/blob/master/src/logic/relator.lean), so we can't use that here.)
 
 We use `F.obj X` to denote the action of a functor on an object.
 We use `F.map f` to denote the action of a functor on a morphism`.