feat(presheaves)

src/category_theory/instances/topological_spaces.lean

@@ -134,6 +134,15 @@ def map
 def map_iso {X Y : Top.{u}} (f g : X ⟶ Y) (h : f = g) : map f ≅ map g :=
 nat_iso.of_components (λ U, eq_to_iso (congr_fun (congr_arg _ (congr_arg _ h)) _) ) (by obviously)
 
-@[simp] def map_iso_id {X : Top.{u}} (h) : map_iso (𝟙 X) (𝟙 X) h = iso.refl (map _) := rfl
+@[simp] lemma map_iso_id {X : Top.{u}} (h) : map_iso (𝟙 X) (𝟙 X) h = iso.refl (map _) := rfl
+@[simp] lemma map_iso_id' {X Y : Top.{u}} (f : X ⟶ Y) : map_iso f f (refl _) = iso.refl (map _) := rfl
+
+@[simp] lemma map_iso_hom_app {X Y : Top.{u}} (f g : X ⟶ Y) (h : f = g) (U : opens Y) :
+  (map_iso f g h).hom.app U = eq_to_hom (congr_fun (congr_arg functor.obj (congr_arg map h)) U) :=
+rfl
+
+@[simp] lemma map_iso_inv_app {X Y : Top.{u}} (f g : X ⟶ Y) (h : f = g) (U : opens Y) :
+  (map_iso f g h).inv.app U = eq_to_hom (congr_fun (congr_arg functor.obj (congr_arg map h.symm)) U) :=
+rfl
 
 end topological_space.opens

src/category_theory/isomorphism.lean

@@ -48,6 +48,10 @@ calc α.inv
 @[simp] lemma symm_hom (α : X ≅ Y) : α.symm.hom = α.inv := rfl
 @[simp] lemma symm_inv (α : X ≅ Y) : α.symm.inv = α.hom := rfl
 
