Zulip Chat Archive

Stream: maths

Topic: Sheaves


view this post on Zulip Kevin Buzzard (Jun 10 2019 at 14:55):

Kenny and I have been playing about with the schemes repo; I've been trying to glue sheaves together on subspaces. I realise when doing this work that there are big design decisions that need to be made. A sheaf in maths is just some assignment of a type to each open subset of a topological space, modulo a bit of extra structure and some axioms. I'd been working with opens X but now I'm working with sheaves on open subsets of X I am forever wrestling with opens U with U : opens X and having to dig through subtypes of subtypes etc. Sure I could write a bunch of API for opens U. On the other hand I could just try and avoid subtypes completely -- this was @Kenny Lau 's suggestion -- and even go so far as to define a sheaf on an open subspace of a topological space just to be pair (U,F) where U is open, F is a sheaf on all of X, and the values of F are irrelevant if we evaluate on a set that isn't an open subset of U. This seems to be leading to some sort of "how to do this sort of thing optimally in dependent type theory" conversation and it reminds me a lot of @Assia Mahboubi using subgroups instead of groups in Coq (the rooster and the butterfly) and so on. Doing it like this, the restriction of F to an open subspace is very very easy indeed.

On the other hand, my plan has always been to use @Scott Morrison 's category theory work to do sheaves, as this is the language which is used in practice by mathematicians. However in some sense I now feel that this would drift even further from the "very easy" approach and force me to write even more API. I do not object to writing more API. But I'm just confused about the best approach to take. Scott's approach seems to be far closer to what a mathematician would do, and Kenny's to what a computer scientist would do. I don't know which one I want to be though, in this context. I somehow get the feeling that it matters though.

view this post on Zulip Kenny Lau (Jun 10 2019 at 14:56):

I'm proud of my construction :P

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:00):

It makes no mathematical sense :P

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:01):

It feels a bit like this weird idea of defining a subset to be compact instead of defining what it means for a top space to be compact.

view this post on Zulip Reid Barton (Jun 10 2019 at 15:05):

I don't know how feasible this is in this case but maybe you can pick an application which needs gluing of sheaves--fiber products maybe--and imagine (if not actually carry out) the construction using the interface you intend to provide

view this post on Zulip Reid Barton (Jun 10 2019 at 15:06):

Well I guess gluing schemes is a bit more work than gluing sheaves

view this post on Zulip Simon Pepin Lehalleur (Jun 10 2019 at 15:53):

It makes no mathematical sense :P

Couldn't you identify a sheaf on U with either its extension by zero or push-forward to X? They both make a lot of mathematical sense , and they are fully faithful functors so that you don't lose any information.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 16:02):

Indeed! But in this game people might equally want to just say "what is going on outside U is junk". The extension by zero would be hard to work with in Lean -- the definition would then be "if V is a subset of U then the correct thing, else 0", and you would forever be splitting ifs. The pushforward is easier because its value on V is the correct value on V intersect U, so you are just having to invoke the fact that the intersection of two opens is open occasionally, which sounds nicer. What I am frustrated about is that both of them seem to be slightly artificial workarounds for the thing I want to have, which is the sheaf on U and nothing more. My question is whether I should bite the bullet and work with the thing that seems right to me or make these artificial extensions. Even with the extensions one has to choose whether to prove that the sheaf axiom holds for the extension or just check it on U.

Hmm. Here's another issue. What I want to be easy is this: given X a top space, and F a sheaf on U (an open subset of X) and V an open subset of U, I want the restriction of F to V. With my suggestion ("junk outside U") I can literally use F again, With either the pushforward (they call it map here) or extension by zero one would have to change F. What I have no real feeling about is whether the convenience of being able to recycle F is worth anything, or whether I should just bite the bullet, write some code which does what I want "properly" (i.e. a sheaf on U is just a function on the open subsets of U and hang the other open subsets of X) and then just figure out the API I need. I might need a lot of API. But this is not a mathematical issue, it is a tedious implementation issue.

view this post on Zulip Johan Commelin (Jun 10 2019 at 16:29):

@Simon Pepin Lehalleur Welcome on the chat!

view this post on Zulip Simon Pepin Lehalleur (Jun 10 2019 at 16:35):

@Johan Commelin Thanks! I saw the mathoverflow question and I got curious...

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:25):

I don't believe "extension by zero" makes sense mathematically.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:27):

I've just spent another 20 minutes struggling to even write down the definition of glueing sheaves. The mathematical argument is: you have a topological space XX covered by opens UiU_i, and for each ii you have a sheaf Fi\mathcal{F}_i on UiU_i. Say you have isomorphisms ϕij:Fi(UiUj)Fj(UiUj)\phi_{ij}:\mathcal{F}_i|(U_i\cap U_j)\to\mathcal{F}_j|(U_i\cap U_j) of sheaves satisfying the cocycle condition ϕik=ϕjkϕij\phi_{ik}=\phi_{jk}\circ\phi_{ij} as maps of sheaves on UiUjUkU_i\cap U_j\cap U_k, and such that ϕii\phi_{ii} is the identity. Then we want a sheaf on all of XX.

