fixing sheaves; they'll need replacing anyway

src/category_theory/locally_ringed.lean

@@ -1,25 +1,25 @@
--- import category_theory.sheaves
--- import category_theory.examples.rings.universal
+import category_theory.sheaves
+import category_theory.examples.rings.universal
 
--- universes v
+universes v
 
--- open category_theory.examples
--- open category_theory.limits
+open category_theory.examples
+open category_theory.limits
 
--- variables (α : Type v) [topological_space α]
+variables (X : Top.{v})
 
--- def structure_sheaf := sheaf.{v+1 v} α CommRing
+def structure_sheaf := sheaf.{v+1 v} X CommRing
 
--- structure ringed_space :=
--- (𝒪 : structure_sheaf α)
+structure ringed_space :=
+(𝒪 : structure_sheaf X)
 
--- structure locally_ringed_space extends ringed_space α :=
--- (locality : ∀ x : α, local_ring (stalk_at.{v+1 v} 𝒪 x).1)
+structure locally_ringed_space extends ringed_space X :=
+(locality : ∀ x : X, local_ring (stalk_at.{v+1 v} 𝒪.presheaf x).1) -- coercion from sheaf to presheaf?
 
--- def ringed_space.of_topological_space : ringed_space α :=
--- { 𝒪 := { presheaf := { obj       := λ U, sorry /- ring of continuous functions U → ℂ -/,
---                         map'      := sorry,
---                         map_id'   := sorry,
---                         map_comp' := sorry },
---           sheaf_condition := sorry,
---   } }
+def ringed_space.of_topological_space : ringed_space X :=
+{ 𝒪 := { presheaf := { obj       := λ U, sorry /- ring of continuous functions U → ℂ -/,
+                        map'      := sorry,
+                        map_id'   := sorry,
+                        map_comp' := sorry },
+          sheaf_condition := sorry,
+  } }

src/category_theory/presheaves.lean

@@ -70,7 +70,7 @@ def comp {F G H : Presheaf.{u v} C} (α : Presheaf_hom F G) (β : Presheaf_hom G
 
 end Presheaf_hom
 
-instance : category (Presheaf.{u v} C) :=
+instance category_of_presheaves : category (Presheaf.{u v} C) :=
 { hom := Presheaf_hom,
   id := Presheaf_hom.id,
   comp := @Presheaf_hom.comp C _,
@@ -123,8 +123,8 @@ instance : category (Presheaf.{u v} C) :=
       erw [category.comp_id],
       erw [category.comp_id],
       erw [category.id_comp] },
-  end
+  end }.
 
-}
+#print presheaves.category_of_presheaves
 
 end category_theory.presheaves

src/category_theory/presheaves/map.lean

@@ -6,15 +6,20 @@ universes u₁ v₁ u₂ v₂
 
 namespace category_theory.presheaves
 
-/- Presheaf to a 2-functor CAT ⥤₂ CAT, but we're not going to prove all of that yet. -/
+/- `Presheaf` is a 2-functor CAT ⥤₂ CAT, but we're not going to prove all of that yet. -/
 
 namespace Presheaf
 
 variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
 include 𝒞 𝒟
 variable (F : C ⥤ D)
 
--- def map (F : C ⥤ D) : Presheaf.{u₁ v₁} C ⥤ Presheaf.{u₂ v₂} D := sorry
+def map (F : C ⥤ D) : Presheaf.{u₁ v₁} C ⥤ Presheaf.{u₂ v₂} D :=
+{ obj := λ X, { X := X.X, 𝒪 := begin end },
+  map' := λ X Y f, { f := f.f, c := begin end } }
+
+def map₂ {F G : C ⥤ D} (α : F ⟹ G) : (map F) ⟹ (map G) :=
+{ app := begin end, }
 
 end Presheaf
 

src/category_theory/sheaves.lean

@@ -1,143 +1,148 @@
--- import category_theory.opposites
--- import category_theory.full_subcategory
--- import category_theory.universal.types
--- import category_theory.examples.topological_spaces
+import category_theory.opposites
+import category_theory.full_subcategory
+import category_theory.universal.types
+import category_theory.examples.topological_spaces
 
--- open category_theory
--- open category_theory.limits
--- open category_theory.examples
+open category_theory
+open category_theory.limits
+open category_theory.examples
 
--- universes u v u₁ v₁ u₂ v₂
+universes u v u₁ v₁ u₂ v₂
 
--- section
--- variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (V : Type u₂) [𝒱 : category.{u₂ v₂} V]
--- include 𝒞 𝒱
+section
+variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (V : Type u₂) [𝒱 : category.{u₂ v₂} V]
+include 𝒞 𝒱
 
--- def presheaf := C ⥤ V -- I know there's usually an op on C here, but I'm having trouble with opposites, so
---                        -- you'll have to provide it yourself!
+def presheaf := C ⥤ V -- I know there's usually an op on C here, but I'm having trouble with opposites, so
+                       -- you'll have to provide it yourself!
 
--- def presheaves : category (presheaf C V) := begin unfold presheaf, apply_instance end
--- end
-
--- variables (α : Type v) [topological_space α]
+def presheaves : category (presheaf C V) := begin unfold presheaf, apply_instance end
+end
 
--- local attribute [back] topological_space.is_open_inter
--- local attribute [back] open_set.is_open
+section
+variables {V : Type u} [𝒱 : category.{u v} V]
+include 𝒱 
+variables {X : Top.{v}}
 
--- instance : has_inter (open_set α) := 
--- { inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ }
+def presheaf.near (F : presheaf (open_set X) V) (x : X) : presheaf { U : open_set X // x ∈ U } V :=
+(full_subcategory_embedding (λ U : open_set X, x ∈ U)) ⋙ F
 
--- instance has_inter_op : has_inter ((open_set α)ᵒᵖ) := 
--- { inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ }
+variable [has_colimits.{u v} V]
 
--- structure cover' :=
--- (I : Type v)
--- (U : I → (open_set α))
+def stalk_at (F : presheaf (open_set X) V) (x : X) : V :=
+colimit (F.near x)
 
--- variables {α}
+end
 
--- -- TODO cleanup
--- def cover'.union (c : cover' α) : open_set α := ⟨ set.Union (λ i : c.I, (c.U i).1), 
---   begin 
---   apply topological_space.is_open_sUnion, 
---   tidy, 
---   subst H_h,
---   exact (c.U H_w).2
---   end ⟩
--- def cover'.union_subset (c : cover' α) (i : c.I) : c.union ⟶ c.U i := by obviously
+variable (X : Top.{v})
 
--- private definition inter_subset_left {C : cover' α} (i j : C.I) : (C.U i) ⟶ (C.U i ∩ C.U j) := by obviously
--- private definition inter_subset_right {C : cover' α} (i j : C.I) : (C.U j) ⟶ (C.U i ∩ C.U j) := by obviously
+local attribute [back] topological_space.is_open_inter
+local attribute [back] open_set.is_open
 
+instance : has_inter (open_set X) := 
+{ inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ }
 
--- section
--- variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
--- include 𝒟
+instance has_inter_op : has_inter ((open_set X)ᵒᵖ) := 
+{ inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ }
 
--- definition res_left
---   {C : cover' α} 
---   (i j : C.I) 
---   (F : (open_set α) ⥤ D) : (F.obj (C.U i)) ⟶ (F.obj ((C.U i) ∩ (C.U j))) := 
--- F.map (inter_subset_left i j)
+structure cover' :=
+(I : Type v)
+(U : I → (open_set X))
 
--- definition res_right
---   {C : cover' α} 
---   (i j : C.I) 
---   (F : (open_set α) ⥤ D) : (F.obj (C.U j)) ⟶ (F.obj ((C.U i) ∩ (C.U j))) := 
--- F.map (inter_subset_right i j)
+variables {X}
 
--- private definition union_res
---   {C : cover' α} 
---   (i : C.I) 
---   (F : (open_set α) ⥤ D) : (F.obj (C.union)) ⟶ (F.obj ((C.U i))) := 
--- F.map (C.union_subset i)
+-- TODO cleanup
+def cover'.union (c : cover' X) : open_set X := ⟨ set.Union (λ i : c.I, (c.U i).1), 
+  begin 
+  apply topological_space.is_open_sUnion, 
+  tidy, 
+  subst H_h,
+  exact (c.U H_w).2
+  end ⟩
+def cover'.union_subset (c : cover' X) (i : c.I) : c.union ⟶ c.U i := by obviously
 
--- @[simp] lemma union_res_left_right 
---   {C : cover' α} 
---   (i j : C.I) 
---   (F : presheaf (open_set α) D) : union_res i F ≫ res_left i j F = union_res j F ≫ res_right i j F :=
--- begin
---   dsimp [union_res, res_left, res_right],
---   rw ← functor.map_comp,
---   rw ← functor.map_comp,
---   refl,
--- end
--- end
+private definition inter_subset_left {C : cover' X} (i j : C.I) : (C.U i) ⟶ (C.U i ∩ C.U j) := by obviously
+private definition inter_subset_right {C : cover' X} (i j : C.I) : (C.U j) ⟶ (C.U i ∩ C.U j) := by obviously
 
--- section
--- variables {V : Type u} [𝒱 : category.{u v} V] [has_products.{u v} V]
--- include 𝒱
 
--- variables (cover : cover' α) (F : presheaf (open_set α) V) 
+section
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
 
--- def sections : V :=
--- pi.{u v} (λ c : cover.I, F.obj (cover.U c))
+definition res_left
+  {C : cover' X} 
+  (i j : C.I) 
+  (F : (open_set X) ⥤ D) : (F.obj (C.U i)) ⟶ (F.obj ((C.U i) ∩ (C.U j))) := 
+F.map (inter_subset_left i j)
 
--- def select_section (i : cover.I) := pi.π (λ c : cover.I, F.obj (cover.U c)) i
+definition res_right
+  {C : cover' X} 
+  (i j : C.I) 
+  (F : (open_set X) ⥤ D) : (F.obj (C.U j)) ⟶ (F.obj ((C.U i) ∩ (C.U j))) := 
+F.map (inter_subset_right i j)
 
--- def overlaps : V :=
--- pi.{u v} (λ p : cover.I × cover.I, F.obj (cover.U p.1 ∩ cover.U p.2))
+private definition union_res
+  {C : cover' X} 
+  (i : C.I) 
+  (F : (open_set X) ⥤ D) : (F.obj (C.union)) ⟶ (F.obj ((C.U i))) := 
+F.map (C.union_subset i)
 
--- def left : (sections cover F) ⟶ (overlaps cover F) := 
--- pi.pre _ (λ p : cover.I × cover.I, p.1) ≫ pi.map (λ p, res_left p.1 p.2 F)
+@[simp] lemma union_res_left_right 
+  {C : cover' X} 
+  (i j : C.I) 
+  (F : presheaf (open_set X) D) : union_res i F ≫ res_left i j F = union_res j F ≫ res_right i j F :=
+begin
+  dsimp [union_res, res_left, res_right],
+  rw ← functor.map_comp,
+  rw ← functor.map_comp,
+  refl,
+end
+end
 
--- def right : (sections cover F) ⟶ (overlaps cover F) := 
--- pi.pre _ (λ p : cover.I × cover.I, p.2) ≫ pi.map (λ p, res_right p.1 p.2 F)
+section
+variables {V : Type u} [𝒱 : category.{u v} V] [has_products.{u v} V]
+include 𝒱
 
--- def res : F.obj (cover.union) ⟶ (sections cover F) :=
--- pi.lift (λ i, union_res i F)
+variables (cover : cover' X) (F : presheaf (open_set X) V) 
 
--- @[simp] lemma res_left_right : res cover F ≫ left cover F = res cover F ≫ right cover F :=
--- begin
---   dsimp [left, right, res],
---   rw ← category.assoc,
---   simp,
---   rw ← category.assoc,
---   simp,
--- end
+def sections : V :=
+pi.{u v} (λ c : cover.I, F.obj (cover.U c))
 
--- def cover_fork : fork (left cover F) (right cover F) :=
--- { X := F.obj (cover.union),
---   ι := res cover F, }
+def select_section (i : cover.I) := pi.π (λ c : cover.I, F.obj (cover.U c)) i
 
+def overlaps : V :=
+pi.{u v} (λ p : cover.I × cover.I, F.obj (cover.U p.1 ∩ cover.U p.2))
 
--- class is_sheaf (presheaf : presheaf (open_set α) V) :=
--- (sheaf_condition : Π (cover : cover' α), is_equalizer (cover_fork cover presheaf))
+def left : (sections cover F) ⟶ (overlaps cover F) := 
+pi.pre _ (λ p : cover.I × cover.I, p.1) ≫ pi.map (λ p, res_left p.1 p.2 F)
 
--- variables (α V)
+def right : (sections cover F) ⟶ (overlaps cover F) := 
+pi.pre _ (λ p : cover.I × cover.I, p.2) ≫ pi.map (λ p, res_right p.1 p.2 F)
 
--- structure sheaf  :=
--- (presheaf : presheaf (open_set α) V)
--- (sheaf_condition : is_sheaf presheaf)
+def res : F.obj (cover.union) ⟶ (sections cover F) :=
+pi.lift (λ i, union_res i F)
 
--- variables {α V}
+@[simp] lemma res_left_right : res cover F ≫ left cover F = res cover F ≫ right cover F :=
+begin
+  dsimp [left, right, res],
+  rw ← category.assoc,
+  simp,
+  rw ← category.assoc,
+  simp,
+end
 
--- def sheaf.near (F : sheaf α V) (x : α) : presheaf { U : open_set α // x ∈ U } V :=
--- (full_subcategory_embedding (λ U : open_set α, x ∈ U)) ⋙ F.presheaf
+def cover_fork : fork (left cover F) (right cover F) :=
+{ X := F.obj (cover.union),
+  ι := res cover F, }
 
--- variable [has_colimits.{u v} V]
 
--- def stalk_at (F : sheaf α V) (x : α) : V :=
--- colimit (F.near x)
+class is_sheaf (presheaf : presheaf (open_set X) V) :=
+(sheaf_condition : Π (cover : cover' X), is_equalizer (cover_fork cover presheaf))
 
--- end
+variables (X V)
+
+structure sheaf  :=
+(presheaf : presheaf (open_set X) V)
+(sheaf_condition : is_sheaf presheaf)
+
+end