Merge branch 'category_theory_4' into scott-supremum

category_theory/functor.lean

@@ -50,6 +50,8 @@ instance : has_coe_to_fun (C ↝ D) :=
 { F   := λ F, C → D,
   coe := λ F, F.obj }
 
+lemma refold_coe {F : C ↝ D} (X : C) : F.obj X = F X := by unfold_coes
+
 def map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F X) ⟶ (F Y) := F.map' f
 
 @[simp] lemma map_id (F : C ↝ D) (X : C) : F.map (𝟙 X) = 𝟙 (F X) := 

category_theory/heterogeneous_identity.lean

@@ -0,0 +1,34 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.isomorphism
+
+universes u v
+
+namespace category_theory
+
+section
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+
+def eq_to_iso {X Y : C} (p : X = Y) : X ≅ Y := by rw p
+
+@[simp,ematch] lemma eq_to_iso_refl (X : C) (p : X = X) : eq_to_iso p = (iso.refl X) := rfl
+
+@[simp,ematch] lemma eq_to_iso_trans {X Y Z : C} (p : X = Y) (q : Y = Z) : (eq_to_iso p) ≪≫ (eq_to_iso q) = eq_to_iso (p.trans q) :=
+begin /- obviously' says: -/ ext, induction q, induction p, dsimp at *, simp at * end
+end
+
+namespace functor
+
+universes u₁ v₁ u₂ v₂
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒞 𝒟
+
+@[simp,ematch] lemma eq_to_iso (F : C ↝ D) {X Y : C} (p : X = Y) : F.on_isos (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
+begin /- obviously says: -/ ext1, induction p, dsimp at *, simp at * end
+end functor
+end category_theory
+

category_theory/isomorphism.lean

@@ -0,0 +1,160 @@
+-- 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_theory.functor
+
+-- TODO remove these once everything is merged
+import tactic.tidy
+@[obviously] meta def obviously' := tactic.tidy
+
+universes u v
+
+namespace category_theory
+
+structure iso {C : Type u} [category.{u v} C] (X Y : C) :=
+(hom : X ⟶ Y)
+(inv : Y ⟶ X)
+(hom_inv_id' : hom ≫ inv = 𝟙 X . obviously)
+(inv_hom_id' : inv ≫ hom = 𝟙 Y . obviously)
+
+restate_axiom iso.hom_inv_id'
+restate_axiom iso.inv_hom_id'
+attribute [simp] iso.hom_inv_id iso.inv_hom_id
+
+infixr ` ≅ `:10  := iso             -- type as \cong or \iso
+
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+variables {X Y Z : C}
+
+namespace iso
+
+instance : has_coe (iso.{u v} X Y) (X ⟶ Y) :=
+{ coe := iso.hom }
+
+@[extensionality] lemma ext
+  (α β : X ≅ Y)
+  (w : α.hom = β.hom) : α = β :=
+  begin
+    induction α with f g wα1 wα2,
+    induction β with h k wβ1 wβ2,
+    dsimp at *,
+    have p : g = k,
+      begin
+        induction w,
+        rw [← category.id_comp C k, ←wα2, category.assoc, wβ1, category.comp_id]
+      end,
+    induction p, induction w,
+    refl
+  end
+
+@[refl] def refl (X : C) : X ≅ X := 
+{ hom := 𝟙 X,
+  inv := 𝟙 X }
+
+@[simp] lemma refl_map (X : C) : (iso.refl X).hom = 𝟙 X := rfl
+@[simp] lemma refl_coe (X : C) : ((iso.refl X) : X ⟶ X) = 𝟙 X := rfl
+@[simp] lemma refl_inv  (X : C) : (iso.refl X).inv  = 𝟙 X := rfl
+
+@[trans] def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z := 
+{ hom := α.hom ≫ β.hom,
+  inv := β.inv ≫ α.inv,
+  hom_inv_id' := begin /- `obviously'` says: -/ erw [category.assoc], conv { to_lhs, congr, skip, rw ← category.assoc }, rw iso.hom_inv_id, rw category.id_comp, rw iso.hom_inv_id end,
+  inv_hom_id' := begin /- `obviously'` says: -/ erw [category.assoc], conv { to_lhs, congr, skip, rw ← category.assoc }, rw iso.inv_hom_id, rw category.id_comp, rw iso.inv_hom_id end }
+
+infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
+
+@[simp] lemma trans_hom (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).hom = α.hom ≫ β.hom := rfl
+@[simp] lemma trans_coe (α : X ≅ Y) (β : Y ≅ Z) : ((α ≪≫ β) : X ⟶ Z) = (α : X ⟶ Y) ≫ (β : Y ⟶ Z) := rfl
+@[simp] lemma trans_inv (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv  = β.inv ≫ α.inv   := rfl
+
+@[symm] def symm (I : X ≅ Y) : Y ≅ X := 
+{ hom := I.inv,
+  inv := I.hom }
+
+@[simp] lemma refl_symm_coe (X : C) : ((iso.refl X).symm : X ⟶ X)  = 𝟙 X := rfl
+@[simp] lemma trans_symm_coe (α : X ≅ Y) (β : Y ≅ Z) : ((α ≪≫ β).symm : Z ⟶ X) = (β.symm : Z ⟶ Y) ≫ (α.symm : Y ⟶ X) := rfl
+
+-- These next two aggressively rewrite the projections `.hom` and `.inv` into coercions.
+-- I'm not certain it is a good idea.
+@[simp] lemma hom_coe (α : X ≅ Y) : α.hom = (α : X ⟶ Y) := rfl
+@[simp] lemma inv_coe (α : X ≅ Y) : α.inv = (α.symm : Y ⟶ X) := rfl
+
+-- FIXME these are actually the ones we want to use
+@[simp] lemma hom_inv_id_coe (α : X ≅ Y) : (α : X ⟶ Y) ≫ (α.symm : Y ⟶ X) = 𝟙 X := begin unfold_coes, unfold symm, rw iso.hom_inv_id, end
+@[simp] lemma inv_hom_id_coe (α : X ≅ Y) : (α.symm : Y ⟶ X) ≫ (α : X ⟶ Y) = 𝟙 Y := begin unfold_coes, unfold symm, rw iso.inv_hom_id, end
+
+end iso
+
+class is_iso (f : X ⟶ Y) :=
+(inv : Y ⟶ X)
+(hom_inv_id' : f ≫ inv = 𝟙 X . obviously)
+(inv_hom_id' : inv ≫ f = 𝟙 Y . obviously)
+
+restate_axiom is_iso.hom_inv_id'
+restate_axiom is_iso.inv_hom_id'
+attribute [simp,ematch] is_iso.hom_inv_id is_iso.inv_hom_id
+
+def inv' {f : X ⟶ Y} (p : is_iso f) := is_iso.inv f 
+def hom_inv_id' {f : X ⟶ Y} (p : is_iso f) : f ≫ inv' p = 𝟙 X := is_iso.hom_inv_id f 
+def inv_hom_id' {f : X ⟶ Y} (p : is_iso f) : inv' p ≫ f = 𝟙 Y := is_iso.inv_hom_id f 
+
+namespace is_iso
+
+instance (X : C) : is_iso (𝟙 X) := 
+{ inv := 𝟙 X }
+
+instance of_iso         (f : X ≅ Y) : is_iso (f : X ⟶ Y) :=
+{ inv   := f.inv }
+instance of_iso_inverse (f : X ≅ Y) : is_iso (f.symm : Y ⟶ X)  := 
+{ inv   := f.hom }
+
+end is_iso
+
+namespace functor
+
+universes u₁ v₁ u₂ v₂ 
+variables {D : Type u₂}
+
+variables [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+def on_isos (F : C ↝ D) {X Y : C} (i : X ≅ Y) : (F X) ≅ (F Y) :=
+{ hom := F.map i.hom,
+  inv := F.map i.inv,
+  hom_inv_id' := begin /- `obviously'` says: -/ dsimp at *, erw [←map_comp, iso.hom_inv_id_coe, ←map_id] end,
+  inv_hom_id' := begin /- `obviously'` says: -/ dsimp at *, erw [←map_comp, iso.inv_hom_id_coe, ←map_id] end }
+
+@[simp,ematch] lemma on_isos_hom (F : C ↝ D) {X Y : C} (i : X ≅ Y) : (F.on_isos i).hom = F.map i.hom := rfl
+@[simp,ematch] lemma on_isos_inv (F : C ↝ D) {X Y : C} (i : X ≅ Y) : (F.on_isos i).inv = F.map i.inv := rfl
+
+end functor
+
+class epi  (f : X ⟶ Y) := 
+(left_cancellation : Π {Z : C} (g h : Y ⟶ Z) (w : f ≫ g = f ≫ h), g = h)
+class mono (f : X ⟶ Y) :=
+(right_cancellation : Π {Z : C} (g h : Z ⟶ X) (w : g ≫ f = h ≫ f), g = h)
+
+instance epi_of_iso  (f : X ⟶ Y) [is_iso f] : epi f  := 
+{ left_cancellation := begin
+                         -- This is an interesting test case for better rewrite automation.
+                         intros,
+                         rw [←category.id_comp C g, ←category.id_comp C h],
+                         rw [← is_iso.inv_hom_id f],
+                         erw [category.assoc, w, category.assoc],
+                       end }
+instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f := 
+{ right_cancellation := begin
+                         intros,
+                         rw [←category.comp_id C g, ←category.comp_id C h],
+                         rw [← is_iso.hom_inv_id f],
+                         erw [←category.assoc, w, ←category.assoc]
+                       end }
+
+@[simp] lemma cancel_epi  (f : X ⟶ Y) [epi f]  (g h : Y ⟶ Z) : (f ≫ g = f ≫ h) ↔ g = h := 
+⟨ λ p, epi.left_cancellation g h p, by tidy ⟩
+@[simp] lemma cancel_mono (f : X ⟶ Y) [mono f] (g h : Z ⟶ X) : (g ≫ f = h ≫ f) ↔ g = h := 
+⟨ λ p, mono.right_cancellation g h p, by tidy ⟩
+
+end category_theory

category_theory/opposites.lean

@@ -2,7 +2,6 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Stephen Morgan, Scott Morrison
 
-import category_theory.functor
 import category_theory.products
 import category_theory.types
 

category_theory/types.lean

@@ -42,7 +42,7 @@ variables {D : Type u'} [𝒟 : category.{u' v'} D] (I J : D ↝ C) (ρ : I ⟹
 
 end functor_to_types
 
-definition ulift : (Type u) ↝ (Type (max u v)) := 
+definition ulift_functor : (Type u) ↝ (Type (max u v)) := 
 { obj       := λ X, ulift.{v} X,
   map'      := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down),
   map_id'   := begin /- `obviously'` says: -/ intros, ext, refl end,

docs/theories.md

@@ -15,7 +15,7 @@ scientists.
 * [Relations on types, quotients](theories/relations.md)
 * [Partial and total orders, lattices](theories/orders.md)
 * [Sets and set like objects](theories/sets.md)
-* [Categories](theories/categories.md)
+* [Categories](theories/category_theory.md)
 * [The natural numbers](theories/naturals.md)
 * [The integers](theories/integers.md)
 * [Groups](theories/groups.md)

docs/theories/categories.md → docs/theories/category_theory.md

@@ -9,32 +9,47 @@ 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).
 
+The category of functors and natural transformations between fixed categories `C` and `D`
+is defined in [category_theory/functor_category.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/functor_category.lean).
+
+Cartesian products of categories, functors, and natural transformations appear in
+ [category_theory/products.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/products.lean). (Product in the sense of limits will appear elsewhere soon!)
+
+ The category of types, and the hom pairing functor, are defined in  [category_theory/types.lean](https://github.com/leanprover/mathlib/blob/master/category_theory/types.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₂)}
+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
+nat_trans F G        : Type (max u₁ v₂)
+functor.category 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.
+Note then that if we specialise to small categories, where `uᵢ = vᵢ`, then 
+`functor.category 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 
+`functor.category 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:
+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 𝒞 𝒟
 ````
 
+Some care with using `section ... end` can be required to make sure these 
+included variables don't end up where they aren't wanted.
 
 ## Notation
 
@@ -56,8 +71,7 @@ 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 `⇒` (`\functor` or `\func`) is reserved in core: https://github.com/leanprover/lean/blob/master/library/init/relator.lean, so we can't use that here.
 
 We use `F 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`.
@@ -68,6 +82,6 @@ Functor composition can be written as `F ⋙ G`.
 We use `⟹` (`\nattrans` or `\==>`) to denote the type of natural transformations, e.g. `F ⟹ G`.
 We use `⇔` (`\<=>`) to denote the type of natural isomorphisms.
 
-We can use `τ X` for `τ.components X`.
+We prefer the of use `τ X` over `τ.app X`.
 
 For vertical and horiztonal composition of natural transformations we "cutely" use `⊟` (`\boxminus`) and `◫` (currently untypeable, but we could ask for `\boxvert`).