Even writing down the definition of F(U)\mathcal{F}(U) is a pain. It involves taking the elements (ti)iFi(UUi)(t_i)\in\prod_i\mathcal{F_i}(U\cap U_i) which agree on overlaps; however the way @Ramon Fernandez Mir has set up sheaves is with categories in mind, so we have U: opens X and so to make the tit_i we need U ∩ U_i : opens U_i and then to say "agree on overlaps" it becomes a bit of a nightmare.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:27):

I don't believe "extension by zero" makes sense mathematically.

Sure it does; it's a sheaf, not vector bundle. Its fibre is 0 outside U.

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:28):

what does "agree on overlaps" even mean in the Hartshorn exercise?

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:28):

I don't believe "extension by zero" makes sense mathematically.

Sure it does; it's a sheaf, not vector bundle. Its fibre is 0 outside U.

then isn't it just the same as the pushforward

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:28):

No -- the pushforward you're allowed poles outside U.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:30):

Agree on overlaps: mathematically it's easy to say. I want ϕij\phi_{ij} to send (the restriction of tit_i to UUiUjU\cap U_i\cap U_j) to (the restriction of tjt_j to UUiUjU\cap U_i\cap U_j)

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:31):

but isn't it also a philosophy in maths that we don't talk about equality / subset relations between two unrelated sets / groups / rings?

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:31):

I'm using ϕij\phi_{ij} -- that's the glue.

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:32):

oh right we're gluing along an isomorphism

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:32):

the problem with formalising all this in Lean is that I have all these terms of type open A and I want them to be of type open B so I seem to be forever writing explicit results going from one random open set in some space to another random open set in another space.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:33):

On the tube home I tried implementing your solution Kenny, but this seems to involve rewriting all definitions of sheaves and presheaves.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:34):

Because now I want to talk about a top space X, and an open subset U, and a sheaf-on-U, which takes as input an open subset of X and a proof that it's a subset of U, and spits out a ring, and now the sheaf axiom etc all need to be redone in this context.

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:34):

gluing-vs-glueing

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:34):

Also maybe it's time to care about spelling

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:34):

As I said before, it feels very much like Assia's approach to proving Zassenhaus by having every group living in a bigger group

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:35):

ok I'll try formulating the statement

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:35):

In which context?

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:35):

It seems to me that there is a big design decision to be made here.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:36):

Sheaves-on-an-open-subset, or go full category, or this type-theory-friendly approach which involves defining "sheaf on U" as "sheaf on X except not quite"

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:37):

well I still stand by my approach :P

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:37):

I suspect you want to do the type-theory-friendly approach, but in some sense this brings into question Ramon's very definition of a sheaf.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:38):

Does one then have two definitions of a sheaf? Sheaf-on-a-subset and then you define sheaf to be sheaf-on-a-subset-but-the-subset-is-X? And then you have to supply lots of proofs of X \subseteq X everywhere?

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:38):

def sheaf_on_open_subset (X : Type u) [topological_space X] (U : opens X) : Type (max u (v+1)) :=
sheaf.{u v} X

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:46):

You'll get laughed at in the maths department

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:52):

import sheaves.sheaf

universes v u w

open topological_space

def sheaf_on_opens (X : Type u) [topological_space X] (U : opens X) : Type (max u (v+1)) :=
sheaf.{u v} X

namespace sheaf_on_opens

variables {X : Type u} [topological_space X] {U : opens X}

def eval (F : sheaf_on_opens X U) (V : opens X) (HVU : V  U) : Type v :=
presheaf.F (sheaf.F F) V

def res (F : sheaf_on_opens X U) (V : opens X) (HVU : V  U) (W : opens X) (HWU : W  U) (HWV : W  V) : F.eval V HVU  F.eval W HWU :=
presheaf.res _ _ _ HWV

def res_subset (F : sheaf_on_opens X U) (V : opens X) (HVU : V  U) : sheaf_on_opens X V :=
F

structure morphism (F : sheaf_on_opens.{v} X U) (G : sheaf_on_opens.{w} X U) : Type (max u v w) :=
(map :  V  U, F.eval V H  G.eval V H)
(commutes :  (V : opens X) (HV : V  U) (W : opens X) (HW : W  U) (HWV : W  V) (x),
  map W HW (F.res V HV W HW HWV x) = G.res V HV W HW HWV (map V HV x))

end sheaf_on_opens

view this post on Zulip Kenny Lau (Jun 10 2019 at 17:53):

You'll get laughed at in the maths department

so maybe I should LaTeX the whole thing instead

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 17:53):

rofl. Hey, I would recommend not using two universes. Why not just use one?

view this post on Zulip Johan Commelin (Jun 11 2019 at 06:42):

@Kenny Lau Can you prove that f _* and f ^* are adjoint (with or without using category_theory/)?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 06:43):

