Sheaves

Stream: maths

[Kevin Buzzard]

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]

I'm proud of my construction :P

[Kevin Buzzard]

It makes no mathematical sense :P

[Kevin Buzzard]

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]

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]

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

[Simon Pepin Lehalleur]

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]

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]

@Simon Pepin Lehalleur Welcome on the chat!

[Simon Pepin Lehalleur]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

oh right we're gluing along an isomorphism

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

gluing-vs-glueing

[Kenny Lau]

Also maybe it's time to care about spelling

[Kevin Buzzard]

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]

ok I'll try formulating the statement

[Kevin Buzzard]

In which context?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

well I still stand by my approach :P

[Kevin Buzzard]

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]

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]

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]

You'll get laughed at in the maths department

[Kenny Lau]

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]

You'll get laughed at in the maths department

so maybe I should LaTeX the whole thing instead

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

(maybe even only for open immersions)

[Johan Commelin]

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

[Kevin Buzzard]

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]

There's still loads to do.

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

That's in topology.category.Top.opens

[Johan Commelin]

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

[Reid Barton]

I don't think we have anything about pullbacks anywhere

[Kevin Buzzard]

Are there any PR's about sheaves?

[Johan Commelin]

Nope, don't think so

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

And sometimes the category is Type

[Kevin Buzzard]

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

[Johan Commelin]

That definition seems right

[Johan Commelin]

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

[Johan Commelin]

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]

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

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

[Kevin Buzzard]

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]

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]

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]

nice

[Kevin Buzzard]

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

[David Michael Roberts]

Sheaf of categories or sheaves valued in a given category?

[Kevin Buzzard]

Yes, sheaves valued in a given category. Sorry.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

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]

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]

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

[Patrick Massot]

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

[Reid Barton]

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

[Bhavik Mehta]

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]

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]

Yes, I mean exactly this word "Omitted"

[Johan Commelin]

@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

[Johan Commelin]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

or is that what you want a link for

[Bhavik Mehta]

Ah okay sure

[Johan Commelin]

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

[Johan Commelin]

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

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

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

[Bhavik Mehta]

Reid Barton said:

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

I'll defer to you on this

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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]

and this probably contributed to slowness

[Johan Commelin]

That might certainly be true

[Reid Barton]

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]

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]

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

[Johan Commelin]

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

[Bhavik Mehta]

Yeah

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

Yes what Bhavik sent me in PM, pretty much.

[Bhavik Mehta]

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]

Reid Barton said:

Yes what Bhavik sent me in PM, pretty much.

image.png

[Bhavik Mehta]

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

[Reid Barton]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Reid Barton]

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]

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]

But that's an implementation detail.

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

Who can say?

[Johan Commelin]

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

[Bhavik Mehta]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

Or, I should say over is not a functor

[Reid Barton]

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]

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

[Johan Commelin]

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]

I think it doesn't really work anyways

[Reid Barton]

e.g. how to state base change theorems

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

or what exactly the problem is