# Zulip Chat Archive

## Stream: maths

### Topic: Sheaves

#### 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.

#### Kenny Lau (Jun 10 2019 at 14:56):

I'm proud of my construction :P

#### Kevin Buzzard (Jun 10 2019 at 15:00):

It makes no mathematical sense :P

#### 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.

#### 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

#### Reid Barton (Jun 10 2019 at 15:06):

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

#### 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.

#### 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.

#### Johan Commelin (Jun 10 2019 at 16:29):

@Simon Pepin Lehalleur Welcome on the chat!

#### Simon Pepin Lehalleur (Jun 10 2019 at 16:35):

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

#### Kenny Lau (Jun 10 2019 at 17:25):

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

#### 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 $X$ covered by opens $U_i$, and for each $i$ you have a sheaf $\mathcal{F}_i$ on $U_i$. Say you have isomorphisms $\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 $\phi_{ik}=\phi_{jk}\circ\phi_{ij}$ as maps of sheaves on $U_i\cap U_j\cap U_k$, and such that $\phi_{ii}$ is the identity. Then we want a sheaf on all of $X$.

Even writing down the definition of $\mathcal{F}(U)$ is a pain. It involves taking the elements $(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 $t_i$ we need `U ∩ U_i : opens U_i`

and then to say "agree on overlaps" it becomes a bit of a nightmare.

#### 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`

.

#### Kenny Lau (Jun 10 2019 at 17:28):

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

#### 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

#### Kevin Buzzard (Jun 10 2019 at 17:28):

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

#### Kevin Buzzard (Jun 10 2019 at 17:30):

Agree on overlaps: mathematically it's easy to say. I want $\phi_{ij}$ to send (the restriction of $t_i$ to $U\cap U_i\cap U_j$) to (the restriction of $t_j$ to $U\cap U_i\cap U_j$)

#### 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?

#### Kevin Buzzard (Jun 10 2019 at 17:31):

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

#### Kenny Lau (Jun 10 2019 at 17:32):

oh right we're gluing along an isomorphism

#### 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.

#### 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.

#### 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.

#### Kenny Lau (Jun 10 2019 at 17:34):

#### Kenny Lau (Jun 10 2019 at 17:34):

Also maybe it's time to care about spelling

#### 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

#### Kenny Lau (Jun 10 2019 at 17:35):

ok I'll try formulating the statement

#### Kevin Buzzard (Jun 10 2019 at 17:35):

In which context?

#### Kevin Buzzard (Jun 10 2019 at 17:35):

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

#### 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"

#### Kenny Lau (Jun 10 2019 at 17:37):

well I still stand by my approach :P

#### 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.

#### 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?

#### 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

#### Kevin Buzzard (Jun 10 2019 at 17:46):

You'll get laughed at in the maths department

#### 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

#### 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

#### Kevin Buzzard (Jun 10 2019 at 17:53):

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

#### 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/`

)?

#### Kevin Buzzard (Jun 11 2019 at 06:43):

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

#### Johan Commelin (Jun 11 2019 at 06:44):

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

#### Kevin Buzzard (Jun 11 2019 at 06:44):

(maybe even only for open immersions)

#### Johan Commelin (Jun 11 2019 at 06:44):

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

#### 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...

#### Kevin Buzzard (Jun 11 2019 at 06:45):

There's still loads to do.

#### Johan Commelin (Jun 11 2019 at 06:45):

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

#### 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.

#### 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?

#### 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.

#### Reid Barton (Dec 14 2019 at 17:22):

That's in `topology.category.Top.opens`

#### 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.

#### Reid Barton (Dec 14 2019 at 17:25):

I don't think we have anything about pullbacks anywhere

#### Kevin Buzzard (Dec 14 2019 at 17:54):

Are there any PR's about sheaves?

#### Johan Commelin (Dec 14 2019 at 17:55):

Nope, don't think so

#### 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

#### 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?

#### Johan Commelin (Dec 14 2019 at 19:16):

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

#### 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

#### 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

#### Johan Commelin (Dec 14 2019 at 19:17):

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

#### Johan Commelin (Dec 14 2019 at 19:18):

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

#### Johan Commelin (Dec 14 2019 at 19:18):

And sometimes the category is `Type`

#### Kevin Buzzard (Dec 16 2019 at 21:15):

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).

#### Johan Commelin (Dec 16 2019 at 21:26):

That definition seems right

#### Johan Commelin (Dec 16 2019 at 21:27):

@Kevin Buzzard Huh, wait? How are `to_fork`

and `map_to_equalizer`

related?

#### 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...

#### Kevin Buzzard (Dec 16 2019 at 22:14):

`map_to_equalizer`