We don't even have f^* apart from for open maps.

view this post on Zulip Johan Commelin (Jun 11 2019 at 06:44):

Sure... but a sheaves API without this adjunction is quite incomplete.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 06:44):

(maybe even only for open immersions)

view this post on Zulip Johan Commelin (Jun 11 2019 at 06:44):

Any decent approach to sheaves should at least give us sheafification and this adjunction.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 06:44):

And if we did it for sheaves of types you'd say it was incomplete because we didn't have it for sheaves of groups, rings, modules...

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 06:45):

There's still loads to do.

view this post on Zulip Johan Commelin (Jun 11 2019 at 06:45):

In the end, I don't care how we get there. (Implementation details, like you say.)

view this post on Zulip Johan Commelin (Jun 11 2019 at 06:45):

And if we did it for sheaves of types you'd say it was incomplete because we didn't have it for sheaves of groups, rings, modules...

No, not really. I can kind of see how we would bolt that on afterwards.

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 16:56):

I'm trying to make sense of what we have for sheaves. It's time I understood what has been done. There are (at least) four branches on mathlib:

Branch sheaf-2 of mathlib has sieves, grothendieck topologies and sheaves on a site.

Branch sheaf-old does not have a name which fills you with confidence.

Branch sheaf is 6000 lines of code.

Branch sheaves is some code @Scott Morrison wrote over the summer.

Do we have the assertion that pullback and pushforward of sheaves of abelian groups are adjoint functors on the category of open sets of a topological space?

Do we have the assertion that pullback and pushforward of sheaves of abelian groups are adjoint functors in the category of sheaves on a site?

Do we have any more general assertions about pullback and pushforward of sheaves of algebraic objects or other objects?

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 17:16):

@Johan Commelin you said you had trouble with this stuff. What is in mathlib? I can't even find the category of open sets of a topological space.

view this post on Zulip Reid Barton (Dec 14 2019 at 17:22):

That's in topology.category.Top.opens

view this post on Zulip Johan Commelin (Dec 14 2019 at 17:25):

Besides that, only the definition of a presheaf (on a topological space, I think) is in mathlib.

view this post on Zulip Reid Barton (Dec 14 2019 at 17:25):

I don't think we have anything about pullbacks anywhere

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 17:54):

Are there any PR's about sheaves?

view this post on Zulip Johan Commelin (Dec 14 2019 at 17:55):

Nope, don't think so

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:12):

Old gist of @Mario Carneiro :

/-
  Presheaf (of types).
  https://stacks.math.columbia.edu/tag/006D
-/

import topology.basic
import topology.opens
import order.bounds

universes u v

-- Definition of a presheaf.

open topological_space lattice

structure presheaf (α : Type u) [semilattice_inf α] :=
(F     : α  Type v)
(res   :  (U V) (HVU : V  U), F U  F V)
(Hid   :  (U), res U U (le_refl U) = id)
(Hcomp :  (U V W) (HWV : W  V) (HVU : V  U),
  res U W (le_trans HWV HVU) = res V W HWV  res U V HVU)

namespace presheaf

variables {α : Type u} [semilattice_inf α]

instance : has_coe_to_fun (presheaf α) :=
{ F := λ _, α  Type v,
  coe := presheaf.F }

-- Simplification lemmas for Hid and Hcomp.

@[simp] lemma Hcomp' (F : presheaf α) :
 (U V W) (HWV : W  V) (HVU : V  U) (s : F U),
  (F.res U W (le_trans HWV HVU)) s =
  (F.res V W HWV) ((F.res U V HVU) s) :=
λ U V W HWV HVU s, by rw F.Hcomp U V W HWV HVU

@[simp] lemma Hid' (F : presheaf α) :
 (U) (s : F U),
  (F.res U U (le_refl U)) s = s :=
λ U s, by rw F.Hid U; simp

def total (F : presheaf α) : Type (max u v) := Σ U, F.F U

instance (F : presheaf α) (U : α) : has_coe_t (F U) F.total :=
sigma.mk _⟩

@[elab_as_eliminator]
theorem total.cases_on (F : presheaf α) {C : F.total  Sort*}
  (x) (H :  U (x : F U), C x) : C x :=
by cases x; apply H

def res' (F : presheaf α) (V : α) : F.total  F.total
| U, x := F.res U (U  V) inf_le_left x

theorem res'_def (F : presheaf α) {U V} (x : F U) :
  F.res' V x = F.res U (U  V) inf_le_left x := rfl

theorem res'_val (F : presheaf α) {U V} (x : F U) (h : V  U) :
  F.res' V x = F.res U V h x :=
have  W (H : W  U), W = V 
  (F.res U W H x : F.total) = F.res U V h x :=
  by rintro _ _ rfl; refl,
this _ _ (inf_of_le_right h)

theorem res'_eq_inf (F : presheaf α) {U V} (x : F U) :
  F.res' V x = F.res' (U  V) x :=
by rw [res'_def,  res'_val _ _ inf_le_left]

