Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# kbuzzard/presheaf.lean

Last active Dec 23, 2019
problems with pulling back presheaves
 /- Theory of presheaves (of objects of a category) on a topological space cf : https://stacks.math.columbia.edu/tag/006D Notes: KMB has never really understood whether we should be using category theory or not when working with sheaves on a topological space. By explicitly avoiding this and doing everything from first principles on the topological space side, but letting sheaves take values which are objects of a general category is certainly something we want to do. This is just really an exercise for KB to learn how to use the category theory library. -/ import category_theory.full_subcategory import category_theory.limits.limits -- random import import topology.opens import topology.sheaves.presheaf open category_theory open topological_space universes v u -- Homs in C and the top space will be in the same universe v ("sets"). -- when I hover over 𝟙 I don't get the keyboard shortcut /-- Definition of a presheaf -/ structure topological_space.presheaf (X : Type v) [topological_space X] (C : Type u) [𝒞 : category.{v} C] := (val : Π (U : opens X), C) -- ℱ (res : ∀ (U V) (HVU : V ⊆ U), val U ⟶ val V) (Hid : ∀ (U), res U U (set.subset.refl U) = 𝟙 (val U)) (Hcomp : ∀ (U V W) (HWV : W ⊆ V) (HVU : V ⊆ U), res U W (set.subset.trans HWV HVU) = res U V HVU ≫ res V W HWV) open topological_space lattice namespace topological_space.presheaf variables {C : Type u} [𝒞 : category.{v} C] variables {X : Type v} [topological_space X] include 𝒞 -- I don't know why they used (U V), this changes it to {U V} def res' : ∀ (ℱ : presheaf X C) {U V : opens X} (HVU : V ⊆ U), ℱ.val U ⟶ ℱ.val V := res instance : has_coe_to_fun (topological_space.presheaf X C) := { F := λ ℱ, opens X → C, coe := topological_space.presheaf.val} -- simp lemma to get ℱ.val U back into ℱ U form @[simp] lemma val_eq_coe {ℱ : presheaf X C} {U : opens X} : ℱ.val U = ℱ U := rfl -- Simplification lemmas for Hid and Hcomp. @[simp] lemma Hcomp' (ℱ : presheaf X C) : ∀ (U V W : opens X) (HWV : W ⊆ V) (HVU : V ⊆ U), (ℱ.res _ _ (set.subset.trans HWV HVU)) = (ℱ.res _ _ HVU) ≫ (ℱ.res _ _ HWV) := λ U V W HWV HVU, by rw ℱ.Hcomp _ _ _ HWV HVU; simp @[simp] lemma Hid' (ℱ : presheaf X C) : ∀ (U : opens X), (ℱ.res _ _ (set.subset.refl U)) = 𝟙 (ℱ U) := λ U, begin rw ℱ.Hid U, dunfold coe_fn has_coe_to_fun.coe, -- why refl no work? simp, end -- presheaves are a category. structure morphism (ℱ 𝒢 : presheaf X C) := (map : ∀ (U), ℱ U ⟶ 𝒢 U) (commutes : ∀ (U V) (HVU : V ⊆ U), (map U) ≫ (𝒢.res U V HVU) = (ℱ.res U V HVU) ≫ (map V)) variables {ℱ 𝒢 : presheaf X C} -- notation instance : has_hom (presheaf X C) := ⟨morphism⟩ namespace morphism instance : has_coe_to_fun (morphism ℱ 𝒢) := { F := λ φ, Π (U : opens X), ℱ U ⟶ 𝒢 U, coe := λ φ, φ.map} def commutes' (φ : ℱ ⟶ 𝒢): ∀ {U V : opens X} (HVU : V ⊆ U), φ U ≫ 𝒢.res' HVU = ℱ.res' HVU ≫ φ V := φ.commutes @[ext] def ext (φ ψ : ℱ ⟶ 𝒢) : (φ : ∀ (U : opens X), ℱ U ⟶ 𝒢 U) = ψ → φ = ψ := begin intro h, -- how am I supposed to be doing this? This is too CS for me :-/ cases φ, cases ψ, unfold_coes at h, dsimp at h, simp [h], end end morphism --#check morphism.commutes' -- Morphism of presheaves. instance category_struct : category_struct (presheaf X C) := { hom := morphism,--∀ ℱ 𝒢 (U), ℱ U ⟶ 𝒢 U), id := λ ℱ, { map := λ U, 𝟙 (ℱ U), commutes := begin intros U V HVU, cases V, cases U, dsimp at *, simp at *, end }, -- is there a better tactic? comp := λ ℱ 𝒢 ℋ φ ψ,{ map := λ U, (φ U) ≫ (ψ U),--begin sorry end,--λ U, φ U ≫ ψ U, commutes := begin intros, -- I surely want automation to do this. show (φ U ≫ ψ U) ≫ ℋ.res' HVU = ℱ.res' HVU ≫ φ V ≫ ψ V, rw category.assoc, have X1 := φ.commutes', have Xφ := X1 HVU, have X2 := ψ.commutes', have Xψ := X2 HVU, rw ψ.commutes', rw ←category.assoc, -- tidy just makes everything explode at this point rw φ.commutes', apply category.assoc, end} } instance category : category (presheaf X C) := { id_comp' := begin -- what is the tactic? intros, ext, apply category.id_comp, end, comp_id' := begin intros, ext, apply category.comp_id, end, assoc' := begin intros, ext, apply category.assoc, end, ..topological_space.presheaf.category_struct } -- Equality lemma lemma presheaf_eq_of_subset_eq (ℱ : presheaf X C) (U V : opens X) : U = V → ℱ U = ℱ V := λ h, by simp [h] end topological_space.presheaf -- 𝟙 is \b1 and 𝟭 who knows /-! pushforwards and pullbacks for presheaves and maybe sheaves too -/ open topological_space lattice category_theory variables {X Y : Type v} [topological_space X] [topological_space Y] variables {C : Type u} [𝒞 : category.{v} C] variables (f : X → Y) (hf : continuous f) include 𝒞 instance : preorder (opens X) := by apply_instance --instance : small_category (opens X) := by apply_instance -- :-( -- wrong way def small_category {α : Type v} [preorder α] : small_category α := { hom := λ U V, ulift (plift (V ≤ U)), id := λ X, ⟨ ⟨ le_refl X ⟩ ⟩, comp := λ _ _ _ f g, ⟨ ⟨ le_trans g.down.down f.down.down ⟩ ⟩ } -- need to beat 100 to have an effect local attribute [instance, priority 200] small_category --instance : category (presheaf X C) := topological_space.presheaf.category --instance foo : category (presheaf Y C) := topological_space.presheaf.category --set_option trace.class_instances true def map (f : X → Y) (hf : continuous f) : presheaf X C ⥤ presheaf Y C := { obj := λ ℱ, { val := λ _, ℱ (hf.comap _), res := λ _ _ hV, ℱ.res' (λ _ hv, hV hv), Hid := λ _, ℱ.Hid _, Hcomp := λ _ _ _ _ _, ℱ.Hcomp _ _ _ _ _}, map := λ ℱ 𝒢 φ,{ map := λ V, φ (continuous.comap hf V), commutes := λ _ _ _, φ.commutes _ _ _}, map_id' := by intros; split, map_comp' := by intros; split } -- todo: pushforward of a sheaf should be a sheaf --example (X Y : Type) {f : X → Y} -- (U : set X) (V : set Y) : f '' U ⊆ V ↔ U ⊆ f ⁻¹' V := easy namespace topological_space.presheaf /-- The functor induced by ℱ on the opens containing a subset of X -/ def to_aux_functor (ℱ : presheaf X C) (Y : set X) : {V : opens X // Y ⊆ V} ⥤ C := { obj := λ V, ℱ V, map := λ V₁ V₂ j, ℱ.res' j.1.1, map_id' := λ _, ℱ.Hid _, map_comp' := λ _ _ _ _ _, ℱ.Hcomp _ _ _ _ _} -- I should only need filtered colimits variable [limits.has_colimits.{v} C] def aux_cocone (ℱ : presheaf X C) (Y : set X) : limits.cocone (ℱ.to_aux_functor Y) := limits.colimit.cocone (ℱ.to_aux_functor Y) def aux_colimit (ℱ : presheaf X C) (Y : set X) : C := (ℱ.aux_cocone Y).X def res_functor {Y₁ Y₂ : set X} (hY : Y₂ ⊆ Y₁) : {V : opens X // Y₁ ⊆ V} ⥤ {V : opens X // Y₂ ⊆ V} := { obj := λ V, ⟨V.1, set.subset.trans hY V.2⟩, map := λ _ _, id} example (ℱ : presheaf X C) {Y₁ Y₂ : set X} (hY : Y₂ ⊆ Y₁) : res_functor hY ⋙ ℱ.to_aux_functor Y₂ = ℱ.to_aux_functor Y₁ := rfl -- :-) example (Y : set X) : res_functor (set.subset.refl Y) ≅ 𝟭 _ := begin /- `tidy` says -/ fsplit, { fsplit, { intros X_1, cases X_1, cases X_1_val, dsimp at *, fsplit, dsimp at *, fsplit, intros a a_1, assumption }, { intros X_1 Y_1 f, refl}}, { fsplit, { intros X_1, cases X_1, cases X_1_val, dsimp at *, fsplit, dsimp at *, fsplit, intros a a_1, assumption }, { intros X_1 Y_1 f, refl }}, { apply_auto_param }, { apply_auto_param } end example (Y : set X) : res_functor (set.subset.refl Y) = 𝟭 _ := begin unfold res_functor, unfold category_theory.functor.id, simp, refl, end example (C D E : Type*) [𝒞 : category C] [𝒟 : category D] [ℰ : category E] (F G : C ⥤ D) (H : D ⥤ E) (h : F ≅ G) : (F ⋙ H) ≅ (G ⋙ H) := iso_whisker_right h H #check limits.colimit.pre /- category_theory.limits.colimit.pre : Π {J K : Type v} [_inst_1 : small_category J] [_inst_2 : small_category K] {C : Type u} [𝒞 : category_theory.category C] (F : J ⥤ C) [_inst_3 : limits.has_colimit F] (E : K ⥤ J) [_inst_4 : limits.has_colimit (E ⋙ F)], limits.colimit (E ⋙ F) ⟶ limits.colimit F -/ --example {J K : Type v} [_inst_1 : small_category J] --[small_category K] {C : Type u} [𝒞 : category_theory.category C] (F : J ⥤ C) --[limits.has_colimit F] (E₁ E₂ : K ⥤ J) [limits.has_colimit (E₁ ⋙ F)] [limits.has_colimit (E₂ ⋙ F)] --(h : E₁ = E₂) : limits.colimit.pre F E₁ = limits.colimit.pre F E₂ := sorry #check limits.colimit.desc set_option pp.proofs true --set_option trace.simplify.rewrite true def comap {f : X → Y} (hf : continuous f) : presheaf Y C ⥤ presheaf X C := { obj := λ ℱ, { val := λ U, ℱ.aux_colimit (f '' U), res := λ U₁ U₂ hU, limits.colimit.pre (ℱ.to_aux_functor _) (res_functor \$ set.image_subset _ hU), Hid := λ U, begin show limits.colimit.pre (to_aux_functor ℱ (f '' U.val)) (res_functor _) = 𝟙 (aux_colimit ℱ (f '' ↑U)), have h : res_functor (set.subset.refl (f '' U.val)) = 𝟭 _, unfold res_functor, unfold category_theory.functor.id, simp, refl, have h' : res_functor (set.image_subset f (set.subset.refl ↑U)) = 𝟭 _, unfold res_functor, unfold category_theory.functor.id, simp, refl, unfold limits.colimit.pre, dsimp, ext V, dsimp, -- simp only [h'], -- fails sorry end, Hcomp := begin sorry end }, map := λ ℱ 𝒢 φ, { map := λ U, sorry, commutes := sorry }, map_id' := sorry, map_comp' := sorry } end topological_space.presheaf
to join this conversation on GitHub. Already have an account? Sign in to comment