is the morphism from $\mathcal{F}(U)$ to the equalizer of $\prod_i\mathcal{F}(U_i)\to\to\prod_{j,k}\mathcal{F}(U_j\cap U_k)$

#### 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.

#### 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.

#### 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).

#### 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...

#### Kenny Lau (Dec 16 2019 at 23:44):

nice

#### Kevin Buzzard (Dec 16 2019 at 23:50):

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

#### David Michael Roberts (Dec 17 2019 at 00:04):

Sheaf of categories or sheaves valued in a given category?

#### Kevin Buzzard (Dec 17 2019 at 00:05):

Yes, sheaves valued in a given category. Sorry.

#### 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.

#### 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?

#### Kevin Buzzard (Dec 17 2019 at 01:27):

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

#### 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`

.

#### 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 :)

#### 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

#### Reid Barton (Jun 02 2020 at 14:15):

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

#### Patrick Massot (Jun 02 2020 at 14:15):

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

#### Reid Barton (Jun 02 2020 at 14:16):

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

#### 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

#### 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?

#### Reid Barton (Jun 02 2020 at 14:21):

Yes, I mean exactly this word "Omitted"

#### Johan Commelin (Jun 02 2020 at 14:29):

@Bhavik Mehta What will be very important is

- sheaves with extra structure (sheaves of abelian grous, sheaves of rings)
- pushing and pulling sheaves between spaces
- a way to do (1) and (2) that

- doesn't take 5 seconds to elaborate per line
- remains readable

#### 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".

#### 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.

#### 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.

#### Bhavik Mehta (Jun 02 2020 at 14:31):

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

#### 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

#### Reid Barton (Jun 02 2020 at 14:33):

or is that what you want a link for

#### Bhavik Mehta (Jun 02 2020 at 14:34):

Ah okay sure

#### 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: )

#### Johan Commelin (Jun 02 2020 at 14:37):

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

#### 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)

#### 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

#### Reid Barton (Jun 02 2020 at 14:40):

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

#### Reid Barton (Jun 02 2020 at 14:40):

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

#### 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

#### Reid Barton (Jun 02 2020 at 14:41):

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

#### Johan Commelin (Jun 02 2020 at 14:41):

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

#### 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

#### Reid Barton (Jun 02 2020 at 14:44):

and this probably contributed to slowness

#### Johan Commelin (Jun 02 2020 at 14:44):

That might certainly be true

#### 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

#### 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?

#### Johan Commelin (Jun 02 2020 at 14:47):

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

#### 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...

#### Bhavik Mehta (Jun 02 2020 at 14:47):

Yeah

#### 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

#### Johan Commelin (Jun 02 2020 at 14:48):

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

#### Reid Barton (Jun 02 2020 at 14:50):

Yes what Bhavik sent me in PM, pretty much.

#### 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?

#### Bhavik Mehta (Jun 02 2020 at 14:50):

Reid Barton said:

Yes what Bhavik sent me in PM, pretty much.

#### 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!

#### 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).

#### 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 $\otimes_C$ thing.

#### 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))

#### 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

#### 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?

#### 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]

#### Johan Commelin (Jun 02 2020 at 15:08):

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

#### 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?

#### 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...

#### Johan Commelin (Jun 02 2020 at 15:11):

But that's an implementation detail.

#### Johan Commelin (Jun 02 2020 at 15:11):

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

#### Johan Commelin (Jun 02 2020 at 15:12):

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

#### Reid Barton (Jun 02 2020 at 15:26):

Is it really?

Anyways the right adjoint is obviously functorial, so that's enough

#### Johan Commelin (Jun 02 2020 at 15:27):

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

#### Reid Barton (Jun 02 2020 at 15:27):

Who can say?

#### Johan Commelin (Jun 02 2020 at 15:28):

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

#### 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

#### Reid Barton (Jun 02 2020 at 15:29):

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

#### Reid Barton (Jun 02 2020 at 15:30):

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

#### 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`

#### Reid Barton (Jun 02 2020 at 15:31):

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

#### Reid Barton (Jun 02 2020 at 15:33):

Or, I should say `over`

is not a functor

#### Reid Barton (Jun 02 2020 at 15:35):

Defining and using an isomorphism $(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 $(g \circ f)_* = g_* \circ f_*$.

#### 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...

#### 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.

#### Reid Barton (Jun 02 2020 at 15:39):

I think it doesn't really work anyways

#### Reid Barton (Jun 02 2020 at 15:39):

e.g. how to state base change theorems

#### 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]

#### Reid Barton (Jun 02 2020 at 15:41):

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

#### Reid Barton (Jun 02 2020 at 15:42):

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

#### Reid Barton (Jun 02 2020 at 15:42):

or what exactly the problem is

Last updated: May 11 2021 at 17:39 UTC