theorem res'_eq_left (F : presheaf α) {U V W} (x : F U) (H : U  V = U  W) :
  F.res' V x = F.res' W x :=
by rw [res'_eq_inf, H,  res'_eq_inf]

@[simp] theorem res'_id {F : presheaf α} {U} (x : F U) : F.res' U x = x :=
by rw [res'_val _ _ (le_refl U), F.Hid]; refl

@[simp] theorem res'_comp {F : presheaf α} {U V} (x : F.total) :
  F.res' U (F.res' V x) = F.res' (U  V) x :=
total.cases_on F x $ λ W x,
by rw [res'_def, res'_def,  F.Hcomp',  res'_val, res'_eq_left];
   simp [inf_left_comm, inf_comm]

-- Morphism of presheaves.

-- Kenny wants morphisms on the subsheaves
structure morphism (F G : presheaf α) :=
(map      :  (U), F U  G U)
(commutes :  (U V) (HVU : V  U),
  (G.res U V HVU)  (map U) = (map V)  (F.res U V HVU))

infix `  `:80 := morphism

section morphism

def comp {F G H : presheaf α} (fg : F  G) (gh : G  H) : F  H :=
{ map := λ U, gh.map U  fg.map U,
  commutes := λ U V HVU,
    begin
      rw [function.comp.assoc, gh.commutes U V HVU], symmetry,
      rw [function.comp.assoc, fg.commutes U V HVU]
    end }

infix `  `:80 := comp

def id (F : presheaf α) : F  F :=
{ map := λ U, id,
  commutes := λ U V HVU, by simp, }

structure iso (F G : presheaf α) :=
(mor : F  G)
(inv : G  F)
(mor_inv_id : mor  inv = id F)
(inv_mor_id : inv  mor = id G)

infix `  `:80 := iso

end morphism

section sheaf_condition

-- Sheaf condition.

def locality (F : presheaf α) :=
 {{U S}}, is_lub S U   {{s t : F U}},
  ( V  S, F.res' V s = F.res' V t)  s = t

def gluing (F : presheaf α) :=
 {{U : α}} {{S}}, is_lub S U   (s : Π V : S, F V),
  ( V W : S, res' F (V  W) (s V) = res' F (V  W) (s W)) 
   x : F U,  V:S, F.res' V x = s V

def is_sheaf (F : presheaf α) :=
locality F  gluing F

end sheaf_condition

end presheaf

structure semilattice_inf_hom
  (α β : Type*) [semilattice_inf α] [semilattice_inf β] :=
(to_fun : α  β)
(mono : monotone to_fun)
(map_inf' :  a b, to_fun (a  b) = to_fun a  to_fun b)

namespace semilattice_inf_hom

infixr `  `:25 := semilattice_inf_hom

instance {α β : Type*} [semilattice_inf α] [semilattice_inf β] :
  has_coe_to_fun (α  β) := ⟨_, to_fun

@[simp] theorem map_inf {α β : Type*} [semilattice_inf α] [semilattice_inf β]
  (f : α  β) (a b : α) : f (a  b) = f a  f b := map_inf' _ _ _

def id {α : Type*} [semilattice_inf α] : α  α :=
id, monotone_id, λ _ _, rfl

def comp {α β γ : Type*} [semilattice_inf α] [semilattice_inf β] [semilattice_inf γ]
  (g : β  γ) (f : α  β) : α  γ :=
g  f, monotone.comp g.mono f.mono, λ a b, by simp

end semilattice_inf_hom

structure semilattice_inf_lub_emb
  (α β : Type*) [semilattice_inf α] [semilattice_inf β] extends α  β :=
(inj : function.injective to_fun)
(map_lub :  {{S a}}, is_lub S a  is_lub (to_fun '' S) (to_fun a))

namespace semilattice_inf_lub_emb

infixr ` ↪⊓⨆ `:25 := semilattice_inf_lub_emb

instance {α β : Type*} [semilattice_inf α] [semilattice_inf β] :
  has_coe (α ↪⊓⨆ β) (α  β) := to_semilattice_inf_hom

@[simp] theorem map_inf {α β : Type*} [semilattice_inf α] [semilattice_inf β]
  (f : α ↪⊓⨆ β) (a b : α) : f (a  b) = f a  f b := f.map_inf' _ _

def id {α : Type*} [semilattice_inf α] : α ↪⊓⨆ α :=
semilattice_inf_hom.id, function.injective_id,
  λ S a h, by simp [semilattice_inf_hom.id, h]

def comp {α β γ : Type*} [semilattice_inf α] [semilattice_inf β] [semilattice_inf γ]
  (g : β ↪⊓⨆ γ) (f : α ↪⊓⨆ β) : α ↪⊓⨆ γ :=
(g : β  γ).comp f, function.injective_comp g.inj f.inj,
  λ S a h, by have := g.map_lub (f.map_lub h); rwa [set.image_image] at this

end semilattice_inf_lub_emb

namespace presheaf

variables {α : Type*} {β : Type*} [semilattice_inf α] [semilattice_inf β]

def comap (f : α  β) (F : presheaf β) : presheaf α :=
{ F := λ a, F (f a),
  res := λ a b h, F.res _ _ (f.mono h),
  Hid := λ a, F.Hid _,
  Hcomp := λ a b c bc ab, F.Hcomp _ _ _ _ _ }

theorem comap_res (f : α  β) (F : presheaf β) (a b h) :
  (F.comap f).res a b h = F.res _ _ (f.mono h) := rfl

instance (f : α  β) (F : presheaf β) : has_coe (F.comap f).total F.total :=
⟨λ x, ⟨_, x.2⟩⟩

theorem comap_coe_inj (f : α  β) (F : presheaf β) (h : function.injective f) :
  function.injective (coe : (F.comap f).total  F.total)
| a, x b, y e := by cases h (congr_arg sigma.fst e:_); cases e; refl

@[simp] theorem coe_total_coe
  (f : α  β) (F : presheaf β) (U : α) (x : (F.comap f) U) :
  ((x : (F.comap f).total) : F.total) = @coe (F (f U)) _ _ x := rfl

theorem comap_res' (f : α  β) (F : presheaf β) (U : α) (x : (F.comap f).total) :
  ((F.comap f).res' U x) = F.res' (f U) x :=
total.cases_on (F.comap f) x $ λ W x,
by rw [res'_def, coe_total_coe, coe_total_coe, comap_res,  res'_val, f.map_inf,
        res'_eq_inf]

end presheaf

structure sheaf (α : Type u) [semilattice_inf α] extends presheaf α :=
(locality : to_presheaf.locality)
(gluing   : to_presheaf.gluing)

structure sheaf_of_rings (α : Type u) [semilattice_inf α] extends sheaf α :=
[ring' :  U, ring (F U)]
[ring_hom :  U V h, is_ring_hom (res U V h)]

namespace sheaf

variables {α : Type*} {β : Type*} [semilattice_inf α] [semilattice_inf β]

def total (F : sheaf α) := F.to_presheaf.total

def res' (F : sheaf α) : α  F.total  F.total := F.to_presheaf.res'

instance : has_coe_to_fun (sheaf α) :=
{ F := λ _, α  Type v,
  coe := λ F, F.to_presheaf }

instance (F : sheaf α) (U : α) : has_coe_t (F U) F.total :=
sigma.mk _⟩

def comap (f : α ↪⊓⨆ β) (F : sheaf β) : sheaf α :=
{ locality := λ a S lub (s t : F (f a)) H, F.locality (f.map_lub lub) begin
    rintro _ b, hb, rfl,
    let G := F.to_presheaf.comap (f : α  β),
    have : G.res' b (@coe (G a) _ _ s) =
           G.res' b (@coe (G a) _ _ t) := H b hb,
    have H1 := F.to_presheaf.comap_res' (f : α  β) b _,
    rw [this, F.to_presheaf.comap_res' (f : α  β) b] at H1,
    simp at H1, exact H1.symm
  end,
  gluing := λ a S lub (g :  U : S, F (f U)), begin
    let G := F.to_presheaf.comap (f : α  β),
    change ∀_:  V W : S, G.res' (V  W) (@coe (G V) _ _ (g V)) =
                          G.res' (V  W) (@coe (G W) _ _ (g W)),
       U : F (f a),  V : S, G.res' V (@coe (G a) _ _ U) = @coe (G V) _ _ (g V),
    choose k hk using show  V : f '' S,  U : S, (V:β) = f U,
    by rintro ⟨_, U, hU, rfl⟩; exact ⟨⟨U, hU, rfl,
    let g' :  V : f '' S, F (V:β) := λ V, by rw hk V; exact g (k V),
    have g'eq :  U (hU : U  S), (g' f U, U, hU, rfl : F.total) = g U, hU,
    { intros,
      suffices :  U' (h' : U' = k f U, _⟩),
        (by rw h'; exact g (k f U, U, hU, rfl) : F (f U')) = g U',
      { congr, exact this U, hU (subtype.eq (f.inj (hk f U, _⟩))) },
      rintro _ rfl, refl },
    intro h,
    cases F.gluing (f.map_lub lub) g' _ with z hz,
    { use z, rintro U, hU,
      apply presheaf.comap_coe_inj _ _ f.inj,
      rw [presheaf.comap_res'],
      exact (hz ⟨_, U, hU, rfl).trans (g'eq _ _) },
    { rintro ⟨_, V, hV, rfl ⟨_, W, hW, rfl,
      have := congr_arg coe (h V, hV W, hW),
      rw [presheaf.comap_res', presheaf.comap_res'] at this,
      simp at this, rwa [ g'eq,  g'eq] at this }
  end,
  ..F.to_presheaf.comap f.to_semilattice_inf_hom }

end sheaf

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:15):

I am trying to read topology/category/Top/opens.lean and I can't tell the difference between usual Lean function arrow and category theory very-slightly-longer-in-my-current-font arrow. I'm on Ubuntu. Does anyone have any recommendations for a font where I will be more easily able to see the difference between the two kinds of morphism?

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:16):

In VScode I don't have any trouble. (They also have different colours.)

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:16):

Dependent type theory is a bit like concrete categories, and I am beginning to see the point of abstract categories slowly and surely thanks to the continued efforts of @Scott Morrison calmly telling me that this is actually going to be a good way to do sheaves

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 19:17):

In VS Code they are indistinguishable to my eyes and I've even got my glasses on

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:17):

Hmm, that's annoying. I don't really have a good font recommendation... sorry

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:18):

Maybe the safe thing to do is assume that all arrows belong to some category.

view this post on Zulip Johan Commelin (Dec 14 2019 at 19:18):

And sometimes the category is Type

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 21:15):

