-
Notifications
You must be signed in to change notification settings - Fork 297
/
plus.lean
39 lines (28 loc) · 1.12 KB
/
plus.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
import topology.Top.presheaf.cech
universes v u
open category_theory
open category_theory.limits
open topological_space
open opposite
namespace Top
variables {X : Top.{v}}
def foo {U V : (opens X)ᵒᵖ} (h : U ⟶ V) : covers_of (unop U) ⥤ covers_of (unop V) := sorry
def bar {U V : (opens X)ᵒᵖ} (h : U ⟶ V) : (foo h ⋙ covers_of.forget (unop V)) ⟶ covers_of.forget (unop U) := sorry
variables {C : Type u} [𝒞 : category.{v+1} C]
include 𝒞
variables [has_limits.{v} C] [has_colimits.{v} C]
def plus_obj_obj (ℱ : X.presheaf C) (U : (opens X)ᵒᵖ) : C :=
colimit.{v} ((covers_of.forget (unop U)).op ⋙ ℱ.cech_zero)
def plus_obj_map (ℱ : X.presheaf C) (U V : (opens X)ᵒᵖ) (h : U ⟶ V) : plus_obj_obj ℱ U ⟶ plus_obj_obj ℱ V :=
begin
let p :=
limits.colim.{v}.map (whisker_right (nat_trans.op (bar h)) ℱ.cech_zero),
-- TODO need to use `functor.op_comp`.
-- exact p ≫ colimit.pre ((covers_of.forget (unop U)).op ⋙ ℱ.cech_zero) _
end
def plus_obj (ℱ : X.presheaf C) : X.presheaf C :=
{ obj := plus_obj_obj ℱ,
map := plus_obj_map ℱ,
map_id' := sorry,
map_comp' := sorry }
end Top