feat(category_theory): basic definitions

category_theory/category.lean

@@ -0,0 +1,43 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Stephen Morgan, Scott Morrison
+
+import tactic.make_lemma
+import tactic.interactive
+
+namespace categories
+
+universes u v
+
+meta def obviously := `[skip]  
+
+/- 
+The propositional fields of `category` are annotated with the auto_param `obviously`, which is just a synonym for `skip`.
+Actually, there is a tactic called `obviously` which is not part of this pull request, which should be used here. It successfully
+discharges a great many of these goals. For now, proofs which could be provided entirely by `obviously` (and hence omitted entirely
+and discharged by an auto_param), are all marked with a comment "-- obviously says:".
+-/
+
+class category (Obj : Type u) : Type (max u (v+1)) :=
+  (Hom : Obj → Obj → Type v)
+  (identity : Π X : Obj, Hom X X)
+  (compose  : Π {X Y Z : Obj}, Hom X Y → Hom Y Z → Hom X Z)
+  (left_identity  : ∀ {X Y : Obj} (f : Hom X Y), compose (identity X) f = f . obviously)
+  (right_identity : ∀ {X Y : Obj} (f : Hom X Y), compose f (identity Y) = f . obviously)
+  (associativity  : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z), compose (compose f g) h = compose f (compose g h) . obviously)
+
+notation `𝟙` := category.identity     -- type as \b1
+infixr ` ≫ `:80 := category.compose   -- type as \gg
+infixr ` ⟶ `:10  := category.Hom     -- type as \h
+
+-- make_lemma is a command that creates a lemma from a structure field, discarding all auto_param wrappers from the type.
+make_lemma category.left_identity
+make_lemma category.right_identity
+make_lemma category.associativity
+-- We tag some lemmas with the attribute `@[ematch]`, for later automation. (I'd be happy to change this to e.g. `@[search]`.)
+attribute [simp,ematch] category.left_identity_lemma category.right_identity_lemma category.associativity_lemma 
+
+abbreviation large_category (C : Type (u+1)) : Type (u+1) := category.{u+1 u} C
+abbreviation small_category (C : Type u)     : Type (u+1) := category.{u u} C
+
+end categories

category_theory/functor/default.lean

@@ -0,0 +1,75 @@
+-- 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 ..category
+
+open categories
+
+namespace categories.functor
+
+universes u₁ v₁ u₂ v₂ u₃ v₃
+
+structure Functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : Type (max u₁ v₁ u₂ v₂) :=
+  (onObjects     : C → D)
+  (onMorphisms   : Π {X Y : C}, (X ⟶ Y) → ((onObjects X) ⟶ (onObjects Y)))
+  (identities    : ∀ (X : C), onMorphisms (𝟙 X) = 𝟙 (onObjects X) . obviously)
+  (functoriality : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), onMorphisms (f ≫ g) = (onMorphisms f) ≫ (onMorphisms g) . obviously)
+
+make_lemma Functor.identities
+make_lemma Functor.functoriality
+attribute [simp,ematch] Functor.functoriality_lemma Functor.identities_lemma
+
+infixr ` +> `:70 := Functor.onObjects
+infixr ` &> `:70 := Functor.onMorphisms -- switch to ▹?
+infixr ` ↝ `:70 := Functor              -- type as \lea 
+
+definition IdentityFunctor (C : Type u₁) [category.{u₁ v₁} C] : C ↝ C := 
+{ onObjects     := id,
+  onMorphisms   := λ _ _ f, f,
+  identities    := begin 
+                     -- `obviously'` says:
+                     intros,
+                     refl 
+                   end,
+  functoriality := begin
+                     -- `obviously'` says:
+                     intros,
+                     refl
+                   end }
+
+instance (C) [category C] : has_one (C ↝ C) :=
+{ one := IdentityFunctor C }
+
+variable {C : Type u₁}
+variable [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+@[simp] lemma IdentityFunctor.onObjects (X : C) : (IdentityFunctor C) +> X = X := by refl
+@[simp] lemma IdentityFunctor.onMorphisms {X Y : C} (f : X ⟶ Y) : (IdentityFunctor C) &> f = f := by refl
+
+variable {D : Type u₂}
+variable [𝒟 : category.{u₂ v₂} D]
+variable {E : Type u₃}
+variable [ℰ : category.{u₃ v₃} E]
+include 𝒟 ℰ
+
+definition FunctorComposition (F : C ↝ D) (G : D ↝ E) : C ↝ E := 
+{ onObjects     := λ X, G +> (F +> X),
+  onMorphisms   := λ _ _ f, G &> (F &> f),
+  identities    := begin 
+                     -- `obviously'` says:
+                     intros,
+                     simp,
+                   end,
+  functoriality := begin
+                     -- `obviously'` says:
+                     intros,
+                     simp
+                   end }
+infixr ` ⋙ `:80 := FunctorComposition
+
+@[simp] lemma FunctorComposition.onObjects (F : C ↝ D) (G : D ↝ E) (X : C) : (F ⋙ G) +> X = G +> (F +> X) := by refl
+@[simp] lemma FunctorComposition.onMorphisms (F : C ↝ D) (G : D ↝ E) (X Y : C) (f : X ⟶ Y) : (F ⋙ G) &> f = G.onMorphisms (F &> f) := by refl
+
+end categories.functor

category_theory/natural_transformation.lean

@@ -0,0 +1,101 @@
+-- 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 .functor
+
+open categories
+open categories.functor
+
+namespace categories.natural_transformation
+
+universes u₁ v₁ u₂ v₂ u₃ v₃
+
+variable {C : Type u₁}
+variable [𝒞 : category.{u₁ v₁} C]
+variable {D : Type u₂}
+variable [𝒟 : category.{u₂ v₂} D]
+include 𝒞 𝒟
+
+structure NaturalTransformation (F G : C ↝ D) : Type (max u₁ v₂) :=
+  (components: Π X : C, (F +> X) ⟶ (G +> X))
+  (naturality: ∀ {X Y : C} (f : X ⟶ Y), (F &> f) ≫ (components Y) = (components X) ≫ (G &> f) . obviously)
+
+make_lemma NaturalTransformation.naturality
+attribute [ematch] NaturalTransformation.naturality_lemma
+
+infixr ` ⟹ `:50  := NaturalTransformation             -- type as \==> or ⟹
+
+definition IdentityNaturalTransformation (F : C ↝ D) : F ⟹ F := 
+{ components := λ X, 𝟙 (F +> X),
+  naturality := begin
+                  -- `obviously'` says:
+                  intros,
+                  simp
+                end }
+
+@[simp] lemma IdentityNaturalTransformation.components (F : C ↝ D) (X : C) : (IdentityNaturalTransformation F).components X = 𝟙 (F +> X) := by refl
+
+variables {F G H : C ↝ D}
+
+-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
+@[extensionality] lemma NaturalTransformations_componentwise_equal (α β : F ⟹ G) (w : ∀ X : C, α.components X = β.components X) : α = β :=
+begin
+  induction α with α_components α_naturality,
+  induction β with β_components β_naturality,
+  have hc : α_components = β_components := funext w,
+  subst hc
+end
+
+definition vertical_composition_of_NaturalTransformations (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H := 
+{ components := λ X, (α.components X) ≫ (β.components X),
+  naturality := begin
+                  -- `obviously'` says:
+                  intros,
+                  simp,
+                  erw [←category.associativity_lemma, NaturalTransformation.naturality_lemma, category.associativity_lemma, ←NaturalTransformation.naturality_lemma]
+                end }
+
+notation α `⊟` β:80 := vertical_composition_of_NaturalTransformations α β    
+
+@[simp,ematch] lemma vertical_composition_of_NaturalTransformations.components (α : F ⟹ G) (β : G ⟹ H) (X : C) : (α ⊟ β).components X = (α.components X) ≫ (β.components X) := by refl
+
+variable {E : Type u₃}
+variable [ℰ : category.{u₃ v₃} E]
+include ℰ
+
+instance (F : C ↝ D) : has_one (F ⟹ F) := 
+{ one := IdentityNaturalTransformation F }
+
+definition horizontal_composition_of_NaturalTransformations {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) : (F ⋙ H) ⟹ (G ⋙ I) :=
+{ components := λ X : C, (β.components (F +> X)) ≫ (I &> (α.components X)), 
+  naturality := begin
+                  -- `obviously'` says:
+                  intros,
+                  simp,
+                  -- Actually, obviously doesn't use exactly this sequence of rewrites, but achieves the same result
+                  rw [← category.associativity_lemma],
+                  rw [NaturalTransformation.naturality_lemma],
+                  rw [category.associativity_lemma],
+                  conv { to_rhs, rw [← Functor.functoriality_lemma] },
+                  rw [← α.naturality_lemma],
+                  rw [Functor.functoriality_lemma],
+                end }
+
+notation α `◫` β:80 := horizontal_composition_of_NaturalTransformations α β
+
+@[simp,ematch] lemma horizontal_composition_of_NaturalTransformations.components {F G : C ↝ D} {H I : D ↝ E} (α : F ⟹ G) (β : H ⟹ I) (X : C) : (α ◫ β).components X = (β.components (F +> X)) ≫ (I &> (α.components X)) := by refl
+
+@[ematch] lemma NaturalTransformation.exchange {F G H : C ↝ D} {I J K : D ↝ E} (α : F ⟹ G) (β : G ⟹ H) (γ : I ⟹ J) (δ : J ⟹ K) : ((α ⊟ β) ◫ (γ ⊟ δ)) = ((α ◫ γ) ⊟ (β ◫ δ)) := 
+begin
+  -- `obviously'` says:
+  apply categories.natural_transformation.NaturalTransformations_componentwise_equal,
+  intros,
+  simp,
+  -- again, this isn't actually what obviously says, but it achieves the same effect.
+  conv {to_lhs, congr, skip, rw [←category.associativity_lemma] },
+  rw [←NaturalTransformation.naturality_lemma],
+  rw [category.associativity_lemma],
+end
+
+end categories.natural_transformation

docs/theories/categories.md

@@ -0,0 +1,78 @@
+# Maths in Lean : category theory
+
+The `category` typeclass is defined in [category_theory/category.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/category.lean).
+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`).
+Some care is needed with universes (see the section [Universes](##markdown-header-universes)), and end users may often prefer the abbreviations `small_category` and `large_category`.
+
+Functors (which are a structure, not a typeclass) are defined in [category_theory/functor/default.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/functor/default.lean),
+along with identity functors and functor composition.
+
+Natural transformations, and their compositions, are defined in [category_theory/natural_transformation.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/natural_transformation.lean).
+
+## Universes
+
+Unfortunately in a category theory library we have to deal with universes carefully. We have the following:
+
+````
+category.{u₁ v₁}          : Type (max (u₁+1) (v₁+1))
+C                         : category.{u₁ v₁}
+D                         : category.{u₂ v₂}
+Functor C D               : Type (max u₁ u₂ v₁ v₂)
+F G                       : Functor C D
+NaturalTransformation F G : Type (max u₁ v₂)
+FunctorCategory C D       : category.{(max u₁ u₂ v₁ v₂) (max u₁ v₂)}
+````
+
+Note then that if we specialise to small categories, where `uᵢ = vᵢ`, then `FunctorCategory C D : category.{(max u₁ u₂) (max u₁ u₂)}`, and so is again a small category.
+If `C` is a small category and `D` is a large category (i.e. `u₂ = v₂+1`), and `v₂ = v₁` then we have `FunctorCategory C D : category.{v₁+1 v₁}` so is again a large category.
+
+Whenever you want to write code uniformly for small and large categories (which you do by talking about categories whose universe levels `u` and `v` are unrelated), you will find that
+Lean's `variable` mechanism doesn't always work, and the following trick is often helpful:
+
+````
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒞 𝒟
+````
+
+
+## Notation
+
+### Categories
+
+We use the `⟶` (`\hom`) arrow to denote sets of morphisms, as in `X ⟶ Y`.
+This leaves the actual category implicit; it is inferred from the type of X and Y by typeclass inference.
+
+We use `𝟙` (`\b1`) to denote identity morphisms, as in `𝟙 X`.
+
+We use `≫` (`\gg`) to denote composition of morphisms, as in `f ≫ g`, which means "`f` followed by `g`".
+This is the opposite order than the usual convention (which is lame).  
+
+### Isomorphisms
+We use `≅` for isomorphisms.
+
+### Functors
+We use `↝` (`\leadsto` or `\lea` or `\r~`) to denote functors, as in `C ↝ D` for the type of functors from `C` to `D`.
+Unfortunately Johannes reserved `⇒` (`\functor` or `\func`) in core: https://github.com/leanprover/lean/blob/master/library/init/relator.lean, so we can't use that here.
+Perhaps this is unnecessary, and it's better to just write `Functor C D`.
+
+Unfortunately, writing application of functors on objects and morphisms merely by function application is problematic.
+To do either, we need to use a coercion to a function type, and we aren't allowed to do both this way.
+Even doing one (probably application to objects) causes some serious problems to automation. I'll have one more go at this,
+but in the meantime:
+
+We use `+>` to denote the action of a functor on an object, as in `F +> X`.
+We use `&>` to denote the action of a functor on a morphism, as in `F &> f`.
+
+Functor composition can be written as `F ⋙ G`.
+
+### Natural transformations
+We use `⟹` (`\nattrans` or `\==>`) to denote the type of natural transformations, e.g. `F ⟹ G`.
+We use `⇔` (`\<=>`) to denote the type of natural isomorphisms.
+
+Unfortunately, while we'd like to write components of natural transformations via function application (e.g. `τ X`),
+this requires coercions to function types, which I don't like.
+
+For now we just write out `τ.components X`.
+
+For vertical and horiztonal composition of natural transformations we "cutely" use `⊟` (`\boxminus`) and `◫` (currently untypeable, but we could ask for `\boxvert`).

tactic/make_lemma.lean

@@ -0,0 +1,41 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import data.buffer.parser
+
+open lean.parser tactic interactive parser
+
+@[user_attribute] meta def field_lemma_attr : user_attribute :=
+{ name := `field_lemma, descr := "This definition was automatically generated from a structure field by `make_lemma`." }
+
+
+/- Make lemma takes a structure field, and makes a new, definitionally simplified copy of it, appending `_lemma` to the name.
+   The main application is to provide clean versions of structure fields that have been tagged with an auto_param. -/
+meta def make_lemma (d : declaration) (new_name : name) : tactic unit :=
+do (levels, type, value, reducibility, trusted) ← pure (match d.to_definition with
+  | declaration.defn name levels type value reducibility trusted :=
+    (levels, type, value, reducibility, trusted)
+  | _ := undefined
+  end),
+  (s, u) ← mk_simp_set ff [] [],
+  new_type ← (s.dsimplify [] type) <|> pure (type),
+  updateex_env $ λ env, env.add (declaration.defn new_name levels new_type value reducibility trusted),
+  field_lemma_attr.set new_name () tt
+
+private meta def name_lemma (n : name) :=
+match n.components.reverse with
+| last :: most := mk_str_name n.get_prefix (last.to_string ++ "_lemma")
+| nil          := undefined
+end
+
+@[user_command] meta def make_lemma_cmd (meta_info : decl_meta_info)
+  (_ : parse $ tk "make_lemma") : lean.parser unit :=
+do from_lemma ← ident,
+   from_lemma_fully_qualified ← resolve_constant from_lemma,
+  d ← get_decl from_lemma_fully_qualified <|>
+    fail ("declaration " ++ to_string from_lemma ++ " not found"),
+  do {
+    make_lemma d (name_lemma from_lemma_fully_qualified)
+  }.
+