https://github.com/ramonfmir/lean-scheme/blob/sheaves_of_categories/src/sheaves_of_categories/sheaf.lean

There's a definition of a sheaf on a topological space taking values in a category. @Ramon Fernandez Mir had locality and gluing but it seems to me that these just claim that a certain morphism is monic and epic. The sheaf axiom, I believe, is
that it is an isomorphism.

I was playing around at the end and ran into two sorrys. Is there a cute way of solving them @Reid Barton ? I don't know what I'm doing really. My definition of sheaf is that a certain fork is a limit (an equalizer).

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:26):

That definition seems right

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:27):

@Kevin Buzzard Huh, wait? How are to_fork and map_to_equalizer related?

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:27):

Because the sheaf axiom says that one of them is an iso, and then you want to prove that the other is an iso...

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 22:14):

map_to_equalizeris the morphism from F(U)\mathcal{F}(U) to the equalizer of iF(Ui)j,kF(UjUk)\prod_i\mathcal{F}(U_i)\to\to\prod_{j,k}\mathcal{F}(U_j\cap U_k)

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 22:16):

where the two arrows just mean I have an equalizer diagram. And to_fork produces the entire cone.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 22:33):

def is_sheaf' ( : sheaf X C) {U : opens X} (OC : covering U) :
  .to_presheaf.to_fork OC 
    (limit.cone (parallel_pair (.to_presheaf.res_left OC) (.to_presheaf.res_right OC))) :=