+@[simp] lemma symm_mk {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
+  iso.symm {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id} =
+    {hom := inv, inv := hom, hom_inv_id' := inv_hom_id, inv_hom_id' := hom_inv_id} := rfl
+
 @[refl] def refl (X : C) : X ≅ X :=
 { hom := 𝟙 X,
   inv := 𝟙 X }
@@ -64,6 +68,15 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
 @[simp] lemma trans_hom (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).hom = α.hom ≫ β.hom := rfl
 @[simp] lemma trans_inv (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
 
+@[simp] lemma trans_mk {X Y Z : C}
+  (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id)
+  (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id') (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
+  iso.trans
+    {hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id}
+    {hom := hom', inv := inv', hom_inv_id' := hom_inv_id', inv_hom_id' := inv_hom_id'} =
+  {hom := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''} :=
+rfl
+
 @[simp] lemma refl_symm (X : C) : (iso.refl X).hom = 𝟙 X := rfl
 @[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
 

src/category_theory/opposites.lean

@@ -98,6 +98,8 @@ instance category.opposite : category.{v₁} Cᵒᵖ :=
 @[simp] lemma unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :
   (f ≫ g).unop = g.unop ≫ f.unop := rfl
 @[simp] lemma unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) := rfl
+@[simp] lemma id_op_unop {X : C} : (𝟙 (op X)).unop = 𝟙 X := rfl
+@[simp] lemma id_unop_op {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X := rfl
 
 def op_op : (Cᵒᵖ)ᵒᵖ ⥤ C :=
 { obj := λ X, unop (unop X),
@@ -180,6 +182,18 @@ end
 
 end functor
 
+
+namespace nat_trans
+
+variables {D : Type u₂} [𝒟 : category.{v₂} D]
+include 𝒟
+variables {F G : C ⥤ D}
+@[simp] protected definition op (α : F ⟹ G) : G.op ⟹ F.op :=
+{ app         := λ X, (α.app (unop X)).op,
+  naturality' := begin tidy, erw α.naturality, refl, end}
+
+end nat_trans
+
 -- TODO the following definitions do not belong here
 
 omit 𝒞

src/category_theory/presheaf.lean

@@ -0,0 +1,161 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison, Mario Carneiro, Reid Barton
+
+import category_theory.instances.topological_spaces
+import category_theory.functor_category
+import category_theory.whiskering
+import category_theory.natural_isomorphism
+import category_theory.opposites
+import topology.basic
+
+open topological_space
+
+universes v u
+
+@[simp] lemma eq.trans_refl_left {α : Sort u} {p q : α} (h : p = q) : eq.trans (eq.refl _) h = h := rfl
+@[simp] lemma eq.trans_refl_right {α : Sort u} {p q : α} (h : p = q) : eq.trans h (eq.refl _) = h := rfl
+
+@[simp] lemma congr_arg_refl {α : Sort u} {β : Sort v} {f : α → β} {a : α} :
+  congr_arg f (eq.refl a) = eq.refl (f a) := rfl
+
+@[simp] lemma congr_refl_fun {α : Sort u} {β : Sort v} {f : α → β} {a₁ a₂ : α} (h : a₁ = a₂) :
+  congr (eq.refl f) h = congr_arg f h := rfl
+
+@[simp] lemma congr_refl_arg {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a : α} (h : f₁ = f₂) :
+  congr h (eq.refl a) = congr_fun h a := rfl
+
+open category_theory
+open category_theory.instances
+
+namespace category_theory.presheaves
+
+variables (C : Type u) [𝒞 : category.{v} C]
+include 𝒞
+
+structure Presheaf :=
+(X : Top.{v})
+(𝒪 : (opens X)ᵒᵖ ⥤ C)
+
+instance : has_coe_to_sort (Presheaf.{v} C) :=
+{ S := Type v, coe := λ F, F.X.α }
+
+variables {C}
+
+instance Presheaf_topological_space (F : Presheaf.{v} C) : topological_space F := F.X.str
+
+structure Presheaf_hom (F G : Presheaf.{v} C) :=
+(f : F.X ⟶ G.X)
+(c : G.𝒪 ⟹ ((opens.map f).op ⋙ F.𝒪))
+
+@[extensionality] lemma ext {F G : Presheaf.{v} C} (α β : Presheaf_hom F G)
+  (w : α.f = β.f) (h : α.c ⊟ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) F.𝒪) = β.c) :
+  α = β :=
+begin
+  cases α, cases β,
+  dsimp at w,
+  subst w,
+  congr,
+  ext,
+  have h' := congr_fun (congr_arg nat_trans.app h) X,
+  dsimp at h',
+  simpa using h',
+end
+.
+
+namespace Presheaf_hom
+@[simp] def id (F : Presheaf.{v} C) : Presheaf_hom F F :=
+{ f := 𝟙 F.X,
+  c := ((functor.id_comp _).inv) ⊟ (whisker_right (nat_trans.op (opens.map_id _).hom) _) }
+
+@[simp] def comp {F G H : Presheaf.{v} C} (α : Presheaf_hom F G) (β : Presheaf_hom G H) : Presheaf_hom F H :=
+{ f := α.f ≫ β.f,
+  c := β.c ⊟ (whisker_left (opens.map β.f).op α.c) }
+
+/- I tried to break out the axioms for `category (Presheaf C)` below as lemmas here,
+   but mysteriously `ext` (nor `apply ext`) doesn't work here! -/
+lemma comp_id {F G : Presheaf.{v} C} (α : Presheaf_hom F G) : @comp C _ _ _ _ α (id G) = α :=
+begin
+  ext1,
+  { -- Check the comorphisms
+    ext1,  -- compare natural transformations componentwise
+    dsimp [opposite] at X,
+    cases X, -- TODO why is this necessary?
+    dsimp,
+    simp,
+    -- FIXME why aren't these done by `simp`?
+    erw [category_theory.functor.map_id],
+    erw [category.comp_id],
+    refl, },
+  { -- Check the functions
+    simp only [Presheaf_hom.comp, Presheaf_hom.id, category.comp_id], },
+end
+.
+
+lemma id_comp {F G : Presheaf.{v} C} (α : Presheaf_hom F G) : comp (id F) α = α :=
+begin
+  ext1,
+  { -- Check the comorphisms
+    ext1, -- compare natural transformations componentwise
+    dsimp [Presheaf_hom.id, Presheaf_hom.comp],
+    simp,
+    -- FIXME, again, should be done by `simp`
+    erw [category_theory.functor.map_id, category.comp_id, category.comp_id], },
+  { -- Check the functions
+    dsimp [Presheaf_hom.id, Presheaf_hom.comp],
+    simp, }
+end
+lemma assoc {F G H K : Presheaf.{v} C} (α : Presheaf_hom F G) (β : Presheaf_hom G H) (γ : Presheaf_hom H K) :
+  comp (comp α β) γ = comp α (comp β γ) :=
+begin
+  ext1,
+  -- Check the comorphisms
+  { ext1,
+    dsimp only [Presheaf_hom.comp,
+            whisker_right, whisker_left, whiskering_right, whiskering_left,
+            opens.map_iso, nat_iso.of_components],
+    dsimp,
+    -- FIXME, again, by `simp`!
+    erw category_theory.functor.map_id,
+    simp only [category.assoc, category_theory.functor.map_id, category.comp_id],
+    refl, },
+  -- Check the functions
+  { dsimp [Presheaf_hom.comp],
+    simp only [category.assoc, eq_self_iff_true], },
+end
+
+end Presheaf_hom
+
+variables (C)
+
+instance category_of_presheaves : category (Presheaf.{v} C) :=
+{ hom := Presheaf_hom,
+  id := Presheaf_hom.id,
+  comp := @Presheaf_hom.comp C _,
+  comp_id' := @Presheaf_hom.comp_id C _,
+  id_comp' := @Presheaf_hom.id_comp C _,
+  assoc' := @Presheaf_hom.assoc C _ }.
+
+namespace Presheaf_hom
+@[simp] lemma id_f (F : Presheaf.{v} C) : ((𝟙 F) : F ⟶ F).f = 𝟙 F.X := rfl
+@[simp] lemma id_c (F : Presheaf.{v} C) :
+  ((𝟙 F) : F ⟶ F).c = (((functor.id_comp _).inv) ⊟ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) :=
+rfl
+@[simp] lemma comp_f {F G H : Presheaf.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
+  (α ≫ β).f = α.f ≫ β.f :=
+rfl
+@[simp] lemma comp_c {F G H : Presheaf.{v} C} (α : F ⟶ G) (β : G ⟶ H) :
+  (α ≫ β).c = (β.c ⊟ (whisker_left (opens.map β.f).op α.c)) :=
+rfl
+end Presheaf_hom
+
+attribute [simp] set.preimage_id -- TODO mathlib?
+
+variables {D : Type u} [𝒟 : category.{v} D]
+include 𝒟
+
+def functor.map_presheaf (F : C ⥤ D) : Presheaf.{v} C ⥤ Presheaf.{v} D :=
+{ obj := λ X, { X := X.X, 𝒪 := X.𝒪 ⋙ F },
+  map := λ X Y f, { f := f.f, c := whisker_right f.c F } }.
+
+end category_theory.presheaves