various

leanpkg.toml

@@ -5,5 +5,5 @@ lean_version = "nightly-2018-06-21"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "037a4b862e04c9e27823989f6b0156e0868c260f"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "227a7b5c1c26d925837ddb331e9862873385e533"}
 lean-tidy = {git = "https://github.com/semorrison/lean-tidy", rev = "e3edaab7af1d54b630da1a1fa85250bf2181abcb"}

src/category_theory/discrete_category.lean

@@ -8,7 +8,7 @@ import category_theory.equivalence
 
 namespace category_theory
 
-universes u₁ v₁ u₂ 
+universes u₁ v₁ u₂ v₂
 
 def discrete (α : Type u₁) := α
 
@@ -45,7 +45,7 @@ begin
 end
 
 namespace functor
-def of_function {C : Type (u₂+1)} [large_category C] {I : Type u₁} (F : I → C) : (discrete I) ⥤ C := 
+def of_function {C : Type u₂} [category.{u₂ v₂} C] {I : Type u₁} (F : I → C) : (discrete I) ⥤ C := 
 { obj := F,
   map' := λ X Y f, begin cases f, cases f, cases f, exact 𝟙 (F X) end }
 end functor

src/category_theory/equivalence/default.lean

@@ -66,30 +66,30 @@ calc
 
 set_option trace.tidy true
 
-def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E := 
-{ functor := e.functor ⋙ f.functor,
-  inverse := f.inverse ⋙ e.inverse,
-  fun_inv_id' := 
-  { hom := { app := λ X, effe_id e f X, naturality' := 
-      begin 
-        dsimp [effe_id],
-        intros,
-        rw ← category.assoc,
-        rw ← functor.map_comp,
-        rw nat_trans.app_eq_coe,
-        erw nat_trans.naturality ((fun_inv_id f).hom), -- work out why this is so difficult: we must be missing something
-        sorry 
-      end
-      /-begin tidy, rewrite_search_using [`search] end-/ }, -- These fail, exceeding max iterations.
-    inv := { app := λ X, id_effe e f X, naturality' := sorry },
-    hom_inv_id' := sorry, -- These seem to work: 13 step rewrites!
-    inv_hom_id' := sorry },
-  inv_fun_id' :=
-  { hom := { app := λ X, feef_id e f X, naturality' := sorry }, 
-    inv := { app := λ X, id_feef e f X, naturality' := sorry },
-    hom_inv_id' := sorry,
-    inv_hom_id' := sorry },
- }
+-- def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E := 
+-- { functor := e.functor ⋙ f.functor,
+--   inverse := f.inverse ⋙ e.inverse,
+--   fun_inv_id' := 
+--   { hom := { app := λ X, effe_id e f X, naturality' := 
+--       begin 
+--         dsimp [effe_id],
+--         intros,
+--         rw ← category.assoc,
+--         rw ← functor.map_comp,
+--         rw nat_trans.app_eq_coe,
+--         erw nat_trans.naturality ((fun_inv_id f).hom), -- work out why this is so difficult: we must be missing something
+--         sorry 
+--       end
+--       /-begin tidy, rewrite_search_using [`search] end-/ }, -- These fail, exceeding max iterations.
+--     inv := { app := λ X, id_effe e f X, naturality' := sorry },
+--     hom_inv_id' := sorry, -- These seem to work: 13 step rewrites!
+--     inv_hom_id' := sorry },
+--   inv_fun_id' :=
+--   { hom := { app := λ X, feef_id e f X, naturality' := sorry }, 
+--     inv := { app := λ X, id_feef e f X, naturality' := sorry },
+--     hom_inv_id' := sorry,
+--     inv_hom_id' := sorry },
+--  }
 
 end equivalence
 
@@ -141,8 +141,8 @@ def as_equivalence (F : C ⥤ D) [is_equivalence F] : C ≌ D :=
 variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
 include ℰ 
 
-instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] :
-  is_equivalence (F ⋙ G) := sorry
+-- instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] :
+--   is_equivalence (F ⋙ G) := sorry
 
 end functor
 

src/category_theory/examples/TopRing.lean

@@ -1,4 +1,4 @@
-import category_theory.category
+import category_theory.examples.rings
 import analysis.topology.topological_structures
 
 universes u
@@ -8,23 +8,35 @@ open category_theory
 namespace category_theory.examples
 
 structure TopRing :=
-{β : Type u}
-[Ring : comm_ring β]
-[Top : topological_space β]
-[TopRing : topological_ring β]
+{α : Type u}
+[is_comm_ring : comm_ring α]
+[is_topological_space : topological_space α]
+[is_topological_ring : topological_ring α]
 
-instance TopRing_comm_ring (R : TopRing) : comm_ring R.β := R.Ring
-instance TopRing_topological_space (R : TopRing) : topological_space R.β := R.Top
-instance TopRing_topological_ring (R : TopRing) : topological_ring R.β := R.TopRing
+instance : has_coe_to_sort TopRing :=
+{ S := Type u, coe := TopRing.α }
+
+instance TopRing_comm_ring (R : TopRing) : comm_ring R := R.is_comm_ring
+instance TopRing_topological_space (R : TopRing) : topological_space R := R.is_topological_space
+instance TopRing_topological_ring (R : TopRing) : topological_ring R := R.is_topological_ring
 
 instance : category TopRing :=
-{ hom   := λ R S, {f : R.β → S.β // is_ring_hom f ∧ continuous f },
+{ hom   := λ R S, {f : R → S // is_ring_hom f ∧ continuous f },
   id    := λ R, ⟨id, by obviously⟩,
   comp  := λ R S T f g, ⟨g.val ∘ f.val, 
     begin -- TODO automate
       cases f, cases g, cases f_property, cases g_property, split, 
       dsimp, resetI, apply_instance, 
       dsimp, apply continuous.comp ; assumption  
-    end⟩ }
+    end⟩ }.
+
+namespace TopRing
+/-- The forgetful functor to CommRing. -/
+def forget_to_CommRing : TopRing ⥤ CommRing := 
+{ obj := λ R, { α := R, str := examples.TopRing_comm_ring R },
+  map' := λ R S f, ⟨ f.1, f.2.left ⟩ }
+
+instance : faithful (forget_to_CommRing) := by tidy
+end TopRing
 
 end category_theory.examples

src/category_theory/examples/graphs.lean

@@ -12,16 +12,16 @@ namespace category_theory.examples.graphs
 
 universe u₁
 
-def Graph := Σ α : Type (u₁+1), graph α
+def Graph := Σ α : Type (u₁+1), graph.{u₁+1 u₁} α
 
 instance graph_from_Graph (G : Graph) : graph G.1 := G.2
 
-structure GraphHomomorphism (G H : Graph.{u₁}) : Type (u₁+1) := 
-(map : @graph_homomorphism G.1 G.2 H.1 H.2)
+structure Graph_hom (G H : Graph.{u₁}) : Type (u₁+1) := 
+(map : @graph_hom G.1 G.2 H.1 H.2)
 
 @[extensionality] lemma graph_homomorphisms_pointwise_equal
   {G H : Graph.{u₁}}
-  {p q : GraphHomomorphism G H} 
+  {p q : Graph_hom G H} 
   (vertexWitness : ∀ X : G.1, p.map.onVertices X = q.map.onVertices X) 
   (edgeWitness : ∀ X Y : G.1, ∀ f : edges X Y, ⟬ p.map.onEdges f ⟭ = q.map.onEdges f ) : p = q :=
 begin
@@ -32,7 +32,7 @@ begin
 end
 
 instance CategoryOfGraphs : large_category Graph := {
-  hom := GraphHomomorphism,
+  hom := Graph_hom,
   id := λ G, ⟨ {
       onVertices   := id,
       onEdges := λ _ _ f, f

src/category_theory/filtered.lean

@@ -25,6 +25,6 @@ class filtered :=
 instance [inhabited α] [preorder α] [directed α] : filtered.{u₁ u₁} α :=
 { default := default α,
   obj_bound := λ x y, { X := directed.bound x y, ι₁ := ⟨ ⟨ directed.i₁ x y ⟩ ⟩, ι₂ := ⟨ ⟨ directed.i₂ x y ⟩ ⟩ },
-  hom_bound := λ _ y f g, { X := y, π := 𝟙 y, w := begin cases f, cases f, cases g, cases g, simp end } }
+  hom_bound := λ _ y f g, { X := y, π := 𝟙 y, w' := begin cases f, cases f, cases g, cases g, simp end } }
 
 end category_theory

src/category_theory/graph_category.lean

@@ -0,0 +1,47 @@
+import category_theory.path_category
+import tactic.linarith
+
+open category_theory.graphs
+
+universes u₁ v₁
+
+namespace category_theory
+
+def finite_graph {n k : ℕ} (e : vector (fin n × fin n) k) := ulift.{v₁} (fin n)
+
+instance finite_graph_category {n k : ℕ} (e : vector (fin n × fin n) k) : graph.{v₁ v₁} (finite_graph e) :=
+{ edges := λ x y, ulift { a : fin k // e.nth a = (x.down, y.down) } }
+
+def parallel_pair : vector (fin 2 × fin 2) 2 := ⟨ [(0, 1), (0, 1)], by refl ⟩
+
+-- Verify typeclass inference is hooked up correctly:
+example : category.{v₁ v₁} (paths (finite_graph parallel_pair)) := by apply_instance.
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+@[simp] def eq_to_hom {X Y : C} (h : X = Y) : X ⟶ Y := (eq_to_iso h).hom
+
+@[simp] def graph_functor {n k : ℕ} {e : vector (fin n × fin n) k} 
+  (objs : vector C n) (homs : Π m : fin k, objs.nth (e.nth m).1 ⟶ objs.nth (e.nth m).2) :
+  paths (finite_graph.{v₁} e) ⥤ C :=
+functor.of_graph_hom
+{ onVertices := λ x, objs.nth x.down,
+  onEdges := λ x y f, 
+  begin 
+    have p := homs f.down.val,
+    refine (eq_to_hom _) ≫ p ≫ (eq_to_hom _), -- TODO this needs a name, e.g. `convert_hom`
+    rw f.down.property,
+    rw f.down.property,
+  end}
+
+
+def parallel_pair_functor {X Y : C} (f g : X ⟶ Y) : paths.{v₁} (finite_graph parallel_pair) ⥤ C :=
+graph_functor ⟨ [X, Y], by refl ⟩
+(λ m, match m with 
+| ⟨ 0, _ ⟩ := f 
+| ⟨ 1, _ ⟩ := g
+| ⟨ n+2, _ ⟩ := by exfalso; linarith
+end)
+
+end category_theory

src/category_theory/graphs/category.lean

@@ -9,10 +9,10 @@ namespace category_theory
 
 open category_theory.graphs
 
-universe u
+universes u v
 variable {C : Type u}
 
-instance category.graph [𝒞 : small_category C] : graph C := {
+instance category.graph [𝒞 : category.{u v} C] : graph C := {
   edges := 𝒞.hom
 }
 

src/category_theory/graphs/default.lean

@@ -7,28 +7,27 @@ import tidy.auto_cast
 
 namespace category_theory.graphs
 
-universes u₁ u₂
+universes u₁ v₁ u₂ v₂
 
 class graph (vertices : Type u₁) :=
-  (edges : vertices → vertices → Type u₁)
+  (edges : vertices → vertices → Type v₁)
 
 variable {C : Type u₁}
 variables {W X Y Z : C}
-variable [graph C]
+variable [𝒞 : graph.{u₁ v₁} C]
 
-def edges : C → C → Type u₁ := graph.edges
+def edges : C → C → Type v₁ := @graph.edges.{u₁ v₁} C 𝒞
 
-structure graph_homomorphism (G : Type u₁) [graph G] (H : Type u₂) [graph H] := 
+structure graph_hom (G : Type u₁) [graph.{u₁ v₁} G] (H : Type u₂) [graph.{u₂ v₂} H] := 
   (onVertices : G → H)
   (onEdges    : ∀ {X Y : G}, edges X Y → edges (onVertices X) (onVertices Y))
 
-variable {G : Type u₁}
-variable [graph G]
-variable {H : Type u₂}
-variable [graph H]
+section
+variables {G : Type u₁} [𝒢 : graph.{u₁ v₁} G] {H : Type u₂} [ℋ : graph.{u₂ v₂} H]
+include 𝒢 ℋ
 
-@[extensionality] lemma graph_homomorphisms_pointwise_equal
-  {p q : graph_homomorphism G H} 
+@[extensionality] lemma graph_hom_pointwise_equal
+  {p q : graph_hom G H} 
   (vertexWitness : ∀ X : G, p.onVertices X = q.onVertices X) 
   (edgeWitness : ∀ X Y : G, ∀ f : edges X Y, ⟬ p.onEdges f ⟭ = q.onEdges f) : p = q :=
 begin
@@ -41,15 +40,19 @@ begin
   exact edgeWitness X Y f,
   subst h_edges
 end
+end
+
+variables {G : Type u₁} [𝒢 : graph.{u₁ v₁} G]
+include 𝒢
 
-inductive path : G → G → Type u₁
+inductive path : G → G → Type (max u₁ v₁)
 | nil  : Π (h : G), path h h
 | cons : Π {h s t : G} (e : edges h s) (l : path s t), path h t
 
 notation a :: b := path.cons a b
 notation `p[` l:(foldr `, ` (h t, path.cons h t) path.nil _ `]`) := l
 
-inductive path_of_paths : G → G → Type (u₁+1)
+inductive path_of_paths : G → G → Type (max u₁ v₁)
 | nil  : Π (h : G), path_of_paths h h
 | cons : Π {h s t : G} (e : path h s) (l : path_of_paths s t), path_of_paths h t
 

src/category_theory/limits/equalizers.lean

@@ -3,16 +3,13 @@
 -- Authors: Scott Morrison, Reid Barton, Mario Carneiro
 
 import category_theory.limits.shape
-import category_theory.filtered
 
 open category_theory
 
-
 namespace category_theory.limits
 
 universes u v w
 
-
 variables {C : Type u} [𝒞 : category.{u v} C]
 include 𝒞
 
@@ -114,10 +111,14 @@ def equalizer.ι : (equalizer f g) ⟶ Y := (equalizer.fork f g).ι
 @[search] def equalizer.w : (equalizer.ι f g) ≫ f = (equalizer.ι f g) ≫ g := (equalizer.fork f g).w
 def equalizer.universal_property : is_equalizer (equalizer.fork f g) := has_equalizers.is_equalizer.{u v} C f g
 
-def equalizer.lift (P : C) (h : P ⟶ Y) (w : h ≫ f = h ≫ g) : P ⟶ equalizer f g := 
-(equalizer.universal_property f g).lift { X := P, ι := h, w := w }
+variables {f g}
+
+def equalizer.lift {P : C} (h : P ⟶ Y) (w : h ≫ f = h ≫ g) : P ⟶ equalizer f g := 
+(equalizer.universal_property f g).lift { X := P, ι := h, w' := w }
 
-@[extensionality] lemma equalizer.hom_ext {Y Z : C} {f g : Y ⟶ Z} {X : C} (h k : X ⟶ equalizer f g) (w : h ≫ equalizer.ι f g = k ≫ equalizer.ι f g) : h = k :=
+lemma equalizer.lift_ι {P : C} (h : P ⟶ Y) (w : h ≫ f = h ≫ g) : equalizer.lift h w ≫ equalizer.ι f g = h := by obviously
+
+@[extensionality] lemma equalizer.hom_ext {X : C} (h k : X ⟶ equalizer f g) (w : h ≫ equalizer.ι f g = k ≫ equalizer.ι f g) : h = k :=
 begin
   let s : fork f g := ⟨ ⟨ X ⟩, h ≫ equalizer.ι f g ⟩,
   have q := (equalizer.universal_property f g).uniq s h,
@@ -128,4 +129,31 @@ end
 
 end
 
+section
+variables [has_coequalizers.{u v} C] {Y Z : C} (f g : Y ⟶ Z)
+
+def coequalizer.cofork := has_coequalizers.coequalizer.{u v} f g
+def coequalizer := (coequalizer.cofork f g).X
+def coequalizer.π : Z ⟶ (coequalizer f g) := (coequalizer.cofork f g).π
+@[search] def coequalizer.w : f ≫ (coequalizer.π f g)  = g ≫ (coequalizer.π f g) := (coequalizer.cofork f g).w
+def coequalizer.universal_property : is_coequalizer (coequalizer.cofork f g) := has_coequalizers.is_coequalizer.{u v} C f g
+
+variables {f g}
+
+def coequalizer.desc {P : C} (h : Z ⟶ P) (w : f ≫ h = g ≫ h) : coequalizer f g ⟶ P := 
+(coequalizer.universal_property f g).desc { X := P, π := h, w' := w }
+
+lemma coequalizer.desc_π {P : C} (h : Z ⟶ P) (w : f ≫ h = g ≫ h) : coequalizer.π f g ≫ coequalizer.desc h w = h := by obviously
+
+@[extensionality] lemma coequalizer.hom_ext {X : C} (h k : coequalizer f g ⟶ X) (w : coequalizer.π f g ≫ h = coequalizer.π f g ≫ k) : h = k :=
+begin
+  let s : cofork f g := ⟨ ⟨ X ⟩, coequalizer.π f g ≫ h ⟩,
+  have q := (coequalizer.universal_property f g).uniq s h,
+  have p := (coequalizer.universal_property f g).uniq s k,
+  rw [q, ←p],
+  solve_by_elim, refl
+end
+
+end
+
 end category_theory.limits

src/category_theory/limits/limits.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison, Reid Barton, Mario Carneiro
 
-import category_theory.limits.shape
+import category_theory.discrete_category
 import category_theory.filtered
 import category_theory.functor_categories.whiskering
 import category_theory.universal.cones
@@ -123,16 +123,6 @@ def cone.pullback {F : J ⥤ C} (A : cone F) {X : C} (f : X ⟶ A.X) : cone F :=
 
 -- lemma limit.pullback_lift (F : J ⥤ C) (c : cone F) {X : C} (f : X ⟶ c.X) : limit.lift F (c.pullback f) = f ≫ limit.lift F c := sorry
 
--- @[extensionality] def limit.hom_ext {F : J ⥤ C} {c : cone F}
---   (f g : c.X ⟶ limit F)
---   (w_f : ∀ j, f ≫ limit.π F j = c.π j)
---   (w_g : ∀ j, g ≫ limit.π F j = c.π j) : f = g :=
--- begin
---   have p_f := (limit.universal_property F).uniq c f (by obviously),
---   have p_g := (limit.universal_property F).uniq c g (by obviously),
---   obviously,
--- end.
-
 @[extensionality] def limit.hom_ext {F : J ⥤ C} {X : C}
   (f g : X ⟶ limit F)
   (w : ∀ j, f ≫ limit.π F j = g ≫ limit.π F j) : f = g :=