is_limit.unique_up_to_iso (.is_limit OC) (limit.is_limit _)

This has come out really nicely now. I've persevered with universes and now it's all beginning to work.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 22:44):

OK so I think that in the sheaves_of_categories branch of the schemes repo I have defined a sheaf of categories on a top space in the "lowbrow" way (a function on opens X).

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 23:44):

structure sheaf (X : Type v) [topological_space X] (C : Type u) [category.{v} C]
  [has_products.{v} C] [has_equalizers.{v} C]
extends presheaf X C :=
(is_limit :  {U : opens X} (OC : covering U),
   is_limit (topological_space.presheaf.to_fork to_presheaf OC))

Doing it this way, is_limit seems to be data, so sheaf X C is not a full subcategory of presheaf X C; however it is a subsingleton, so maybe it is. Should I make presheaf.is_sheaf or something? Presheaves are a category and I want to make sheaves a category. Hey @Kenny Lau I am doing sheaves of categories in the schemes repo. Next it's pushforward and pullbacks I think...

view this post on Zulip Kenny Lau (Dec 16 2019 at 23:44):

nice

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 23:50):

I think I want to make the fully faithful functor from sheaves to presheaves

view this post on Zulip David Michael Roberts (Dec 17 2019 at 00:04):

Sheaf of categories or sheaves valued in a given category?

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 00:05):

Yes, sheaves valued in a given category. Sorry.

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 00:34):

I don't quite know what to make of the fact that given a presheaf, the assertion that it is a sheaf seems to be data rather than a proposition.

view this post on Zulip David Michael Roberts (Dec 17 2019 at 01:18):

Hmm, yes. Is being a limit a proposition? Or is the data of the cone over the diagram nontrivial?

view this post on Zulip Kevin Buzzard (Dec 17 2019 at 01:27):

In Lean it seems that it's a subsingleton but data shrug

view this post on Zulip Johan Commelin (Dec 17 2019 at 05:29):

@Kevin Buzzard There is some stuff about induced_category. If your type is a subtype, this gives you a full subcategory. In your setup, you would get "merely" a fully faithful functor. Of course those are math-equal.
All you need to do is feed the projection function from sheaves to presheaves into induced_category.

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:11):

Johan Commelin said:

Kevin Buzzard There is some stuff about induced_category. If your type is a subtype, this gives you a full subcategory. In your setup, you would get "merely" a fully faithful functor. Of course those are math-equal.
All you need to do is feed the projection function from sheaves to presheaves into induced_category.

Oh I didn't realise this was already a topic! I actually did exactly what's suggested here before reading this :)

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:12):

