starting on functoriality of Presheaf

leanpkg.toml

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

src/category_theory/functor_categories/whiskering.lean

@@ -37,9 +37,22 @@ variables {C} {D} {E}
 def whisker_on_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟹ H) : (F ⋙ G) ⟹ (F ⋙ H) :=
 ((whiskering_on_left C D E) F).map α
 
+@[simp] lemma whisker_on_left.app (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟹ H) (X : C) : (whisker_on_left F α) X = α (F X) := 
+begin
+  dsimp [whisker_on_left, whiskering_on_left],
+  rw category_theory.functor.map_id,
+  rw category.comp_id,
+end
+
 def whisker_on_right {G H : C ⥤ D} (α : G ⟹ H) (F : D ⥤ E) : (G ⋙ F) ⟹ (H ⋙ F) := 
 ((whiskering_on_right C D E) F).map α
 
+@[simp] lemma whisker_on_right.app {G H : C ⥤ D} (α : G ⟹ H) (F : D ⥤ E) (X : C) : (whisker_on_right α F) X = F.map (α X) := 
+begin
+  dsimp [whisker_on_right, whiskering_on_right],
+  rw category.id_comp,
+end
+
 @[simp] lemma whisker_on_left_vcomp (F : C ⥤ D) {G H K : D ⥤ E} (α : G ⟹ H) (β : H ⟹ K) : 
   whisker_on_left F (α ⊟ β) = ((whisker_on_left F α) ⊟ (whisker_on_left F β)) :=
 ((whiskering_on_left C D E) F).map_comp α β
@@ -53,22 +66,14 @@ include ℬ
 
 @[simp] lemma whisker_on_left_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟹ K) :
   whisker_on_left F (whisker_on_left G α) = (@whisker_on_left _ _ _ _ _ _ (F ⋙ G) _ _ α) :=
-by obviously
+by tidy
 
 @[simp] lemma whisker_on_right_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟹ K) :
   whisker_on_right (whisker_on_right α F) G = (@whisker_on_right _ _ _ _ _ _ _ _ α (F ⋙ G)) :=
-by obviously
+by tidy
 
 lemma whisker_on_right_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟹ H) (K : D ⥤ E) :
   whisker_on_right (whisker_on_left F α) K = whisker_on_left F (whisker_on_right α K) :=