That's frustrating! By the way since you were looking in the repo a while ago, I've merged a whole bunch of stuff into master and also cleaned up a few things so it might be a bit more understandable; and I've updated the readme

view this post on Zulip Reid Barton (Jun 02 2020 at 14:15):

One thing which is definitely required is a description of surjections in the category of sheaves

view this post on Zulip Patrick Massot (Jun 02 2020 at 14:15):

I don't to be vulgar, but what about sheaves on a space?

view this post on Zulip Reid Barton (Jun 02 2020 at 14:16):

I think this isn't so easy to recover from only the above information about sheafification

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:16):

Sheaves on a space is an easy special case of sheaves on a site! I can add this explicitly but there's not really much to it

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:19):

Reid Barton said:

One thing which is definitely required is a description of surjections in the category of sheaves

To clarify do you mean https://stacks.math.columbia.edu/tag/00WL?

view this post on Zulip Reid Barton (Jun 02 2020 at 14:21):

Yes, I mean exactly this word "Omitted"

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:29):

@Bhavik Mehta What will be very important is

  1. sheaves with extra structure (sheaves of abelian grous, sheaves of rings)
  2. pushing and pulling sheaves between spaces
  3. a way to do (1) and (2) that
  • doesn't take 5 seconds to elaborate per line
  • remains readable

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:29):

In particular, I think this will require a fair amount of api, so I'm not so sure that "sheaves on a space" will be "easy".

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:30):

I tried this more than a year ago, and I could define the push-pull adjunction, but it was a pain to use. Very slow, and unreadable.

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:31):

I didn't go full topos back then. Maybe that would have helped...
I think that (1) in particular will be a challenge to get usable.

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:31):

Do you have a nlab/stacks link for the push-pull adjunction?

view this post on Zulip Reid Barton (Jun 02 2020 at 14:33):

I think Johan means the geometric morphism Sh(X) -> Sh(Y) corresponding to a map of spaces X -> Y

view this post on Zulip Reid Barton (Jun 02 2020 at 14:33):

or is that what you want a link for

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:34):

Ah okay sure

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:36):

In particular, I want to move between different toposes effortlessly... (especially along geometric morphisms that come from geometry :stuck_out_tongue_wink: )

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:37):

Staying inside one topos will only get you through page 1 of algebraic geometry.

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:37):

I think this isn't easier by going full topos unfortunately - the pushforward functor is easy but pullback might not be... This might take some time (and help from geometers)

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:40):

Johan Commelin said:

In particular, I want to move between different toposes effortlessly... (especially along geometric morphisms that come from geometry :stuck_out_tongue_wink: )

I should of course have realised that the morphisms are just as important as the objects :P

view this post on Zulip Reid Barton (Jun 02 2020 at 14:40):

I thought it was just left Kan extension, followed by sheafification

view this post on Zulip Reid Barton (Jun 02 2020 at 14:40):

in this case where we start with a suitable functor between sites

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:41):

Reid Barton said:

I thought it was just left Kan extension, followed by sheafification

I'll defer to you on this

view this post on Zulip Reid Barton (Jun 02 2020 at 14:41):

i.e. one that already preserves covering families or whatever

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:41):

@Reid Barton We'll need an equation lemma (-;

view this post on Zulip Reid Barton (Jun 02 2020 at 14:42):

I think one thing that happened with sheaves on spaces was that there were some defeqs that one shouldn't expect in general

view this post on Zulip Reid Barton (Jun 02 2020 at 14:44):

and this probably contributed to slowness

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:44):

That might certainly be true

view this post on Zulip Reid Barton (Jun 02 2020 at 14:45):

Like if you have a map X -> Y which induces a functor on sites opens Y -> opens X then the functor probably satisfies the composition law definitionally... actually this might be a dumb example since these are posets

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:45):

Bhavik Mehta said:

Reid Barton said:

I thought it was just left Kan extension, followed by sheafification

I'll defer to you on this

The description I know of is the one at the start of VII.1 in MM, via etale spaces, maybe you're talking about the things in VII.10?

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:47):

Using etale spaces isn't going to work for arbitrary sites, right?

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:47):

If we're doing this right, it better also give push-pull for etale sheaves over a scheme, etc...

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:47):

Yeah

view this post on Zulip Reid Barton (Jun 02 2020 at 14:48):

I don't have MM on hand (guess where it is)... it would be nice if I could draw a diagram

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:48):

```tikzcd
too bad...
```

view this post on Zulip Reid Barton (Jun 02 2020 at 14:50):

Yes what Bhavik sent me in PM, pretty much.

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:50):

Reid Barton said:

I think one thing that happened with sheaves on spaces was that there were some defeqs that one shouldn't expect in general

Is this solved by marking lots of stuff as irreducible?

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:50):

Reid Barton said:

Yes what Bhavik sent me in PM, pretty much.

image.png

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 14:51):

That doesn't look too scary actually - I didn't want to have to define etale spaces myself!

view this post on Zulip Reid Barton (Jun 02 2020 at 14:52):

I would draw a square with PSh(C) -> PSh(D) on top and sheafification PSh(C) -> Sh(C), PSh(D) -> Sh(D) vertically (never draw a right adjoint as an arrow!) We need to fill in the bottom arrow Sh(C) -> Sh(D) and we can do it using the universal property of Sh(C) as long as we started with a morphism of sites C -> D. Here PSh(C) -> PSh(D) is left Kan extension (because it's left adjoint to restriction along C -> D which is what gives the pushforward... as usual the algebraic geometry names are backwards).

view this post on Zulip Reid Barton (Jun 02 2020 at 14:53):

But this is just a fancy way to say "forget it's a sheaf, left Kan extend, and sheafify" which I think is also equivalent to this C\otimes_C thing.

view this post on Zulip Reid Barton (Jun 02 2020 at 14:55):

You can put C -> D on top of this diagram and then it looks more like the one in that image (which is going around the edge C -> D -> PSh(D) -> Sh(D))

view this post on Zulip Reid Barton (Jun 02 2020 at 14:57):

But then, again, the question is whether this abstract definition in terms of sheafification (itself defined abstractly as a left adjoint) is adequate

view this post on Zulip Reid Barton (Jun 02 2020 at 15:05):

I guess the main thing you want to know about the pullback is that its stalks are isomorphic to the corresponding original stalks, right?

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:08):

No... we just use locales and pointless topology. There shouldn't be any reason to mention stalks ever, at all, nada. [/joking]

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:08):

I think that will certainly be an important first step in the API

view this post on Zulip Reid Barton (Jun 02 2020 at 15:10):

Yes, please excuse my crude language. Anyways, the stalk is just the pullback to a point, right? So we really just need to know that pullback is pseudofunctorial. Better?

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:10):

There's also this fast and loose applying adjunctions invisibly...
Crazy thought: a morphism between a sheaf F on X and a sheaf G on Y should really be a pair of two morphisms (one in Sh(X), and the other in Sh(Y)), plus a proof that they are associated via the adjunction...

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:11):

But that's an implementation detail.

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:11):

Yes, pseudofunctoriality, I hope that will go "smoothly"

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:12):

In maths, pullback is definitionally functorial on the nose :head_bandage:

view this post on Zulip Reid Barton (Jun 02 2020 at 15:26):

Is it really?
Anyways the right adjoint is obviously functorial, so that's enough

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:27):

That's enough to get some statement. But will that lead to fast readable code?

view this post on Zulip Reid Barton (Jun 02 2020 at 15:27):

Who can say?

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:28):

In maths you'll see (gf)=fg(g \circ f)^* = f^* \circ g^* all the time... it's treated as an invisible trivial defeq

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 15:29):

def real_pullback {A B : C} (f : A  B) : over B  over A :=
{ obj := λ g, over.mk (pullback.fst : pullback f g.hom  A),

is functorial

view this post on Zulip Reid Barton (Jun 02 2020 at 15:29):

Okay, I totally agree it is treated as an equality.

view this post on Zulip Reid Barton (Jun 02 2020 at 15:30):

which can of course be justified "by appealing to well-known strictification results"

view this post on Zulip Reid Barton (Jun 02 2020 at 15:31):

real_pullback f is a functor, but real_pullback is not a functor from C^op to Cat

view this post on Zulip Reid Barton (Jun 02 2020 at 15:31):

Unless you got very lucky or put in extra effort to make it so

view this post on Zulip Reid Barton (Jun 02 2020 at 15:33):

Or, I should say over is not a functor

view this post on Zulip Reid Barton (Jun 02 2020 at 15:35):

Defining and using an isomorphism (gf)fg(g \circ f)^* \cong f^* \circ g^* is easy enough, the tricky part will be keeping track of the fact that it somehow corresponds to the identity (gf)=gf(g \circ f)_* = g_* \circ f_*.

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:38):

We could have a variant on "never use , only use ": never use pullbacks... always apply adjunction and use pushforward...

view this post on Zulip Johan Commelin (Jun 02 2020 at 15:39):

I don't know if that would work in practice... but it gives me shivers anyways. We shouldn't need to jump through hoops like that.

view this post on Zulip Reid Barton (Jun 02 2020 at 15:39):

I think it doesn't really work anyways

view this post on Zulip Reid Barton (Jun 02 2020 at 15:39):

e.g. how to state base change theorems

view this post on Zulip Reid Barton (Jun 02 2020 at 15:41):

another attitude one could take is it's just another example of R[1/a][1/b]

view this post on Zulip Reid Barton (Jun 02 2020 at 15:41):

(gf)(g \circ f)^* is just some left adjoint to (gf)(g \circ f)_*, and fgf^* \circ g^* is one too

view this post on Zulip Reid Barton (Jun 02 2020 at 15:42):

though I don't really know if that solves the problem

view this post on Zulip Reid Barton (Jun 02 2020 at 15:42):

or what exactly the problem is


Last updated: May 11 2021 at 17:39 UTC