-begin
-ext1, dsimp at *, 
-/- rewrite_search says (that humans shouldn't write proofs like): -/
-conv { to_lhs, rw [nat_trans.hcomp_app, category.id_comp, nat_trans.hcomp_app, functor.category.id_app, functor.map_comp ] {md := semireducible} },
-dsimp at *, simp at *,
-conv { to_rhs, rw [nat_trans.hcomp_app] {md := semireducible} },
-dsimp at *, simp at *, 
-erw [nat_trans.hcomp_app, category.id_comp],
-end
+by tidy
 
 end category_theory

src/category_theory/presheaves.lean

@@ -18,7 +18,7 @@ variables (C : Type u) [𝒞 : category.{u v} C]
 include 𝒞
 
 structure Presheaf :=
-(X : Top)
+(X : Top.{v})
 (𝒪 : (open_set X) ⥤ C)
 
 variables {C}
@@ -30,7 +30,7 @@ structure Presheaf_hom (F G : Presheaf.{u v} C) :=
 (c : G.𝒪 ⟹ ((open_set.map f) ⋙ F.𝒪))
 
 @[extensionality] lemma ext {F G : Presheaf.{u v} C} (α β : Presheaf_hom F G)
-  (w : α.f = β.f) (h : α.c ⊟ (whisker_on_right (open_set.map_iso w).hom F.𝒪) = β.c) :
+  (w : α.f = β.f) (h : α.c ⊟ (whisker_on_right (open_set.map_iso _ _ w).hom F.𝒪) = β.c) :
   α = β :=
 begin
   cases α, cases β,
@@ -70,6 +70,8 @@ def comp {F G H : Presheaf.{u v} C} (α : Presheaf_hom F G) (β : Presheaf_hom G
 
 end Presheaf_hom
 
+variables (C)
+
 instance category_of_presheaves : category (Presheaf.{u v} C) :=
 { hom := Presheaf_hom,
   id := Presheaf_hom.id,
@@ -125,6 +127,11 @@ instance category_of_presheaves : category (Presheaf.{u v} C) :=
       erw [category.id_comp] },
   end }.
 
-#print presheaves.category_of_presheaves
+namespace Presheaf_hom
+@[simp] lemma id_f (F : Presheaf.{u v} C) : ((𝟙 F) : F ⟶ F).f = 𝟙 F.X := rfl
+@[simp] lemma id_c (F : Presheaf.{u v} C) : ((𝟙 F) : F ⟶ F).c = (((functor.id_comp _).inv) ⊟ (whisker_on_right (open_set.map_id _).inv _)) := rfl
+@[simp] lemma comp_f {F G H : Presheaf.{u v} C} (α : F ⟶ G) (β : G ⟶ H) : (α ≫ β).f = α.f ≫ β.f := rfl
+@[simp] lemma comp_c {F G H : Presheaf.{u v} C} (α : F ⟶ G) (β : G ⟶ H) : (α ≫ β).c = (β.c ⊟ (whisker_on_left (open_set.map β.f) α.c)) := rfl
+end Presheaf_hom
 
 end category_theory.presheaves

src/category_theory/presheaves/map.lean

@@ -1,26 +1,80 @@
 import category_theory.presheaves
 
 open category_theory
+open category_theory.examples
 
-universes u₁ v₁ u₂ v₂
+universes u v
 
 namespace category_theory.presheaves
 
 /- `Presheaf` is a 2-functor CAT ⥤₂ CAT, but we're not going to prove all of that yet. -/
 
+attribute [simp] set.preimage_id -- mathlib??
+
 namespace Presheaf
 
-variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D]
+section
+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 :=
-{ obj := λ X, { X := X.X, 𝒪 := begin end },
-  map' := λ X Y f, { f := f.f, c := begin end } }
+set_option trace.tidy true
+
+def map (F : C ⥤ D) : Presheaf.{u v} C ⥤ Presheaf.{u v} D :=
+{ obj := λ X, { X := X.X, 𝒪 := X.𝒪 ⋙ F },
+  map' := λ X Y f, { f := f.f, c := whisker_on_right f.c F },
+  map_id' := 
+  begin 
+    intros X, 
+    ext1,
+    swap, -- check the continuous map first (hopefully this will not be necessary after my PR)
+    refl,
+    ext1, -- check the equality of natural transformations componentwise
+    dsimp at *, simp at *, dsimp at *,
+    obviously,
+  end,
+  map_comp' :=
+  begin
+    intros X Y Z f g, 
+    ext1, 
+    swap,
+    refl,
+    tidy,
+    dsimp [open_set.map_iso, nat_iso.of_components, open_set.map],
+    simp,
+  end }.
+
+def map₂ {F G : C ⥤ D} (α : F ⟹ G) : (map G) ⟹ (map F) :=
+{ app := λ ℱ, 
+  { f := 𝟙 ℱ.X,
+    c := { app := λ U, (α.app _) ≫ G.map (ℱ.𝒪.map (((open_set.map_id ℱ.X).symm U).hom)),
+           naturality' := sorry }
+  }, 
+  naturality' := sorry }
+
+def map₂_id {F : C ⥤ D} : map₂ (nat_trans.id F) = nat_trans.id (map F) := sorry
+def map₂_vcomp {F G H : C ⥤ D} (α : F ⟹ G) (β : G ⟹ H) : map₂ β ⊟ map₂ α = map₂ (α ⊟ β) := sorry
+end
 
-def map₂ {F G : C ⥤ D} (α : F ⟹ G) : (map F) ⟹ (map G) :=
-{ app := begin end, }
+section
+variables (C : Type u) [𝒞 : category.{u v} C]
+include 𝒞
+def map_id : (map (functor.id C)) ≅ functor.id (Presheaf.{u v} C) :=  sorry
+end
+
+section
+variables {C : Type u} [𝒞 : category.{u v} C] {D : Type u} [𝒟 : category.{u v} D] {E : Type u} [ℰ : category.{u v} E]
+include 𝒞 𝒟 ℰ
+def map_comp (F : C ⥤ D) (G : D ⥤ E) : (map F) ⋙ (map G) ≅ map (F ⋙ G) := 
+{ hom := sorry,
+  inv := sorry,
+  hom_inv_id' := sorry,
+  inv_hom_id' := sorry }
+
+def map₂_hcomp {F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟹ G) (β : H ⟹ K) : ((map₂ α ◫ map₂ β) ⊟ (map_comp F H).hom) = ((map_comp G K).hom ⊟ (map₂ (α ◫ β))) :=
+sorry
+end
 
 end Presheaf
 
+
 end category_theory.presheaves