breaking equality with sheaves

Stream: maths

[Kevin Buzzard]

A sheaf of types $\mathcal{F}$ on a topological space $X$ is, for every open set $V\subseteq X$, a type $\mathcal{F}(V)$, plus some extra data and some axioms.

As part of the schemes project we would like to glue sheaves on open subsets. In short, given an open cover $U_i$ of $X$ and sheaves on each $U_i$ which are compatible in some precise way, one can glue the sheaves together to get a sheaf on $X$. I tried to formalise this the naive way, and formalising the compatibility was a real nightmare, because a sheaf is on a topological space so I had to really work with types $U_i$ and I had to constantly be moving between the type $U_i\cap U_j$, the open subset $U_i\cap U_j$ of $U_i$, the open subset $U_i\cap U_j$ of $U_j$$ and the open subset $U_i\cap U_j$ of $X$; all of these four objects show up. One of the compatibilities one needs is a "cocycle identity" which involves three subsets $U_i$, $U_j$ and $U_k$, and it was pretty horrible.

Kenny suggested a completely insane way around this. He defined a sheaf on an open subset $U$ of $X$ to simply be a sheaf on $X$! It is true that given a sheaf on an open subset $U\subseteq X$ one can push it forward to get a sheaf on $X$, given a sheaf on $X$ one can pull it back to get a sheaf on an open subset $U$, but it is also true that two sheaves on $X$ which are not equal (resp isomorphic), can become equal (resp isomorphic) when restricted to $U$.

In short, Kenny has proposed a definition of a sheaf on $U$ for which Lean's = type is wrong -- it does not correctly capture the notion of equality of sheaves.

Kenny went on to define morphisms of sheaves-on-$U$ (using his definition) and a notion of equiv which is the correct definition. So we do have the correct notion of isomorphism, and the sheaves-on-$U$ form a category which is equivalent to the correct category. This category has the extraordinary (to me) property that the notion of equality on it is incorrect. However I have just formalised the statement of the universal property which the glued sheaf has to satisfy (its restriction to the $U_i$ should be isomorphic to the sheaf $\mathcal{F}_i$ we started with -- not equal to it) and at least the statement looks fine.

Am I going to run into trouble later?

One way of thinking about this is that a sheaf is a functor, so we have made some functor category, and we are interested in restricting this functor to a subcategory to get a new functor category, and I want to define it to be the actual restriction, but Kenny has just defined it to be the original functor and has basically said screw equality.

[Kenny Lau]

we don't ever want to say that two (at least set-valued-) sheaves are equal right

[Kevin Buzzard]

I guess that's my question. They are two terms of some type so I thought that equality was ok. But they involve some dependent type so maybe it's not ok

[Kevin Buzzard]

You can prove that if two sheaves are equal when restricted to an open subset then they are equal. This is very counterintuitive to me

[Kevin Buzzard]

Perhaps your argument is that equality of sheaves is never ok

[Kenny Lau]

that is indeed my argument

[Kevin Buzzard]

It is not true that if two sheaves are the same when restricted to an open subset then they are the same

[Kevin Buzzard]

But I have become more and more confused about what "the same" means recently

[Kevin Buzzard]

I find this very surprising. Here we have an equality on a type which is literally not correct -- it is too weak

[Kevin Buzzard]

My rule of thumb was that x = y was not good if x : Sort u but x = y was OK if x : T with T : Type u. This is a counterexample.

[Sebastien Gouezel]

I encountered a similar situation with manifolds. The basic objects is charts, i.e., local homeomorphisms (defined on their source), that one keeps composing (thereby restricting the sources by taking the intersection of the source of the first guy and the preimage of the source of the second guy). There are (at least) three ways to formalize them:

• (1) use a homeomorphism defined on a subtype
• (2) use a map taking values in option ..., which is none outside of the source
• (3) use a map defined on all the space, that happens to be a homeomorphism on a subset of the space that you call source, and do not care about what this map does outside of source.

(1) is a nightmare from the point of view of intersections of subtypes just as what you have for sheaves. (2) is a nightmare when you want to define regularity classes because you always need to distinguish between points in the genuine space and points in option. (3) looks crazy, but in fact it works very well. The only drawback is that you want to say that two local homeomorphisms are "equal" if they have the same source and coincide there. This is an equiv, that I introduced. But in fact it turns out that in 99% of the proofs I don't need to talk about equality of local homeomorphisms, I just need to compose them. So it works fine. And I think it more or less corresponds to Kenny's suggestion for sheaves.

There was already a discussion on the chat where people told me to use (1) or (2) instead. And I agree that from a mathematical point of view this is the right thing to do, but from an implementation point of view (3) simply works better. Yesterday, I asked Assia Mahboubi , who has done way more formalization using DTT than anyone on this chat, about what to choose between (1), (2), (3), and her reaction was: (3) is clearly better.

[Kevin Buzzard]

OK I'm convinced :-)

[Kevin Buzzard]

In fact I was already half-convinced when I realised that I could formalise the glueing lemma and the statement of its universal property. I guess what I am half-worried about is rewriting. If we lose the true meaning of = then we lose the ability to rewrite.

I will try and formalise the proof of the glueing lemma over the weekend, this will be a very good test case I think.

[Sebastien Gouezel]

Yes, you can not rewrite. But if you have enough lemmas saying that, under the assumption that two objects are "equivalent", then some property holds, then you can rewrite using these lemmas.

[Kevin Buzzard]

I do not yet have a feeling as to how much of a handicap this will be.

[Sebastien Gouezel]

I think it will be very interesting to hear how your proof of the glueing lemma goes.

[Mario Carneiro]

There is a way to recover equality while still using sheaves on X. There is a condition you can put on your sheaf such that pushing back to U and then forward to X recovers the same sheaf

[Kevin Buzzard]

Yes you're right; I discussed this privately with Kenny. The condition is that for all V open in X, the restriction map from F(V) to F(V intersect U) is an isomorphism (in the appropriate category). Here are several comments about this idea.

Firstly, we have a restriction map from F(V) to F(V intersect U), but we have no inverse, so one would have to make a choice about either just saying it's a bijection, or demanding an inverse. This seemed a bit weird.

Secondly, if we do this then sheaves on U are a subtype of sheaves on X, so we get the right equality but we'd have to constantly be carrying round and checking these proofs.

Thirdly, I can see that my philosophy is wrong. If x, y : T with T : Type u then sometimes it's fine to talk about x = y (e.g. if T=nat). If x, y : Type u then in general I can see that it is not really the right thing to do in dependent type theory, and I am quite happy with the weaker concept of being isomorphic, although I still think that there should be a whole bunch of automation which is not currently in Lean which will enable me to rewrite along isomorphisms in certain cases, with auto-generated proofs. However I do see that equality of two types is a bit weird. With the sheaf setting, equality really does look weird, because here x, y : T and T : Type u but T is a structure which has a dependent type as a field, and equality of x and y would imply equality of those dependent functions, which by functional extensionality boils down to equality of types again. This does not seem to be a good idea in type theory. If we go with the philosophy that equality of types is to be avoided, then equality of these particular terms should also I think be avoided.

Another way to recover equality is simply to quotient out by the correct notion. Whether this comes out nicer or more nastily than the subtype approach Mario is suggesting -- who knows. But currently my plan is to go with Kenny's crazy idea, because Sebastian and Assia seem to think that it's not so crazy after all, and I am open to the suggestion that losing the ability to rewrite will not hurt me. After all, if I have sheaves F_i on U_i and glue them together to get a sheaf F on X, the universal property really is not the statement that the restriction of F to U_i equals F_i, it is the data of an isomorphism.

[Mario Carneiro]

I agree that equality of sheafs should be avoided. What I want to avoid is "random" data inside a sheaf

[Kevin Buzzard]

So currently we have random data. I agree that there are several ways of getting rid of the randomness, including replacing sheaves on X by either a sub or a quotient. But each of these is more inconvenient to work with.

[Kevin Buzzard]

I thought that randomness was everywhere in topology in Lean, with functions being randomly extended. Even 1/ 0 = 0 is a random choice.

[Mario Carneiro]

A similar sort of example is subfilters. A filter on X is not the same as a filter on a subset S, but given a filter on a subset there is a canonical way to extend it to a filter, and restrict any filter to a subset, and the filters that are extended subset filters are exactly those such that S \in F

[Mario Carneiro]

random meaning not uniquely defined

[Kevin Buzzard]

If I was buying into your idea I think I would go with the subtype. But then there's the question of how you say that the map F(V) -> F(U intersect V) is an isomorphism. Do you just state that there exists an inverse, or do you give it?

[Kevin Buzzard]

Another alternative is extension by zero. You just define F(V) to be zero if V is not a subset of U, or whatever the appropriate initial object is

[Mario Carneiro]

You said there is a way to go from a sheaf on U to one on X and back. How does that work? what map F(V) -> F(U \cap V) does it give you?

[Kevin Buzzard]

There is more than one way.

[Kevin Buzzard]

You don't know about the 6 functor formalism? ;-)

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Six_operations

[Mario Carneiro]

mathematician naming at its best

[Kevin Buzzard]

At least there are 6 of them.

[Kevin Buzzard]

You can see how to get from a sheaf on X to a sheaf on U, right? This is just some kind of forgetful functor.

[Kevin Buzzard]

Well guess what: in many situations this has both a left and a right adjoint, which typically do not agree.

[Mario Carneiro]

If G is the sheaf on X, then it is defined by G(V) = F(U cap V), yes?

[Kevin Buzzard]

That's one of the ways of going from sheaves on U to sheaves on X, yes.

[Mario Carneiro]

oh it's backwards?

[Kevin Buzzard]

The other way is G(V)=0 if V is not a subset of U, and G(V)=F(V)otherwise.

[Mario Carneiro]

I want the original one you said, sheaf on U -> sheaf on X

[Kevin Buzzard]

That one is just G(V)=F(V)

[Kevin Buzzard]

wait, notation

[Kevin Buzzard]

There are two ways of going from U to X. There is one way of going from X to U. There are two theorems that say something is adjoint to something else.

[Kevin Buzzard]

The trivial thing is going from X to U. U is a subset of X here.

[Mario Carneiro]

But if G is the newly defined sheaf on X, shouldn't it take an open set in X? so F(V) doesn't necessarily work

[Kevin Buzzard]

The non-trivial things are going from sheaves on U to sheaves on X. One way is G(V)=F(V intersect U). The other way is G(V)=F(V) if this makes sense and 0 otherwise

[Kevin Buzzard]

I am so used to thinking about etale sheaves, I am not even sure if this is right for sheaves on a top space.

[Kevin Buzzard]

i might need to go and check the sheaf axiom. If it doesn't work, I might have to sheafify :-/

[Mario Carneiro]

where 0 is an empty type?

[Kevin Buzzard]

0 is an initial object.

[Kevin Buzzard]

I'm thinking about sheaves taking values in some arbitrary category really.

[Mario Carneiro]

so we can't really avoid some variation here

[Kevin Buzzard]

I'm thinking about sheaves taking values in the category of abelian groups, truth be told.

[Kevin Buzzard]

I think the extension by 0 is OK.

[Kevin Buzzard]

It looks like the sort of thing you computer scientists would really like. "Don't know the answer? Try zero!"

[Mario Carneiro]

I think that it would be best to have the actual definition be the one you started with, using subtypes, but then build an API to see them as sheafs on X

[Kevin Buzzard]

If I wanted to build an API I'd just define them as sheaves on U and then go through all the pain ;-)

[Mario Carneiro]

is all this pain just to build the API?

[Kevin Buzzard]

Kenny built an API for sheaves on U just being sheaves on X.

[Kevin Buzzard]

import sheaves.sheaf

universes v w u₁ v₁ u

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

namespace morphism

protected def id (F : sheaf_on_opens.{v} X U) : F.morphism F :=
{ map := λ V HV, id,
  commutes := λ V HV W HW HWV x, rfl }

def comp {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} {H : sheaf_on_opens.{u₁} X U}
  (η : G.morphism H) (ξ : F.morphism G) : F.morphism H :=
{ map := λ V HV x, η.map V HV (ξ.map V HV x),
  commutes := λ V HV W HW HWV x, by rw [ξ.commutes, η.commutes] }

@[extensionality] lemma ext {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U}
  {η ξ : F.morphism G} (H : ∀ V HV x, η.map V HV x = ξ.map V HV x) : η = ξ :=
by cases η; cases ξ; congr; ext; apply H

@[simp] lemma id_comp {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} (η : F.morphism G) :
  (morphism.id G).comp η = η :=
ext $ λ V HV x, rfl

@[simp] lemma comp_id {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} (η : F.morphism G) :
  η.comp (morphism.id F) = η :=
ext $ λ V HV x, rfl

@[simp] lemma comp_assoc {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} {H : sheaf_on_opens.{u₁} X U} {I : sheaf_on_opens.{v₁} X U}
  (η : H.morphism I) (ξ : G.morphism H) (χ : F.morphism G) :
  (η.comp ξ).comp χ = η.comp (ξ.comp χ) :=
rfl

def res_subset {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} (η : F.morphism G) (V : opens X) (HVU : V ⊆ U) :
  (F.res_subset V HVU).morphism (G.res_subset V HVU) :=
{ map := λ W HWV, η.map W (set.subset.trans HWV HVU),
  commutes := λ S HSV T HTV, η.commutes S (set.subset.trans HSV HVU) T (set.subset.trans HTV HVU) }

@[simp] lemma comp_res_subset {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} {H : sheaf_on_opens.{u₁} X U}
  (η : G.morphism H) (ξ : F.morphism G) (V : opens X) (HVU : V ⊆ U) :
  (η.res_subset V HVU).comp (ξ.res_subset V HVU) = (η.comp ξ).res_subset V HVU :=
rfl

@[simp] lemma id_res_subset {F : sheaf_on_opens.{v} X U} (V : opens X) (HVU : V ⊆ U) :
  (morphism.id F).res_subset V HVU = morphism.id (F.res_subset V HVU) :=
rfl

end morphism

structure equiv (F : sheaf_on_opens.{v} X U) (G : sheaf_on_opens.{w} X U) : Type (max u v w) :=
(to_fun : morphism F G)
(inv_fun : morphism G F)
(left_inv : inv_fun.comp to_fun = morphism.id F)
(right_inv : to_fun.comp inv_fun = morphism.id G)

namespace equiv

def refl (F : sheaf_on_opens.{v} X U) : equiv F F :=
⟨morphism.id F, morphism.id F, rfl, rfl⟩

def symm {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{v} X U} (e : equiv F G) : equiv G F :=
⟨e.2, e.1, e.4, e.3⟩

def trans {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{v} X U} {H : sheaf_on_opens.{u₁} X U}
  (e₁ : equiv F G) (e₂ : equiv G H) : equiv F H :=
⟨e₂.1.comp e₁.1, e₁.2.comp e₂.2,
by rw [morphism.comp_assoc, ← e₂.2.comp_assoc, e₂.3, morphism.id_comp, e₁.3],
by rw [morphism.comp_assoc, ← e₁.1.comp_assoc, e₁.4, morphism.id_comp, e₂.4]⟩

def res_subset {F : sheaf_on_opens.{v} X U} {G : sheaf_on_opens.{w} X U} (e : equiv F G)
  (V : opens X) (HVU : V ⊆ U) : equiv (F.res_subset V HVU) (G.res_subset V HVU) :=
⟨e.1.res_subset V HVU, e.2.res_subset V HVU,
by rw [morphism.comp_res_subset, e.3, morphism.id_res_subset],
by rw [morphism.comp_res_subset, e.4, morphism.id_res_subset]⟩

end equiv

-- should be in mathlib

namespace opens

def Union {I : Type*} (s : I → opens X) : opens X :=
⟨set.Union (λ i, (s i).1), is_open_Union (λ i, (s i).2)⟩

variables {I : Type*} (s : I → opens X)

theorem subset_Union : ∀ (s : I → opens X) (i : I), s i ⊆ Union s :=
-- why does lattice.le_supr need complete lattice?
λ s i x hx, set.mem_Union.2 ⟨i, hx⟩

/- Other things I might need about this Union

@[simp] theorem mem_Union {x : β} {s : ι → set β} : x ∈ Union s ↔ ∃ i, x ∈ s i :=
⟨assume ⟨t, ⟨⟨a, (t_eq : s a = t)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq.symm ▸ h⟩,
  assume ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩
/- alternative proof: dsimp [Union, supr, Sup]; simp -/
  -- TODO: more rewrite rules wrt forall / existentials and logical connectives
  -- TODO: also eliminate ∃i, ... ∧ i = t ∧ ...

theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (⋃ i, s i) ⊆ t :=
-- TODO: should be simpler when sets' order is based on lattices
@supr_le (set β) _ set.lattice_set _ _ h

theorem Union_subset_iff {α : Sort u} {s : α → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t):=
⟨assume h i, subset.trans (le_supr s _) h, Union_subset⟩

theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr

theorem Union_const [inhabited ι] (s : set β) : (⋃ i:ι, s) = s :=
ext $ by simp

theorem inter_Union_left (s : set β) (t : ι → set β) :
  s ∩ (⋃ i, t i) = ⋃ i, s ∩ t i :=
ext $ by simp

theorem inter_Union_right (s : set β) (t : ι → set β) :
  (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
ext $ by simp

theorem Union_union_distrib (s : ι → set β) (t : ι → set β) :
  (⋃ i, s i ∪ t i) = (⋃ i, s i) ∪ (⋃ i, t i) :=
ext $ by simp [exists_or_distrib]

theorem union_Union_left [inhabited ι] (s : set β) (t : ι → set β) :
  s ∪ (⋃ i, t i) = ⋃ i, s ∪ t i :=
by rw [Union_union_distrib, Union_const]

theorem union_Union_right [inhabited ι] (s : set β) (t : ι → set β) :
  (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
by rw [Union_union_distrib, Union_const]

theorem diff_Union_right (s : set β) (t : ι → set β) :
  (⋃ i, t i) \ s = ⋃ i, t i \ s :=
inter_Union_right _ _

-/

end opens

def glue {I : Type*} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :
  sheaf_on_opens.{max u v} X (opens.Union S) :=
{ F :=
  { F := λ W, { f : Π i, (F i).eval ((S i) ∩ W) (set.inter_subset_left _ _) //
      ∀ i j, (φ i j).1.map ((S i) ∩ (S j) ∩ W) (set.inter_subset_left _ _)
        ((F i).res ((S i) ∩ W) _ _ (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _))
          (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))
          (f i)) =
        (F j).res ((S j) ∩ W) _ _ (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _))
          (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))
          (f j) },
    res := λ U V HUV f, ⟨λ i, (F i).res (S i ∩ U) _ (S i ∩ V) _ (set.inter_subset_inter_right _ HUV) (f.1 i),
      begin sorry

      end⟩,
    Hid := sorry,
    Hcomp := sorry },
  locality := sorry,
  gluing := sorry }

def universal_property (I : Type*) (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :
∀ i : I, equiv (res_subset (glue S F φ Hφ1 Hφ2) (S i) $ opens.subset_Union S i) (F i) := sorry

end sheaf_on_opens

[Kevin Buzzard]

If I fill in the sorries then I've proved that Kenny's random idea works out. The alternative is to use a subtype, but then I need " F(V) -> F(U intersect V) is an isomorphism" to be a Prop, so things might get noncomputable.

[Mario Carneiro]

wait so you still have a separate definition? This seems like a lot of duplication

[Kevin Buzzard]

Not that I care, but you might.

[Kevin Buzzard]

We have a wrapper:

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

[Mario Carneiro]

Remind me the original definitions, I will show how to do this without all the proof obligations

[Mario Carneiro]

The res function need not take a proof arg, nor eval

[Kevin Buzzard]

Right!

[Kevin Buzzard]

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

[Kevin Buzzard]

That's the definition of a sheaf.

[Kevin Buzzard]

It uses the file presheaf.lean in the same directory, plus epsilon about open coverings.

[Mario Carneiro]

I will come back to this later, but here's the first pass:

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]

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 (HV : V ∈ S) (HW : W ∈ S),
  res' F (V ⊓ W) (s V HV) = res' F (V ⊓ W) (s W HW)) →
∃ x : F U, ∀ V HV, F.res' V x = s V HV

end presheaf

[Kevin Buzzard]

I think your definition of presheaf is essentially the definition of a functor

[Kevin Buzzard]

To Type

[Reid Barton]

it had better be!

[Mario Carneiro]

more or less; it's a preorder category on the left too, and I use the existence of infima a lot

[Mario Carneiro]

which I think means products?

[Mario Carneiro]

However this generalization is basically zero cost, while I'm not sure that generalizing to functor is also zero cost

[Mario Carneiro]

it's not really even relevant, it's just sort of an obvious generalization the way it's been written

[Kevin Buzzard]

But functors are already there. @Scott Morrison and I had talked about this being a very good use case for the category theory library.

[Mario Carneiro]

the point I want to make involves res'

[Kevin Buzzard]

And this total trick

[Mario Carneiro]

once again, untyped to the rescue

[Mario Carneiro]

there is still some unpacking to do with the definition of locality and gluing; one wants the statement to be in terms of families not sets

[Kevin Buzzard]

There seem to be several approaches to this. I remember Scott saying that presheaves were fine but the sheaf axiom got a bit grotty in the sense that he wasn't happy with his attempts to formalise it. The sheaf axiom is gluing \and locality

[Kevin Buzzard]

You can make them into one axiom by changing that exists in the conclusion of glueing to exists unique, but Ramon found it nicer to keep them separate.

[Mario Carneiro]

Oh, this is epsilon nicer:

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

[Kevin Buzzard]

So what is the advantage of this approach over Kenny's, given that I decided I didn't care about equality being broken? @Sebastien Gouezel does this approach have an analogue in your chart world?

[Mario Carneiro]

Axiomatically, this is equivalent to the very first definition we started with when we first looked at it

[Mario Carneiro]

All I'm doing is layering a more convenient API on top

[Kevin Buzzard]

In the schemes project we need sheaves of rings, and then sheaves of modules over the rings.

[Mario Carneiro]

You can change Type to a category here without changing anything

[Kevin Buzzard]

I'm not sure there's a category of modules over the category of rings, as it were

[Mario Carneiro]

well that's not exactly true; I'm using a sigma type which needs the underlying space to be a type

[Kevin Buzzard]

In the perfectoid project we need sheaves of topological rings, and there's an extra subtlety there

[Kevin Buzzard]

The sheaf axiom says that a certain map is an equalizer, and we're writing it as "there exists unique x" but in the category of topological spaces there's more to it than that.

[Kevin Buzzard]

We need two topologies on a ring to coincide as well. This seems like a good excuse to go full category with the target

[Mario Carneiro]

Eh, I'm not really sure about the quality of any remarks I make here. Show me the code and we can talk

[Mario Carneiro]

Make this definition in the generality that you actually need

[Kevin Buzzard]

I'm just thinking of all the "extreme" notions of sheaves which I've encountered so far in my Lean work.

[Kevin Buzzard]

Make this definition in the generality that you actually need

That's not the right approach, because the generality we actually need is sheaves of categories on a site.

[Kevin Buzzard]

That's what we'll need when we start doing etale cohomology.

[Kevin Buzzard]

So now you won't be able to get away with lattices, there is a category with a Grothendieck topology.

[Kevin Buzzard]

The whole "work in the correct generality" thing might work for basic Lean stuff but in maths things get so absurdly general sometimes that it's really not that clear that you want to work in the fullest 2019 generality.

[Kevin Buzzard]

Not least because you might be out of date in 5 years anyway.

[Mario Carneiro]

I don't mean the possible generality that exists, I mean the generality that suffices for the short to mid term future

[Mario Carneiro]

like "what we need for the current major milestone"

[Kevin Buzzard]

For all I know they're doing sheaves on infinity,1 categories nowadays.

[Mario Carneiro]

always have a concrete application in mind that is not in danger of being pushed off to the infinite future

[Kevin Buzzard]

The reason I'm thinking about gluing sheaves is that we have a nice theory of affine schemes, and then to make general schemes you have to glue affine schemes together. We can glue topological spaces together, so all we have to do is to glue sheaves together and we can make general schemes. That would be a cool milestone. To do that we would need to be able to glue sheaves of commutative rings together.

[Mario Carneiro]

Okay, so you need to have more than sheaves on Type then. Do you need more than lattices?

[Kevin Buzzard]

A sheaf of commutative rings is just a sheaf of types but all the res maps are ring homs. We're still talking about sheaves on topological spaces here, so if opens X is a lattice then we don't need more than lattices.

[Kevin Buzzard]

I've been thinking about the next few things which it would be fun to formalise (and looking for students to do them). I should perhaps post them as issues, as per Scott's suggestion.

[Mario Carneiro]

something like this then?

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

[Mario Carneiro]

you can't prove that res' is a ring_hom because it has the wrong type, but you could either use a different total space that is a ring, like Reid suggested in the CDGA thread, or you could just prove concretely that it preserves addition and so on modulo a coercion

[Mario Carneiro]

Ah, actually neither of those options works. Apparently rings don't have a very nice indexed coproduct; it can be trivial because of characteristic constraints. And it's not really easy to talk about addition and so on over a coercion unless the total space has an addition

[Mario Carneiro]

But this definition is so higher order that perhaps you aren't really doing actual algebra on the rings anymore, and knowing that the res maps are abstractly a ring hom is sufficient

[Kevin Buzzard]

Yes, you really don't want to be making all the objects subtypes of a large object, this can't be done in general (and in particular it can't be done with commutative rings, which are an important case). In the CDGA thread we had abelian groups (or more generally R-modules for a fixed R), where it can be done. As far as I know nobody has formalised sheaves of $\mathcal{O}_X$-modules, where $\mathcal{O}_X$ is the traditional name for the standard sheaf of rings on a scheme, the structure sheaf (namely the sheaf of functions on the scheme).

I am unclear about why Mario is unhappy about the definition containing random junk.

[Mario Carneiro]

It can always be done, but you get some thing that's not in the category in general

[Mario Carneiro]

which is not actually a problem in most cases

[Mario Carneiro]

I don't know if I can explain the issue I have with "random junk" clearly, which is worrisome

[Mario Carneiro]

Although I don't suggest the use of = on these objects, I do want the shape of the types to reflect the structure of the type

[Mario Carneiro]

I will grant that consistently using a "weird equiv" will mostly make this decision invisible

[Mario Carneiro]

maybe I'm still hoping for that HoTT style transfer tactic, where equivs are magicked up from the definition of the type

[Kevin Buzzard]

It can always be done -- ah yes sorry, I was sticking within the category. I see you can always make the sigma type, and doing Reid's CDGA exercise the naive way showed me clearly how it can be advantageous to make the type. I haven't seen the point of it here yet but presumably we're just waiting for the analogue of Reid's challenge questions to show up.

Random junk -- I am going to press ahead with the bad = type just out of interest, although apparently I have to go and be social this weekend, which rather spoils my fun plans. Sheaves and schemes have turned out to be a really good test case for teaching me about the subtleties of type theory. Part of me is still amazed that there weren't mathematicians doing this stuff in Coq 10 years ago.

[Kevin Buzzard]

maybe I'm still hoping for that HoTT style transfer tactic, where equivs are magicked up from the definition of the type

Aah! I see that this will definitely fail with Kenny's approach!

[Kevin Buzzard]

def glue {I : Type*} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :
  sheaf_on_opens.{max u v} X (opens.Union S) :=
{ F :=
  { F := λ W, { f : Π i, (F i).eval ((S i) ∩ W) (set.inter_subset_left _ _) //
      ∀ i j, (φ i j).1.map ((S i) ∩ (S j) ∩ W) (set.inter_subset_left _ _)
        ((F i).res ((S i) ∩ W) _ _ (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _))
          (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))
          (f i)) =
        (F j).res ((S j) ∩ W) _ _ (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _))
          (set.subset_inter (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))
          (f j) },
    res := λ U V HUV f, ⟨λ i, (F i).res (S i ∩ U) _ (S i ∩ V) _ (set.inter_subset_inter_right _ HUV) (f.val i),
      begin
        intros i j,
--        cases f with f hf,
        rw res_comp,
        rw res_comp,
        have answer := congr_arg (res (F j) (S i ∩ (S j) ∩ U) _ (S i ∩ (S j) ∩ V)
          (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_right _ _))
          (set.inter_subset_inter_right _ HUV)) (f.property i j),
        rw res_comp at answer,
        rw ←answer,
        clear answer,
        let XXX := (φ i j).to_fun.commutes (S i ∩ (S j) ∩ U) (set.inter_subset_left _ _)
          (S i ∩ (S j) ∩ V) (set.inter_subset_left _ _) (set.inter_subset_inter_right _ HUV)
          (res (F i) (S i ∩ U) _ (S i ∩ S j ∩ U) _ (set.inter_subset_inter_left _ (set.inter_subset_left _ _))
            (f.val i) : eval (F i) (S i ∩ (S j) ∩ U)
            (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _))),
--        simp only [eval_res_subset] at XXX,
--        rw eval_res_subset at XXX,
--          rw XXX,
--        convert XXX,
--        simp [XXX],
        --rw ←res_comp (F i) (S i ∩ U) _ (S i ∩ S j ∩ U)
        --  (set.subset.trans (set.inter_subset_left _ _) (set.inter_subset_left _ _))
        --  (S i ∩ S j ∩ V) _ (set.inter_subset_inter_left _ (set.inter_subset_left _ _)) (set.inter_subset_inter_right _ HUV),
--        rw ←(F i : sheaf X).F.Hcomp',
--        rw (φ i j).to_fun.commutes _ _ _ _ _, -- (V : opens X) (HV : V ⊆ U) (W : opens X) (HW : W ⊆ U) (HWV : W ⊆ V) (x : eval F V HV)
sorry,
      end⟩,
    Hid := sorry,
    Hcomp := sorry },
  locality := sorry,
  gluing := sorry }

Glueing sheaves is quite interesting @Kenny Lau . There are all sorts of things to think about. I am not sure I fully understand the power of Hφ2 yet. Do you know a better way of understanding it? Is it a 1-cocycle of some sort?

[Kenny Lau]

it's the cocycle condition right

[Kevin Buzzard]

https://github.com/anca797/group-cohomology

[Kevin Buzzard]

@Anca Ciobanu 's definition of a 1-cocycle is in that link.

[Kevin Buzzard]

She's doing 3rd year project with me.

[Kevin Buzzard]

We're just trundling along learning about cocycles.

[Kevin Buzzard]

So can you make a cocycle from something which people call the cocycle condition?

[Kevin Buzzard]

Anca is going to prove the long exact sequence of terms of low degree coming from the spectral sequence of group cohomology.

[Kevin Buzzard]

We're nearly there.

[Reid Barton]

People always call it the cocycle condition when gluing sheaves and things like that, but it actually becomes one if you imagine gluing vector bundles, say, on a topological space, each of which is trivial so we can call it $\mathbb{R}^n$, and then the transition functions $\phi$ can be seen as taking values in $GL(n)$.

[Kevin Buzzard]

So there's your homework @Kenny Lau

[Reid Barton]

It's not group cohomology though, it's some kind of nonabelian Cech cohomology ($H^1$)

[Reid Barton]

Unless your space happens to be the classifying space of a group in which case it might also be group cohomology

[Kevin Buzzard]

Working with group cohomology H^1 as 1-cocycles over 1-coboundaries has been really interesting. I had not realised that the boundary map from H^0 to H^1 was non-computable until recently.

[Kevin Buzzard]

I'm sure there's some crazy spectral sequence way to do all this, but having the really explicit cocycle stuff was still an interesting exercise, and quite a concrete way of doing it.

[Kevin Buzzard]

For the purposes of this exercise, can I make subset inclusion a typeclass and make all the lemmas I'm using again and again equal to instances?

[Johan Commelin]

You can certainly do that locally, I guess.

[Reid Barton]

But can you glue the local instances into global instances?

[Johan Commelin]

They need to satisfy a cocycle condition, I guess (-;

[Kevin Buzzard]

Fortunately I think that cocycle condition is vacuous for some reason, possibly proof irrelevance

[Kevin Buzzard]

It's somehow the statement that the direct proof that W is a subset of U is the same as the proof that says that W is a subset of V which is a subset of U

[Kevin Buzzard]

@Mario Carneiro

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)

So you really do not care that there is a Type v mentioned in a structure field, where v is a universe not mentioned before the colon?

[Kevin Buzzard]

I thought you one told Patrick that he would get into trouble with this, and there would be annoying universe issues everywhere. Am I just being too paranoid here? I still don't understand this issue. I have been led to suspect that your definition is asking for trouble later down the line.

[Kevin Buzzard]

@Kenny Lau what do you think of all these universes? Is Mario's way the correct way to do it or just a waste of time?

[Kevin Buzzard]

I am unclear about this foundational issue.

[Kenny Lau]

this one is fine; the one that bugs me is when you want to quantify over all sets in ZFC, but there isn't an equivalent in type theory, i.e. you can only quantify over all types in Type w

[Kevin Buzzard]

I guess I might have defined something like a glueing of a presheaf of types using Kenny's API. I will try and write this up in a coherent manner right now.

[Kevin Buzzard]

Me trying to glue presheaves

[Kevin Buzzard]

I'm trying to remove all dependency on the schemes project and just make this a little "glueing sheaves" project of its own without all the Spec A stuff. Kenny I'm porting what you wrote to Mario's foundations. It's quite interesting.

[Kevin Buzzard]

I can use regexps to help with the porting. It's pretty cool. VS Code good for this sort of thing.

[Kevin Buzzard]

I find emacs Lean easier to use than VS Code Lean for this stuff. I just know how to do stuff like "search and replace from this point on" in emacs. This is the first time I've used Lean in emacs for ages.

[Kevin Buzzard]

This file only depends on mathlib.

https://github.com/kbuzzard/xena/blob/e524026fa8db94b228b99fe8d500a530de1bf14e/Examples/sheaf_on_opens_total_glueing.lean#L138

I have my first universe issue @Kenny Lau

[Kevin Buzzard]

I really don't care about universes. Can someone just tell me the regex to fix all universe issues?

[Kenny Lau]

change universes u v to universes v u on L10

[Kevin Buzzard]

Many thanks Kenny.

[Kevin Buzzard]

def opens.Union {I : Type*} (s : I →α) :α :=
⟨set.Union (λ i, (s i).1), is_open_Union (λ i, (s i).2)⟩

@Kenny Lau how do I translate that into this semilattice language?

[Kenny Lau]

I mean it doesn't compile right

[Kevin Buzzard]

That's right. I need to take infinite unions at this point.

[Kevin Buzzard]

But I only have [semilattice_inf]

[Kevin Buzzard]

I need more than this to make sense of glueing presheaves. I definitely want my parameter to be {I : Type*} (s : I → α) and I want to take some kind of sup, which has all the properties of sup which I'll need later.

[Kevin Buzzard]

which is this:

theorem subset_Union : ∀ (s : I → α) (i : I), s i ≤ Union s := (some constructor or other)

[Kevin Buzzard]

What mathematical object is that called in Lean?

[Kevin Buzzard]

I need Union and subset_Union. I'm assuming someone has already discovered this object. @Mario Carneiro @Reid Barton any ideas? @Johannes Hölzl if you're out there?

[Kevin Buzzard]

How close is this to a topological space?

[Kevin Buzzard]

Is it some sort of bundled topological space?

[Kevin Buzzard]

Oh, is it precisely opens X or something?

[Kevin Buzzard]

I could even try and prove this!

[Reid Barton]

Not at a computer but is it just about being able to form sups of arbitrary families?

[Reid Barton]

Sounds like you just have a complete lattice

[Kevin Buzzard]

Yes I think that's it. Many thanks Reid. I should be able to literally check this in Lean in quite a formulaic way.

[Kevin Buzzard]

@Reid Barton is there this:

def complete_lattice.Union : Π {I : Type 37}, (I → α) → α

?

[Reid Barton]

I don't know offhand whether it already exists, but you can define it as the sup of the range of the (I → α)

[Kevin Buzzard]

For glueing presheaves I really do not want to restrict myself to glueing on a set of subsets. I believe want to allow these more general unions. This is not a universe issue (at least as far as I'm concerned -- a topological space has a set of subsets). Before I press on, can I check that I have named this function correctly? @Kenny Lau ?

[Kenny Lau]

I'm not very sure what you want to do. Isn't this just supr?

[Kevin Buzzard]

This is a situation where I would just let I and alpha be in the same universe.

[Kevin Buzzard]

I don't know anything about lattices.

[Kevin Buzzard]

The API is huge and I've never looked at it.

[Kevin Buzzard]

Lattices are just weird computer science things that people like @Johannes Hölzl enjoy. They're not proper maths ;-)

[Kevin Buzzard]

That's why I'm happy to call my types \alpha in this development. I don't think a complete lattice deserves a name in maths mode -- a "maths name".

[Kevin Buzzard]

@Kenny Lau

#check complete_lattice.supr -- unknown

[Kenny Lau]

#check lattice.supr

[Kevin Buzzard]

Is complete_lattice.supr a hole in mathlib? @Mario Carneiro ?

[Kevin Buzzard]

Just thinking abstractly about the concept of what setting we need in order to do glueing of sheaves, has led me to a type which has grown organically. It would be interesting if it was precisely complete_lattice or maybe it will be some other known type. It gives some sort of insight into the correct way to think about glueing sheaves. We throw in axioms as we need them and see what we end up growing.

[Kevin Buzzard]

#check @lattice.supr
supr : Π {α : Type u_1} {ι : Sort u_2} [_inst_1 : has_Sup α], (ι → α) → α

Is that order preferred to

supr : Π {α : Type u_1} [_inst_1 : has_Sup α] {ι : Sort u_2}, (ι → α) → α

? Is there some convention?

[Kevin Buzzard]

@Reid Barton

[Kevin Buzzard]

def complete_lattice.supr (α : Type u) (I : Type v) [X : complete_lattice α] :=
  @lattice.supr α I _ -- Grumpy old mathematician observes that stupid polymorphism
                      -- makes me have to fill in more stuff

theorem complete_lattice.subset_Union [X : complete_lattice α] :
  ∀ {I : Type} (s : I → α) (i : I), s i ≤ supr s := sorry

There's a conjecture for you complete_latticeists.

[Kevin Buzzard]

I need to learn your language.

[Kevin Buzzard]

Oh I guess I know exactly where to look in the mathlib API.

[Kevin Buzzard]

le_supr : ∀ (s : ?M_2 → ?M_1) (i : ?M_2), s i ≤ supr s

Porting this code is really interesting. I'm trying to see if I can do it in a completely algorithmic way. I think I'm nearly there.

[Reid Barton]

I think the order of implicit and type class arguments is usually arbitrary and depends on how it was convenient to organize the variable declarations

[Kevin Buzzard]

def complete_lattice.le_supr : ∀ {α : Type u} {ι : Sort v} [complete_lattice α] (s : ι → α) (i : ι),
  s i ≤ supr s := sorry
/-
failed to synthesize type class instance for
α : Type u,
ι : Sort v,
_inst_1 : complete_lattice α,
s : ι → α,
i : ι
⊢ has_le α
sheaf_on_opens_total_glueing.lean:15:8: error
failed to synthesize type class instance for
α : Type u,
ι : Sort v,
_inst_1 : complete_lattice α,
s : ι → α,
i : ι
⊢ has_Sup α
-/

What have I done to deserve this??

[Kevin Buzzard]

import order.complete_lattice

-- #check lattice.le -- unknown identifier
#check lattice.lattice.le -- but this works??

Is that a poorly-named function in mathlib?

[Kevin Buzzard]

instance (α : Type u) [complete_lattice α] : has_le α := by apply_instance
/-
failed to synthesize instance name, name should be provided explicitly
-/

What should this be instance be called?

[Kevin Buzzard]

Why is this happening?

[Kevin Buzzard]

import order.complete_lattice

-- #check lattice.le -- unknown identifier
#check lattice.lattice.le -- should this work?

universes u v

open lattice

def complete_lattice.le (α : Type u) [complete_lattice α] := @lattice.lattice.le

instance I_DONT_KNOW_WHY_I_NEED_TO_NAME_THIS_INSTANCE
  (α : Type u) [complete_lattice α] : has_le α := by apply_instance

def WHAT_IS_GOING_ON (α : Type u) [complete_lattice α] : has_Sup α := by apply_instance

def complete_lattice.le_supr : ∀ {α : Type u} {ι : Sort v} [complete_lattice α] (s : ι → α) (i : ι),
  @has_le.le α (by resetI; exact I_DONT_KNOW_WHY_I_NEED_TO_NAME_THIS_INSTANCE α) (s i) (@supr α ι (@WHAT_IS_GOING_ON α (by resetI; apply_instance))) s := sorry #exit

This is not going well. What am I doing wrong?

[Reid Barton]

You put the [complete_lattice \a] to the right of the colon

[Kevin Buzzard]

bleurgh thanks. I am sort-of generating the code algorithmically, you're just finding bugs in my algorithm.

[Kevin Buzzard]

I am writing some completely mechanical code, made possible because of excellent naming conventions @Mario Carneiro

[Kevin Buzzard]

theorem complete_lattice.subset_Union [X : complete_lattice α] {I : Type} (s : I → α) (i : I) : s i ≤ supr s :=
complete_lattice.le_supr s i

There's some sort of dictionary going between subset land and lattice land. subset_Union becomes le_supr.

[Kevin Buzzard]

When I manipulate terms of type opens X, is the canonical way to manipulate them using the language of complete lattices?

[Kevin Buzzard]

Is that the language that the simp lemmas will be in?

[Kevin Buzzard]

Oh my goodness I just found lattice.complete_lattice.le. What's it doing down there? Complete lattices are actually called lattice.complete_lattice

[Kevin Buzzard]

Is that how it works? Who decided that lattice was a top level thing but complete_lattice wasn't?

[Mario Carneiro]

this is a naming bug which we haven't done anything about yet

[Mario Carneiro]

the lattice.lattice thing is obviously not good

[Mario Carneiro]

I think far too much stuff ended up in the lattice namespace, including lattice itself

[Kevin Buzzard]

Is the naming bug because lattice.complete_lattice is a class which is doesn't have a top level name?

[Kevin Buzzard]

def lattice.complete_lattice.has_le
  (α : Type u) [complete_lattice α] : has_le α := by apply_instance

or

def lattice.complete_lattice.has_le
  {α : Type u} [complete_lattice α] : has_le α := by apply_instance

? Why? And should it be an explicit instance or should it just remain undefined?

[Kevin Buzzard]

I feel like if I ever had to mention this name then something had gone wrong, because there's only one le on a complete lattice.

[Mario Carneiro]

What are you doing?

[Mario Carneiro]

you shouldn't need to write anything remotely close to either of those

[Mario Carneiro]

you should write <= and be done with it

[Kevin Buzzard]

I'm just learning about complete lattices. I've never heard of them. I'm learning the language of complete lattices.

[Mario Carneiro]

lattice is a top level namespace like category_theory

[Mario Carneiro]

it encloses most of the lattice-related constants

[Mario Carneiro]

but like I said, I think it should be removed

[Mario Carneiro]

Most of the time people open lattice for this reason

[Mario Carneiro]

I'm amused you think complete lattices are a CS thing

[Kevin Buzzard]

They're being called alpha in the repo. That is an insult as far as I am concerned

[Kevin Buzzard]

They don't deserve a maths name

[Mario Carneiro]

Huh? that's pretty standard in mathlib

[Kevin Buzzard]

I know but I tell my undergraduates to use maths notation for mathsy stuff

[Mario Carneiro]

what notation are you going to give complete_lattice? That's plain text in maths

[Kevin Buzzard]

That group cohomology repo is all done with $$G$$s and $$M$$s just like in the maths books. No alphas at all

[Kevin Buzzard]

I will never have to mention complete lattices in maths texts. They are beneath mathematicians. They are just some tool that people like Johannes like

[Mario Carneiro]

I'm sure if you had written complete lattices it would use L as well

[Kevin Buzzard]

That's an interesting suggestion

[Kevin Buzzard]

I tend to use the notation that mathematicians use you see

[Mario Carneiro]

I would say that mathlib had a convention for this, and you and others didn't like it, and now we have inconsistency re: variable names

[Mario Carneiro]

and I don't care enough to do anything about it

[Kevin Buzzard]

But I've never seen a mathematician talking about compete lattices in the number theory seminar

[Kevin Buzzard]

The maths stuff gets maths names and the weird stuff can have computer science names.

[Kevin Buzzard]

Maybe the maths conventions should just have one universe too

[Kevin Buzzard]

:-)

[Mario Carneiro]

I don't know why we are on this again, but the only difference is lattices were written before the rebellion

[Mario Carneiro]

I can't be bothered to tell the difference between types, so I call types of things alpha and index types iota and that's about it

[Mario Carneiro]

I have no idea what letter is preferred for these things, I'm not a group theorist

[Mario Carneiro]

I just want library-wide consistency

[Mario Carneiro]

But since variable names don't affect the applicability of a theorem, I don't really care what names are chosen, so if you want to call it G in your own files then go ahead

[Kevin Buzzard]

I can't appeal to alpha-equivalence? ;-)

[Kevin Buzzard]

Anyway, that's got nothing to do with what I'm doing, what I'm doing is wondering whether the natural domain for glueing sheaves of types is complete lattices.

[Mario Carneiro]

based solely on your statements, yes

[Mario Carneiro]

I used a semilattice_inf for the definitions I showed because I didn't actually need a union operator, only a axiom that quantifies over lubs

[Mario Carneiro]

but if you want to actually take some arbitrary subset and "take its union" then you need a complete_lattice

[Kevin Buzzard]

I might be able to get away with just the predicate "the sup of this set is the max"

[Mario Carneiro]

I did something like that in the sheaf axioms

[Kevin Buzzard]

but I sort-of feel that Assia would be frowning.

[Mario Carneiro]

The question is whether this compromises the meaning of the statement in the case that no lub exists

[Kevin Buzzard]

i think that in the odd order project the idea was to just ignore the big ambient group

[Kevin Buzzard]

Let's call it 37 in that case.

[Mario Carneiro]

that will definitely compromise the meaning of the statement

[Kevin Buzzard]

only in your mind

[Kevin Buzzard]

We know what we're doing in the maths department

[Mario Carneiro]

I'm not talking about totalizing a function, I'm talking about statements that require a lub

[Mario Carneiro]

like gluing

[Kevin Buzzard]

OK just make it to option.

[Mario Carneiro]

sure, but again I'm not talking about totalization

[Mario Carneiro]

what does the theorem say if you apply it to a set with no lub?

[Kevin Buzzard]

I do not care because I will always supply a proof that the lub exists in practice.

[Mario Carneiro]

what if there is no lub?

[Kevin Buzzard]

I promise there is a lub

[Mario Carneiro]

if it's a semilattice_inf there may not be a lub

[Kevin Buzzard]

well there are lubs in the only model I'm interested in, which is opens

[Mario Carneiro]

the question of whether to "upgrade" to complete_lattice lies in whether the statements break down in the absence of lubs

[Kevin Buzzard]

And I say that that's your problem

[Kevin Buzzard]

because I promise I will never run that code in the absence of an upper bound

[Kevin Buzzard]

like I promise I will never take the square root of a negative number, even though you let me.

[Mario Carneiro]

this is more the opposite problem - you don't have the language to say something that you want to say

[Mario Carneiro]

I'm not sure why you are so against contemplating such a simple generalization of sheaves when apparently you have much more complicated generalizations in mind

[Mario Carneiro]

I can't answer this question because I don't know what sheaves are beyond the definitions I've seen

[Kevin Buzzard]

You just have to wait for me to catch up Mario :-) I'll get there in the end. I don't know how to steer complete lattices, and I am running into Lean issues which I don't understand. For example

type mismatch at field 'le_sup_left'
  sorry
has type
  ∀ (a b : α), semilattice_inf.le a (?m_1 a b)
but is expected to have type
  ∀ (a b : α), a ≤ a ⊔ b

I hate it when sorry is underlined in red.

[Mario Carneiro]

One thing I'm not a big fan of in the lattice theorems is the large number of implicit parameters

[Mario Carneiro]

it can cause some unification problems

[Mario Carneiro]

but I can't diagnose that problem based on the error alone. What's the context?

[Kevin Buzzard]

I really have no clue about whether to use {} or (). I used to think it was "use {} if and only if you can work it out from all the () stuff, but that's not always the rule. Probably you Mario know some examples of this.

[Mario Carneiro]

that is the rule, and the lattice theorems don't follow it

[Kevin Buzzard]

https://github.com/kbuzzard/xena/blob/1284a71aa327040494f13babb336c73d41680787/Examples/sheaf_on_opens_total_glueing.lean#L274

[Kevin Buzzard]

that is the rule, and the lattice theorems don't follow it

Is this a bug? What is the name for this issue? They don't follow it for a good reason, right?

[Kevin Buzzard]

Should one just force the unconventional functions to have a ' in their name, like the quotient' stuff?

[Mario Carneiro]

what the heck is going on in your file? What is thing?

[Jesse Michael Han]

You just have to wait for me to catch up Mario :-) I'll get there in the end. I don't know how to steer complete lattices, and I am running into Lean issues which I don't understand. For example

type mismatch at field 'le_sup_left'
  sorry
has type
  ∀ (a b : α), semilattice_inf.le a (?m_1 a b)
but is expected to have type
  ∀ (a b : α), a ≤ a ⊔ b

I hate it when sorry is underlined in red.

For some reason, Lean believes the sorry is an inequality taking place in semilattice_inf land, which doesn't have a sup instance

maybe because earlier you filled in some holes with things in semilattice_inf land

[Mario Carneiro]

This issue comes up sometimes when you have a large hierarchical class where you fill everything in with underscores

[Mario Carneiro]

If you fill everything with sorry instead it should work

[Mario Carneiro]

but if you fill early stuff with underscore and later stuff with sorry then it will fail

[Kevin Buzzard]

what the heck is going on in your file? What is thing?

I'm just exploring. This is all your fault. You said "what generality do you want to do glueing in to create a milestone". For me the milestone is a construction of glueing sheaves.

[Kevin Buzzard]

So you said "ok I'll write it all properly, will topological spaces do?" and I said "yeah" and then next thing you know we have bloody lattices.

[Mario Carneiro]

For your reference, if you have a partial order with a supr function, then you can prove it has a complete lattice structure

[Kevin Buzzard]

So you dragged me here and now you have to wait around until I've finished exploring.

[Kevin Buzzard]

For your reference, if you have a partial order with a supr function, then you can prove it has a complete lattice structure

I am using the stupidest constructors imaginable.

[Mario Carneiro]

which is to say, your definitions are provable. It won't be that much fun to do

[Kevin Buzzard]

I am trying to write the code algorithmically, and my algorithm says "just do what the lean hole structure command thing says"

[Kevin Buzzard]

You and I have different ideas about fun.

[Mario Carneiro]

If you really want to do this you should break up the proof into the different parts of the hierarchy

[Kevin Buzzard]

I'm just trying to understand how much work it is to make mathlib's definition of lattice.complete_lattice from scratch, in some sense.

[Mario Carneiro]

I think this might be proven in the complete_lattice.lean file

[Kevin Buzzard]

If you really want to do this you should break up the proof into the different parts of the hierarchy

I'm still learning things about the structure which I am building. How should I be ordering things? There are two files in the Xena project.

[Kevin Buzzard]

I think this might be proven in the complete_lattice.lean file

Hey, why is that file not called lattice/complete_lattice.lean?

[Kevin Buzzard]

I think there are several questions I've raised in this thread that are still not really answered.

[Mario Carneiro]

some of this is architectural stuff you should ask Johannes

[Mario Carneiro]

I recall the entire thing being committed in one huge block that gave us filters and complete lattices and topology, and I wasn't super happy about all the design decisions but I didn't want to bikeshed forever so I merged it

[Mario Carneiro]

so you are asking me a lot of hard questions about stuff where I mostly agree with you. Don't assume everything in mathlib is optimal

[Kevin Buzzard]

I really like learning about this stuff. I got rid of the red sorry :-) Thanks for all your help this evening. I find this very interesting stuff.

[Mario Carneiro]

First you want to prove it's a lattice

[Kevin Buzzard]

golly it's 4am

[Mario Carneiro]

then you prove it's a complete lattice

[Kevin Buzzard]

First you want to prove it's a lattice

How did you know that?

[Kevin Buzzard]

My algorithm is buggy here.

[Mario Carneiro]

because that's the way the hierarchy is set up

[Kevin Buzzard]

But how can I work that out for myself?

[Mario Carneiro]

it's actually broken up into quite a few more pieces than that

[Mario Carneiro]

look at the extends clauses

[Kevin Buzzard]

I want to learn how to write good structures. I am a really bad structure-writer, and I am now indicating that I am also a really bad structure-maker.

[Mario Carneiro]

Ignoring the notation typeclasses, you have complete_lattice <- bounded_lattice <- lattice, order_top, order_bot and lattice <- semilattice_sup, semilattice_inf <- partial order

[Mario Carneiro]

So to keep it organized, you should try to first show partial_order foo, then semilattice_inf foo and semilattice_sup foo, then lattice foo and order_top foo and order_bot foo, then bounded_lattice foo, then complete_lattice foo

[Mario Carneiro]

In practice you can skip some of those steps by proving them simultaneous with other steps, but you should realize that when a later typeclass has an axiom that uses a notation provided by an earlier typeclass, the proof that you are in that typeclass appears as an argument

[Kevin Buzzard]

Had to fix the errors before bed :-)

https://github.com/kbuzzard/xena/blob/master/Examples/sheaf_on_opens_total_glueing.lean

Challenge 1: glue presheaves of types on opens
Challenge 2 : glue sheaves of types on opens.
Challenge 3 : glue sheaves of rings on opens.

[Mario Carneiro]

For example, consider the following:

class A (α : Type) :=
(zero : α)
(one : α)
(zero_ne_one : zero ≠ one)

class B (α : Type) extends A α :=
(pos : α → Prop)
(one_pos : pos one)

instance : B nat :=
{ zero := 0,
  one := 1,
  zero_ne_one := zero_ne_one,
  pos := λ x, x > 0,
  one_pos := _ }

Notice that I've proven both A nat and B nat in one go. The printed type of pos_one is A.one ℕ > 0, but how could it say A.one ℕ if A nat hasn't been proven yet? The truth is that if you look at the typeclass args, you find that the provided instance is

{ zero := 0,
  one := 1,
  zero_ne_one := zero_ne_one }

that is, the full proof that you just wrote above it

[Mario Carneiro]

This happens every time one axiom references a parent instance, and it's even worse the deeper the nesting you prove in one go

[Mario Carneiro]

this can lead to serious performance problems if you aren't careful (plus the pp.all size grows exponentially which isn't great either)

[Kevin Buzzard]

type mismatch at field 'inf_le_left'
  complete_lattice.inf_le_left
has type
  ∀ (a b : α),
    @has_le.le α
      (@preorder.to_has_le α
         (@partial_order.to_preorder α
            (@partial_order.mk α (@lattice.complete_lattice.le α X) (@lattice.complete_lattice.lt α X) _ _ _ _)))
      (@lattice.has_inf.inf α (@lattice.has_inf.mk α (@lattice.complete_lattice.inf α X)) a b)
      a
but is expected to have type
  ∀ (a b : α),
    @has_le.le α
      (@preorder.to_has_le α
         (@partial_order.to_preorder α
            (@partial_order.mk α
               (λ (a a_1 : α), @has_le.le α (@has_le.mk α (@lattice.complete_lattice.le α X)) a a)
               (@partial_order.lt._default α
                  (λ (a a_1 : α), @has_le.le α (@has_le.mk α (@lattice.complete_lattice.le α X)) a a))
               _
               ?m_1
               ?m_2
               ?m_3)))
      (@lattice.has_inf.inf α (@lattice.has_inf.mk α ?m_4) a b)
      a

Why am I in this mess? :-/

[Kevin Buzzard]

https://github.com/kbuzzard/xena/blob/99cd50f01ca068d0e8796a7900f6e1a16fa8ff35/Examples/sheaf_on_opens_total_glueing.lean#L289

why u hate me Lean

[Kevin Buzzard]

Oh I just have to fill in random fields and hope.

[Kevin Buzzard]

All I know is that Lean wants me to prove ?m_1 etc

[Kevin Buzzard]

1 goal
α : Type u,
_inst_2 : bounded_lattice α,
_inst_3 : has_Sup α,
_inst_4 : has_Inf α,
X : complete_lattice α,
_inst : has_inf α := semilattice_inf.to_has_inf α,
_inst_1 : partial_order α := order_bot.to_partial_order α
⊢ (∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) ↔ ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c

by refl doesn't work. Presumably I have got my instances wrong?

[Kevin Buzzard]

I genuinely don't know how I am supposed to make one of these lattice classes. I'm in all sorts of trouble.

[Kevin Buzzard]

theorem semilattice_inf.ext_inf {α} {A B : semilattice_inf α}
  (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)
  (x y : α) : (by haveI := A; exact (x ⊓ y)) = x ⊓ y :=
eq_of_forall_le_iff $ λ c,
by simp only [le_inf_iff]; rw [← H, @le_inf_iff α A, H, H]

That's in mathlib, in order/lattice.lean. What's going on there?

[Kevin Buzzard]

Oh I get it, I just look at the constructor duh. It would be cool if that hole command which spat out structure fields which need to be made, could take this sort of thing into account. I'm all for automation, I'm always using that hole command. Oh I'm back on track now.

[Mario Carneiro]

This is what I mean by proving them one step at a time rather than all in one go

[Mario Carneiro]

if you try to prove them in the wrong order, your goals make no sense

[Mario Carneiro]

but lean and the hole command make it look like order doesn't matter, which is only true after you are done proving everything

[Kevin Buzzard]

What's the trick to do all of the semilattice fields at once?

def canonical2.to_fun (α : Type u)
[bounded_lattice α] [has_Sup α] [has_Inf α]
[lattice.complete_lattice α] : thing α :=
begin
--let this : semilattice_inf α := by apply_instance,
refine { inf := begin exact semilattice_inf.inf end,
         le := semilattice_inf.le,
         le_refl := semilattice_inf.le_refl,
         le_trans := semilattice_inf.le_trans,
         le_antisymm := semilattice_inf.le_antisymm,
  --       inf_le_inf := semilattice_inf.inf_le_inf,
         inf_le_left := semilattice_inf.inf_le_left,
         inf_le_right := semilattice_inf.inf_le_right,
         le_inf := semilattice_inf.le_inf,
          -- the rest are not from semilattice namespace
         le_supr := λ ι s, begin convert lattice.complete_lattice.le_supr s, sorry end,
         supr := λ ι s, lattice.complete_lattice.supr s,
         },
end

And have I got my typeclasses right? Still not entirely confident on these things.

[Kevin Buzzard]

if you try to prove them in the wrong order, your goals make no sense

How do I work out the correct order to prove them?

[Mario Carneiro]

Look at the definition of complete_lattice, it extends bounded_lattice so you should prove stuff about bounded lattice before you do stuff involving Sup and Inf

[Mario Carneiro]

You should not have [bounded_lattice α] [has_Sup α] [has_Inf α] [lattice.complete_lattice α] because complete_lattice contains another copy of the first three

[Mario Carneiro]

That direction should be relatively easy, if you open lattice then the proof should just be supr := supr and le_supr := le_supr

[Kevin Buzzard]

I have a universe issue.

kernel failed to type check declaration 'canonical2.to_fun' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Π (α : Type u) [_inst_1 : complete_lattice α], thing α
elaborated value:
  λ (α : Type u) [_inst_1 : complete_lattice α],
    {to_semilattice_inf := {inf := semilattice_inf.inf (semilattice_inf_bot.to_semilattice_inf α),
                            le := semilattice_inf.le (semilattice_inf_bot.to_semilattice_inf α),
                            lt := partial_order.lt._default semilattice_inf.le,
                            le_refl := _,
                            le_trans := _,
                            lt_iff_le_not_le := _,
                            le_antisymm := _,
                            inf_le_left := _,
                            inf_le_right := _,
                            le_inf := _},
     supr := λ (ι : Sort v) (s : ι → α), complete_lattice.supr s,
     le_supr := _}
nested exception message:
invalid reference to undefined universe level parameter 'v'

[Mario Carneiro]

oh right, thing has a universe issue in its definition because v is free

[Kevin Buzzard]

thing.{v} α

[Kevin Buzzard]

got it

[Mario Carneiro]

You should either use u in place of v , or do the same thing as complete_lattice and axiomatize Sup instead of supr

[Mario Carneiro]

You can't properly axiomatize supr because of the required existential universe variables

[Kevin Buzzard]

I don't really understand what is going on here, as my code probably indicates.

[Mario Carneiro]

My original claim that thing is equivalent to complete_lattice is actually false with v used the way it currently is

[Mario Carneiro]

If v is less than u then you are actually claiming only the existence of "small suprema"

[Kevin Buzzard]

Because I am universe-monomorphic I do not recognise this issue.

[Mario Carneiro]

As a simpler analogue, it's as if you are only asking for countable suprema

[Kevin Buzzard]

That's an interesting analogue

[Mario Carneiro]

if the set itself is not countable it should not be a surprise that this isn't the same as being complete

[Kevin Buzzard]

But another observation is presumably that if Type u and Sort v are just Type then the problem goes away?

[Mario Carneiro]

More specifically, if you set v = u then the problem goes away

[Kevin Buzzard]

Is that right? That would be really nice. I thought the Sort stuff might mess things up.

[Mario Carneiro]

or like I said, if you restrict the indexing set to be subsets of the original space

[Kevin Buzzard]

or like I said, if you restrict the indexing set to be subsets of the original space

I can't do that for glueing schemes.

[Mario Carneiro]

sure you can

[Mario Carneiro]

do you have an example?

[Kevin Buzzard]

You think that the set-valued version of glueing implies the Union version?

[Mario Carneiro]

Yes

[Kevin Buzzard]

I had not realised this

[Mario Carneiro]

The definition I gave of gluing and locality uses subsets

[Kevin Buzzard]

The set-valued version will only use one universe, right?

[Mario Carneiro]

it actually only uses one type, which is in the same universe as the original

[Kevin Buzzard]

I know that gluing and locality use subsets, but they are conceptually simpler than gluing sheaves. They are gluing sections.

[Mario Carneiro]

okay you are going to have to give me a code snippet to back that statement up

[Mario Carneiro]

what are the types of the relevant objects?

[Kevin Buzzard]

This is the thing I want:

def universal_property (I : Type*) (S : I → α) (F : Π (i : I), sheaf_on_opens.{v} α (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :
∀ i : I, equiv (res_subset (glue S F φ Hφ1 Hφ2) (S i) $ opens.subset_Union S i) (F i) := sorry

[Kevin Buzzard]

If you can make the type of an analogous "set version" of this term which mentions no I and no Sort v and replaces S with some kind of set thing, sorry it, and then prove the universal property I want from your set one, then I will understand why the set one suffices.

[Mario Carneiro]

This is a theorem, though, right?

[Kevin Buzzard]

I don't know.

[Mario Carneiro]

you wrote := sorry so I assume so

[Mario Carneiro]

this is supposed to follow from the axioms of sheaves

[Kevin Buzzard]

I don't know if it's true. It's a conjecture.

[Kevin Buzzard]

Assuming Kenny and I have formalised it correctly, that should be true. It's an exercise in Hartshorne.

[Kevin Buzzard]

Exercise 1.22 of one of the early chapters.

[Mario Carneiro]

the proof args make me weep

[Kevin Buzzard]

Just tell me how to do it.

[Kevin Buzzard]

I don't have a clue what I'm doing. I know enough Lean to be able to solve problems I run into, and I just blunder on.

[Kevin Buzzard]

Probably chapter 2, I think section 2.1 is sheaves.

[Johan Commelin]

@Kevin Buzzard Did you just pull an all-nighter gluing sheaves :lol:

[Mario Carneiro]

There are two ways forward: the way I've been championing that tries to hide proof args, or the category theory way that makes the proof args the only thing and hides the objects

[Kevin Buzzard]

And another conjecture is that if T is a type with the discrete topology, and if F(U) is defined to be the continuous maps from U to T, then the cocycle condition should give us a 1-cocycle with values in Aut(T) or something. This might be nonabelian sheaf cohomology though, which we didn't formalise yet. Anca only did abelian group H1.

[Kevin Buzzard]

Kevin Buzzard Did you just pull an all-nighter gluing sheaves :lol:

My partner is away :-)

[Kevin Buzzard]

There will be an easier universal property just for presheaves of types. I might have done this one.

[Kevin Buzzard]

In the opens case, not in the lattice case.

[Kevin Buzzard]

instance has_sup (α : Type u) [semilattice_inf α] (Y : thing α) : has_sup α :=
{ sup := λ a b, @thing.supr α Y bool (@bool.rec (λ _, α) a b)}

Will this instance never trigger?

[Kevin Buzzard]

I rolled my own sup from supr

[Kevin Buzzard]

and now I have universe issues :-(

type mismatch at application
  thing.has_sup α Y
term
  Y
has type
  thing.{u_1 u} α : Type (max u u_1)
but is expected to have type
  thing.{1 u} α : Type (max u 1)
state:
α : Type u,
H : semilattice_inf α,
Y : thing α
⊢ Sort ?

stupid bool. Did I need a ubool or something?

[Mario Carneiro]

you can use ulift bool

[Kevin Buzzard]

I don't understand the universe combinatorics well enough to know which universe I should be lifting to.

[Kevin Buzzard]

type mismatch at application
  thing.has_sup α Y
term
  Y
has type
  thing.{u_1 u} α : Type (max u u_1)
but is expected to have type
  thing.{?l_1+1 u} α : Type (max u (?l_1+1))
state:
α : Type u,
H : semilattice_inf α,
Y : thing α
⊢ Sort ?

I can't even solve the equations.

[Kevin Buzzard]

instance (α : Type u) (Y : thing α) : semilattice_inf α := thing.to_semilattice_inf Y
-- example (α : Type u) (Y : thing α) : semilattice_inf α := by apply_instance -- fails

I can't get this instance to fire. Do I have to make thing a class to proceed more smoothly?

[Mario Carneiro]

Why does thing still take two universe args?

[Kevin Buzzard]

I'm scared Mario

[Mario Carneiro]

I'm still not clear on exactly what the goal is

[Kevin Buzzard]

I am not sure that sets are enough for glueing

[Mario Carneiro]

You aren't using sets

[Mario Carneiro]

I managed to prove that sheaf has a comap operation, will show

[Kevin Buzzard]

I'll formalise the thing I'm not sure whether to believe.

[Mario Carneiro]

https://gist.github.com/digama0/2ee44987e8613b41c24536ddcde86d35

[Mario Carneiro]

That's equivalent to the theorem that you can make a sheaf on a subset

[Kevin Buzzard]

infixr ` ↪⊓⨆ `:25 := semilattice_inf_lub_emb

I'm liking that.

[Kevin Buzzard]

I cannot formalise the "can sheaf glueing be done on subsets WLOG" goal until someone has ported Kenny's work on glueing to Mario's framework.

[Mario Carneiro]

That's the goal

[Johan Commelin]

It seems to me that half of that file is duplicating things that we have in category_theory/ already...

[Kevin Buzzard]

It's normally @Scott Morrison who says that. I don't know too much about the category theory library either.

[Johan Commelin]

In fact, we already have the definition of presheaf in mathlib + a bunch of other abstract generalities. I think it would make a lot of sense to build the sheaf condition on top of that.

[Kevin Buzzard]

But is it a presheaf over a complete lattice?

[Kevin Buzzard]

Oh it's some category definition, right? It's a functor. I think it would be an interesting question to see how much fun it was to formalise sheaf glueing in that language. I think it would be more difficult than what Mario is doing.

[Mario Carneiro]

One thing that the category formulation will give you is a much easier way to do this stuff

  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :

with diagrams

[Johan Commelin]

You can still just work over complete lattices.

[Johan Commelin]

So do the sheafy part the way you've been doing it. But just use the existing presheaves, instead of rolling your own.

[Johan Commelin]

The definition of presheaf and functor or defeq up to eta for records...

[Kevin Buzzard]

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 _ _ _ _ _ }

This is much harder for sheaves; one might need some extra assumptions on alpha to make it work.

[Kevin Buzzard]

You have to "sheafify".

[Kevin Buzzard]

Apply the adjoint functor to the forgetful functor from sheaves to presheaves.

[Mario Carneiro]

Here's presheaves:

import topology.Top.presheaf

universes u v
open category_theory
open topological_space
open opposite

def presheaf' (α : Type v) [topological_space α]
  (C : Type u) [𝒞 : category.{v+1} C] := (Top.of α).presheaf C

namespace presheaf'

variables (α : Type v) [topological_space α]
  (C : Type u) [𝒞 : category.{v+1} C]
include 𝒞

instance : has_coe_to_fun (presheaf' α C) := ⟨_, λ F U, F.obj (op U)⟩

def res (F : presheaf' α C) {U V : opens α} (f : V ⟶ U) : F U ⟶ F V := F.map f.op

end presheaf'

Not sure how to state the sheaf axioms without elements of the category

[Mario Carneiro]

I don't know why presheaf is stated using a Top argument

[Kevin Buzzard]

You can't make sheaves on an arbitrary category.

[Kevin Buzzard]

You need a notion of covering. This is what a site is.

[Mario Carneiro]

okay, how's that work?

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Grothendieck_topology

[Mario Carneiro]

Wait, this is about the domain category

[Kevin Buzzard]

If you work with categories then that is the correct thing to use.

[Mario Carneiro]

mathlib presheaves are on top spaces

[Kevin Buzzard]

To say what a sheaf is, you have to know what a covering of an open set by open sets is

[Mario Carneiro]

The category here is the target, replacing Type

[Kevin Buzzard]

If you want to define sheaves of types on an arbitrary category, you need the extra structure of a site on that category.

[Mario Carneiro]

I don't

[Kevin Buzzard]

No?

[Mario Carneiro]

I'm just considering top spaces for now, because that's what mathlib presheaves are

[Mario Carneiro]

I just want to know why it's bundled

[Mario Carneiro]

mathlib presheaves could also be generalized to preorder categories, but that's work for another day

[Mario Carneiro]

or general categories, and then you have this site business

[Kevin Buzzard]

def sheaf_on_opens (α : Type u) [semilattice_inf α] (U : α) : Type (max u (v+1)) :=
sheaf.{u v} α

How are you going to port that line to your library?

[Kevin Buzzard]

It might be best to do presheaf_on_opens first

[Mario Carneiro]

sheaf_on_opens U := sheaf {V // V <= U}

[Mario Carneiro]

or more generally a sheaf on some object isomorphic to that

[Kevin Buzzard]

So you really want to carry the subtype around?

[Mario Carneiro]

That's why I defined comap, because subtype.val is an inf_sup_emb

[Mario Carneiro]

But the theory starts to look very categorical at that point, because you need products in the category to replace intersection of subsets

[Kevin Buzzard]

And you think that (a) this will make the gluing of presheaves go better and (b) you will be able to prove the universal property from a set-valued one.

[Kevin Buzzard]

We can just stick to gluing of presheaves. I want to see this trick of going from the set to the parametrised set.

[Mario Carneiro]

I'm not sure I want to actually define sheaf_on_opens U := sheaf {V // V <= U} because then it won't apply cleanly to opens, since opens U (using U as a subset of the topological space as a top space in its own right) is isomorphic but not defeq to {V : opens alpha // V <= U}

[Mario Carneiro]

So you can use something like comap to avoid having to prescribe a particular representation for the type, but at some point you just want to say "intersect these subsets and give me the result" without having to assume the result exists in the first place

[Mario Carneiro]

And this is especially important for the gluing axiom, because it's kind of the whole point that you don't know the glued sheaf exists until you construct it

[Mario Carneiro]

But I'm not sure how to state these axioms in the categorical presentation:

def locality (F : presheaf' α C) :=
∀ {{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' α C) :=
∀ {{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

[Mario Carneiro]

they are too pointed

[Kevin Buzzard]

failed to synthesize type class instance for
α : Type u,
_inst_1 : semilattice_inf α,
U : α
⊢ semilattice_inf {V // V ≤ U}

[Kevin Buzzard]

universes u v

open lattice

variables {α : Type u} [semilattice_inf α]

variable (U : α)
def presheaf_on_opens (U : α) := presheaf {V // V <= U}

[Mario Carneiro]

there's that too

[Kevin Buzzard]

instance {α : Type u} [semilattice_inf α] (U : α) :
  semilattice_inf {V // V ≤ U} := sorry

:-(

[Mario Carneiro]

it's not hard to prove

[Kevin Buzzard]

I just thought it would happen by magic

[Kevin Buzzard]

I am really not good at making any instances of anything with the word lattice in the name.

[Kevin Buzzard]

instance {α : Type u} [semilattice_inf α] (U : α) :
  has_inf {V // V ≤ U} := by apply_instance -- fails

[Kevin Buzzard]

but semilattice_inf extends has_inf

[Mario Carneiro]

you have to define that too

[Mario Carneiro]

aha, this typechecks:

def locality (F : presheaf' α C) :=
∀ {{S : set (opens α)}} {{X}} {{s t : X ⟶ F (Sup S)}},
  (∀ (V ∈ S) (f : V ⟶ Sup S), s ≫ F.res f = t ≫ F.res f) → s = t

def gluing (F : presheaf' α C) :=
∀ {{S : set (opens α)}} {{X}} {{s : Π V ∈ S, X ⟶ F V}},
  (∀ V hV W hW (l : V ⊓ W ⟶ V) (r : V ⊓ W ⟶ W),
    s V hV ≫ F.res l = s W hW ≫ F.res r) →
  ∃ x : X ⟶ F (Sup S), ∀ V hV (f : V ⟶ Sup S), x ≫ F.res f = s V hV

[Mario Carneiro]

the main drawback seems to be that you have to specify the morphism all the time, even though it's unique

[Kevin Buzzard]

import mario_sheaf -- Mario's gist

universes u v

open lattice

variables {α : Type u} [semilattice_inf α]

variable (U : α)

--#print notation →⊓
--#check @semilattice_inf_hom

/-
class semilattice_inf (α : Type u) extends has_inf α, partial_order α :=
(inf_le_left : ∀ a b : α, a ⊓ b ≤ a)
(inf_le_right : ∀ a b : α, a ⊓ b ≤ b)
(le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c)
-/

--#where

namespace semilattice_inf.opens

--#print has_inf.inf

def inf {α : Type u} [semilattice_inf α] (U : α) ( a b : {V // V <= U}) : {V // V <= U} :=
⟨a.val ⊓ b.val, le_trans inf_le_left a.property⟩

instance has_inf {α : Type u} [semilattice_inf α] (U : α) :
  has_inf {V // V ≤ U} := ⟨inf U⟩

example {α : Type u} [semilattice_inf α] (U : α) :
  has_inf {V // V ≤ U} := by apply_instance

example {α : Type u} [semilattice_inf α] (U : α) :
  partial_order {V // V ≤ U} := by apply_instance

instance {α : Type u} [semilattice_inf α] (U : α) :
  semilattice_inf {V // V ≤ U} := {
    inf_le_left --: ∀ a b : α, a ⊓ b ≤ a
      := λ a b, by exact semilattice_inf.inf_le_left a.val b.val,
    inf := (⊓),
    le := (≤),
    le_refl := λ a, semilattice_inf.le_refl a.val,
    le_trans := λ a b c, semilattice_inf.le_trans a.val b.val c.val,
    le_antisymm := λ a b,
    begin
      convert semilattice_inf.le_antisymm a.val b.val,
      convert rfl,
      apply propext,
      split,
        intros h1 h2 h3,
        apply subtype.eq,
        apply h1 h2 h3,
      intros h1 h2 h3,
      rw h1 h2 h3,
    end,
    inf_le_right --: ∀ a b : α, a ⊓ b ≤ b
      := λ a b, semilattice_inf.inf_le_right a.val b.val,--sorry,
    le_inf := λ a b c, semilattice_inf.le_inf a.val b.val c.val,
  }

def presheaf_on_opens (U : α) := presheaf {V // V <= U}

structure morphism (F : presheaf_on_opens U) (G : presheaf_on_opens U) :=
(map : Π (V : {V // V ≤ U}), F.F V → G.F V)
(commutes : ∀ (V W : {V // V ≤ U}) (HWV : W ≤ V) (x),
  map W (F.res V W HWV x) = G.res V W HWV (map V x))

namespace morphism

definition commutes' (F : presheaf_on_opens U) (G : presheaf_on_opens U)
  (f : morphism U F G) :
∀ (V W : {V // V ≤ U}) (HWV : W ≤ V) (x : F.F V),
  f.map W ((F.res V W HWV) x) = G.res V W HWV ((f.map V) x)
:= begin intros V W HVW, funext x, apply f.commutes end

def commutes'' (F : presheaf_on_opens U) (G : presheaf_on_opens U)
  (f : morphism U F G) :
∀ (V W : {V // V ≤ U}) (HWV : W ≤ V),
  f.map W ∘ (F.res V W HWV) = G.res V W HWV ∘ (f.map V)
:= begin intros V W HVW, funext x, apply f.commutes end

protected def id (F : presheaf_on_opens U) : morphism U F F :=
{ map := λ V, id,
  commutes := λ V W HWV, by intros; refl}


def comp {F : presheaf_on_opens U} {G : presheaf_on_opens U}
  {H : presheaf_on_opens U}
  (η : morphism U G H) (ξ : morphism U F G) : morphism U F H :=
{ map := λ V x, η.map V (ξ.map V x),
  commutes := λ V W HWV, begin
    intro x,
  rw morphism.commutes' U F G ξ,
  rw morphism.commutes' U G H η,
  end}


@[extensionality] lemma ext {F : presheaf_on_opens U} {G : presheaf_on_opens U}
  {η ξ : morphism U F G}
  (H : ∀ V x, η.map V x = ξ.map V x) : η = ξ :=
by cases η; cases ξ; congr; ext; apply H


@[simp] lemma id_comp {F : presheaf_on_opens U} {G : presheaf_on_opens U}
  (η : morphism U F G) :
  comp U (morphism.id U G) η = η :=
begin
  ext x,
  refl,
end

@[simp] lemma comp_id {F : presheaf_on_opens U} {G : presheaf_on_opens U} (η : morphism U F G) :
  comp U η (morphism.id U F) = η :=
begin
  ext x,
  refl,
end

@[simp] lemma comp_assoc {F : presheaf_on_opens U} {G : presheaf_on_opens U}
  {H : presheaf_on_opens U} {I : presheaf_on_opens U}
  (η : morphism U H I) (ξ : morphism U G H) (χ : morphism U F G) :
  comp U (comp U η ξ) χ = comp U η (comp U ξ χ) :=
rfl

end morphism

structure equiv (F : presheaf_on_opens U) (G : presheaf_on_opens U) :=
(to_fun : morphism U F G)
(inv_fun : morphism U G F)
(left_inv : morphism.comp U inv_fun to_fun = morphism.id U F)
(right_inv : morphism.comp U to_fun inv_fun = morphism.id U G)

#exit

def universal_property (I : Type*) (S : I → α) (F : Π (i : I), presheaf_on_opens (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) (set.inter_subset_left _ _)) ((F j).res_subset ((S i) ∩ (S j)) (set.inter_subset_right _ _)))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.inter_subset_left _ _)).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_right _ _)) (set.inter_subset_right _ _))) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (set.subset_inter (le_trans (set.inter_subset_left _ _) (set.inter_subset_left _ _)) (set.inter_subset_right _ _))) :
∀ i : I, equiv (res_subset (glue S F φ Hφ1 Hφ2) (S i) $ opens.subset_Union S i) (F i) := sorry


end semilattice_inf.opens

That's the equiv in Mario's non-category language, using Kenny's trick. Now I can start to formalise the universal property for glueing.

[Kevin Buzzard]

This is with def presheaf_on_opens (U : α) := presheaf {V // V <= U}

[Mario Carneiro]

Why do you have a proof of partial_order and then not use it for semilattice_inf?

[Kevin Buzzard]

Because I don't know what I'm doing.

[Kevin Buzzard]

I'm behaving quite algorithmically still, I'm not thinking much.

[Mario Carneiro]

I think that if you leave off the fields they get inferred automatically

[Kevin Buzzard]

I was having trouble getting this to work.

[Kevin Buzzard]

Which lines do you think I can delete?

[Mario Carneiro]

if not, you can use ..(by apply_instance : partial_order {V // V ≤ U}) at the end

[Mario Carneiro]

the ones associated to partial_order, so le, le_trans, le_antisymm etc

[Mario Carneiro]

you can do the same thing with has_inf, although that doesn't save a whole lot

[Kevin Buzzard]

Here's the current state of my work:

https://github.com/kbuzzard/xena/blob/master/Examples/mario_glueing.lean

I just can't get the deleting to work. I don't understand structure field inheritence well enough and I can never remember the tricks; there are a couple of cool idioms which I'm sure will help me.

[Mario Carneiro]

import order.lattice
universes u v
open lattice

instance {α : Type u} [semilattice_inf α] (U : α) :
  semilattice_inf {V // V ≤ U} :=
{ inf_le_left := λ a b, inf_le_left,
  inf := λ a b, ⟨a.1 ⊓ b.1, le_trans inf_le_left a.2⟩,
  inf_le_right := λ a b, inf_le_right,
  le_inf := λ a b c, le_inf,
  ..subtype.partial_order _ }

[Kevin Buzzard]

Thanks.

[Reid Barton]

Anyway, that's got nothing to do with what I'm doing, what I'm doing is wondering whether the natural domain for glueing sheaves of types is complete lattices.

Probably it is frames, though as noted there a frame is also a complete lattice. I see you two already have something called semilattice_inf_lub_emb, which is an embedding that's a frame homomorphism.
Also see "Relation to topological spaces", and Definition 4.9 and following.

[Kevin Buzzard]

Do we have frames in mathlib?

[Kenny Lau]

can we glue sheaves on sites?

[Kevin Buzzard]

We can't glue anything on anything right now

[Kevin Buzzard]

But in maths land I should think you can glue sheaves on sites.

[Kevin Buzzard]

Even type-v-indexed sheaves, I should think.

[Mario Carneiro]

Maybe it might help to actually try using this thing rather than working so much to state an axiom

[Mario Carneiro]

I still have no idea if this is the best way to glue things when we have choice

[Jesse Michael Han]

Do we have frames in mathlib?

no, but they would be easy to define

a caveat: complete_lattice bundles together Sup and Inf, and complete_distrib_lattice bundles together distributivity of sup over Inf and inf over Sup, so we might have to refine the hierarchy before implementing frames

[Kevin Buzzard]

So I've done a bunch of Kenny's API, but stopped just short of defining the glued sheaf.

https://github.com/kbuzzard/xena/blob/b4994ccfa949a1586e9119ce8fefdd2b656647f9/Examples/mario_glueing.lean#L197

@Mario Carneiro I didn't use res' at all. How should I have done this better?

[Mario Carneiro]

if there is a nontrivial proof in a statement, the answer is yes

[Kenny Lau]

namespace opens

variables {X : Type u} [topological_space X] {U V W S T : opens X}

theorem subset.refl : U ⊆ U := set.subset.refl U
theorem subset.trans : U ⊆ V → V ⊆ W → U ⊆ W := set.subset.trans
theorem inter_subset_left : U ∩ V ⊆ U := set.inter_subset_left U.1 V.1
theorem inter_subset_right : U ∩ V ⊆ V := set.inter_subset_right U.1 V.1
theorem subset_inter : U ⊆ V → U ⊆ W → U ⊆ V ∩ W := set.subset_inter
theorem inter_subset_inter_left : U ⊆ V → U ∩ W ⊆ V ∩ W := set.inter_subset_inter_left W.1
theorem inter_subset_inter_right : V ⊆ W → U ∩ V ⊆ U ∩ W := set.inter_subset_inter_right U.1
theorem inter_subset_inter : U ⊆ V → S ⊆ T → U ∩ S ⊆ V ∩ T := set.inter_subset_inter

end opens

def glue {I : Type u} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ∩ (S j)) opens.inter_subset_left) ((F j).res_subset ((S i) ∩ (S j)) opens.inter_subset_right))
  (Hφ1 : ∀ i, φ i i = equiv.refl (res_subset (F i) (S i ∩ S i) _))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ∩ (S j) ∩ (S k)) opens.inter_subset_left).trans
      ((φ j k).res_subset ((S i) ∩ (S j) ∩ (S k)) (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_right) opens.inter_subset_right)) =
    (φ i k).res_subset ((S i) ∩ (S j) ∩ (S k)) (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_left) opens.inter_subset_right)) :
  sheaf_on_opens.{max u v} X (opens.Union S) :=
{ F :=
  { F := λ W, { f : Π i, (F i).eval ((S i) ∩ W) opens.inter_subset_left //
      ∀ i j, (φ i j).1.map ((S i) ∩ (S j) ∩ W) opens.inter_subset_left
        ((F i).res ((S i) ∩ W) _ _ (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
          (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_left) opens.inter_subset_right)
          (f i)) =
        (F j).res ((S j) ∩ W) _ _ (opens.subset.trans opens.inter_subset_left opens.inter_subset_right)
          (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_right) opens.inter_subset_right)
          (f j) },
    res := λ U V HVU f, ⟨λ i, (F i).res (S i ∩ U) _ (S i ∩ V) _ (opens.inter_subset_inter_right HVU) (f.val i), λ i j,
      calc  (φ i j).1.map (S i ∩ S j ∩ V) opens.inter_subset_left
              (res (F i) (S i ∩ V) opens.inter_subset_left (S i ∩ S j ∩ V)
                (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                    opens.inter_subset_right)
                (res (F i) (S i ∩ U) opens.inter_subset_left (S i ∩ V) opens.inter_subset_left
                    (opens.inter_subset_inter_right HVU)
                    (f.val i)) : (F i).eval (S i ∩ S j ∩ V) (opens.subset.trans _ _))
          = (φ i j).1.map (S i ∩ S j ∩ V) opens.inter_subset_left
              (res (res_subset (F i) (S i ∩ S j) opens.inter_subset_left) (S i ∩ S j ∩ U) opens.inter_subset_left
                (S i ∩ S j ∩ V)
                opens.inter_subset_left
                (opens.inter_subset_inter_right HVU)
                (res (F i) (S i ∩ U) opens.inter_subset_left (S i ∩ S j ∩ U)
                  (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                  (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                      opens.inter_subset_right)
                  (f.val i) : (F i).eval (S i ∩ S j ∩ U) (opens.subset.trans opens.inter_subset_left opens.inter_subset_left))) :
        by rw [res_res_subset, res_res, res_res]
      ... = res (res_subset (F j) (S i ∩ S j) _) (S i ∩ S j ∩ U) _ (S i ∩ S j ∩ V) _ (opens.inter_subset_inter_right HVU)
              ((φ i j).1.map (S i ∩ S j ∩ U) opens.inter_subset_left
                (res (F i) (S i ∩ U) opens.inter_subset_left (S i ∩ S j ∩ U)
                  (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                  (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_left)
                      opens.inter_subset_right)
                  (f.val i) : (F i).eval (S i ∩ S j ∩ U) (opens.subset.trans opens.inter_subset_left opens.inter_subset_left))) :
        (φ i j).1.commutes (S i ∩ S j ∩ U) _ (S i ∩ S j ∩ V) _ _ _
      ... = (res (F j) (S j ∩ V) opens.inter_subset_left (S i ∩ S j ∩ V)
              (opens.subset.trans opens.inter_subset_left opens.inter_subset_right)
              (opens.subset_inter (opens.subset.trans opens.inter_subset_left opens.inter_subset_right)
                opens.inter_subset_right)
              (res (F j) (S j ∩ U) opens.inter_subset_left (S j ∩ V) opens.inter_subset_left
                (opens.inter_subset_inter_right HVU)
                (f.val j)) : (F j).eval (S i ∩ S j ∩ V) _) :
        by rw [f.2 i j, res_res_subset, res_res, res_res]⟩,
    Hid := sorry,
    Hcomp := sorry },
  locality := sorry,
  gluing := sorry }

[Kenny Lau]

I have |no idea| what I was doing

[Kenny Lau]

I should extract defs/lemmas

[Johan Commelin]

Why are you using the \cap and \cup notation? Isn't it a lot easier to use the lattice notation? Saves you all those little lemmas at the top as well.

[Kevin Buzzard]

Kenny I refactored your code so that it works for complete lattices

[Kevin Buzzard]

That's quite some calc by the way!

[Patrick Massot]

I didn't read code in this thread, but I just want to tell Kevin: Johannes explained countless times why there are lattices all other mathlib. This is category theory that actually works and helps. Up to now nobody managed to make category theory usable in Lean. In Edinburgh I asked Scott and Reid to show me how to define the category of uniform spaces, the subcategory of complete separated uniform spaces, and the completion functor (all of this is already in mathlib, unbundled and without using category theory). They couldn't. Defining categories was ok, but then they hit the weirdest kinds of bugs, with Lean randomly unfolding things beyond recognition.

Also when I changed the order on topological_space and uniform_space last week, I had to change 16 files. After setting up the change correctly in the first file it was a smooth ride all along except for topology/Top/limits.lean which got me amazingly confused, because the statements and intermediate goals were undecipherable to me.

Now there is one kind of category that works in Lean: posets. Setting up is easy, functor work (monotone maps) adjunctions work (the Galois connection thing), limits and colimits work (infi and supr). And many many lemmas in topology are really proven in a categorical way using this trick. If you think complete lattices is computer science (as I also did before Johannes explained it) then category theory is computer science.

[Kevin Buzzard]

category theory is computer science. I think that too, kind of.

[Kevin Buzzard]

So categories with general type-valued homs are hard to work with in dependent type theory, because the morphism isn't actually a function, so we lose some powerful flexibility. Types and morphisms between them (the category Type) are fine though because these are pi-type-valued homs. Patrick is saying that terms and Prop-valued homs are also a good fit for dependent type theory.

[Kevin Buzzard]

It's all beginning to make some sense to me. But in some sense this should just be an interface issue, right?

[Johan Commelin]

@Patrick Massot I'm sad to hear that story

[Kevin Buzzard]

I don't know how much is interface and how much is "Lean could do better".

[Mario Carneiro]

This is kind of why I was against moving Scott's category library into mathlib to start with. I think it's improved a lot since then, but it still is sorely lacking in applications

[Kevin Buzzard]

Every time we try something it's kind of "oh well, probably it can be made to work, but let's just do it the easy way because that's all we need".

[Mario Carneiro]

All the work thus far has been to write things as categories, but all the sharing goes one way only. We need to figure out how to prove something that does not directly use categories via category theory

[Kevin Buzzard]

For etale cohomology I am unclear about how much we can get away with.

[Mario Carneiro]

Notice that orders and lattices are at the very bottom of the mathlib dependency structure

[Mario Carneiro]

I think there is a good argument that once you start dealing with 2-categorical notions you should probably use category theory to organize stuff

[Kevin Buzzard]

The moment homs are not Props, basically.

[Mario Carneiro]

right

[Mario Carneiro]

Your glue and universal_property theorems look like that

[Mario Carneiro]

so I'm hoping that we can maybe use this as a case study for practical use of category theory

[Mario Carneiro]

Yes, we can do it without category theory, but the current solutions look pretty scary. Let's see what the alternative is

[Mario Carneiro]

try it both ways and let the best infrastructure win

[Scott Morrison]

I didn't read code in this thread, but I just want to tell Kevin: Johannes explained countless times why there are lattices all other mathlib. This is category theory that actually works and helps. Up to now nobody managed to make category theory usable in Lean. In Edinburgh I asked Scott and Reid to show me how to define the category of uniform spaces, the subcategory of complete separated uniform spaces, and the completion functor (all of this is already in mathlib, unbundled and without using category theory). They couldn't. Defining categories was ok, but then they hit the weirdest kinds of bugs, with Lean randomly unfolding things beyond recognition.

I'm pretty surprised by this characterisation. My memory was rather than we stopped defining the adjunction def adj : completion_functor ⊣ forget_to_UniformSpace because we realised there was a lemma about completions that hadn't been proved yet. I haven't looked at this since that afternoon in Edinburgh, but the branch category-of-uniform-spaces seems to have what we did then, with a single sorry at that point.

[Scott Morrison]

I do remember some problem with Lean being over eager about unfolding. Unfortunately I can't see it still there.

[Scott Morrison]

The file we wrote that afternoon is here.

[Kevin Buzzard]

Patrick can be a bit cynical at times :-) But the point remains. The last time I talked to you about sheaves you said "we've got presheaves, I just need to figure out a neat way of doing the sheaf condition which is not ugly". But in this low-level approach here we just write stuff down and it works. There's a trick to finding out a good way to write it down, but once you have a good working basic set of definitions it's really good fun to build an API and then "prove some lemmas" (like the "lemma" that you can glue sheaves, which I would say to CS people was a definition, but I would call it a theorem to maths people) and watch the API become robust. I guess the theorem is that a universal object exists.

I am still unclear about whether the problem is having Hom(X,Y) = inductive type, or whether the problem is that Lean 3 is not very good at categories because of design decisions which we're having to fight against.

I mentioned issues with categories to Tom Hales at AITP and he said "well as far as I know Coq doesn't have any issues with them, I believe they have a nice category theory library" (I'm paraphrasing but that's my memory of what he said). Is this true? Can they do things better than us here? Where is this library? There is all this talk of not knowing how best to implement diagrams -- how do they do it in Coq?

[Kevin Buzzard]

This deserves a new thread really.

[Mario Carneiro]

I don't think there are any fundamental issues with using categories any more than any other branch of maths

[Mario Carneiro]

I think people just aren't doing it, because you and I prefer to work without them and Scott and Reid prefer to work on categories as the endpoint

[Mario Carneiro]

stuff like proving that uniform spaces form a category is utterly uninteresting to me. Of course you can do it. It gets interesting when you prove something that's not a triviality in an area that's not category theory using this gigantic library that's being developed. If you can't do that then it just looks like a bridge to nowhere from my point of view

[Kevin Buzzard]

Categories lead to questions about universes which are not there in other branches of maths (at least when maths is done by mathematicians), and one question is how well Lean solves those issues.

@Scott Morrison @Reid Barton how would glueing presheaves on open subsets look in the category theory library? Already it was causing us problems down in the land where the objects were terms and the morphisms were in Prop, but we have this workaround now (analogous to what they did in the odd order repo when they worked with subgroups of a big ambient group because it was more convenient). I find this approach rather distasteful in some sense, but then again these CS people seem to prefer computational efficiency to the abstract approach.

[Kevin Buzzard]

Kenny's code above

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/breaking.20equality.20with.20sheaves/near/168794153

is the definition of a glued presheaf, but he has not proved the universal property. @Kenny Lau Can you formulate the universal property for a glued presheaf? That's what we have right now.

[Kevin Buzzard]

oh -- it is probably exactly the same as the universal property for a glued sheaf isn't it.

[Kevin Buzzard]

Then we will have proved a theorem about glued presheaves, namely that there exists an object having the universal property for glued presheaves. This has turned out to be a great test of various foundational set-ups.

[Kevin Buzzard]

People didn't see the nightmares I had because in the main I didn't post them. But I did hint about having to interpret U intersect V as an object of opens U, opens V, opens U intersect V and opens X. With the Kenny/Mario approach there is only one U intersect V. Can this trick be pulled off in the category theory set-up?

[Reid Barton]

Just regarding the subject of using category theory. https://github.com/rwbarton/lean-homotopy-theory is over 8000 lines and almost all of it is built on top of category theory: either to do homotopy theory in a general category (with additional structure) or to prove things about Top which are hard to even state without category theory (for example, the pushout of a closed embedding is a closed embedding). For context, it is larger than the amount of category theory in mathlib.

[Kevin Buzzard]

Do you have any of presheaves, sheaves, glueing sheaves, sheafification? Or do you not need sheaves at all for this stuff?

[Mario Carneiro]

You know how Kevin says everything is CS? That still sounds like category theory to me

[Reid Barton]

Do you have any of presheaves, sheaves, glueing sheaves, sheafification? Or do you not need sheaves at all for this stuff?

No, these didn't come up in what I was doing

[Reid Barton]

You know how Kevin says everything is CS? That still sounds like category theory to me

This is kind of like saying algebraic geometry is not math but rather French, because EGA is written in French

[Reid Barton]

Using the language of category theory to study subject X doesn't make subject X into category theory

[Reid Barton]

And maybe it's particularly convenient to apply category theory to algebraic topology (considering that category theory was invented for the purpose of algebraic topology in the first place) but in any case it can be done.

[Scott Morrison]

Scott and Reid prefer to work on categories as the endpoint

I don't think this is true at all, and to tell the truth I'm a bit annoyed at this. I worked on an API for limits because it seemed essential for ever doing the basics of sheaf theory, or the basics of homological algebra, or the basics of algebraic topology, without endlessly repeating yourself in slight variations. None of these are subjects that I'm particularly interested in directly, but I was trying to be helpful, because it seemed there was interest in those directions.

It's true that my "day job" research is about things like modular tensor categories. But it is a pretty bad error to think that these things are "part of category theory" in the sense of boring 20th category theory that exists in mathlib at the moment and that we are discussing here. Modular tensor categories are mathematical objects more like ... I don't know schemes or something. Everyone will use category theoretic language to describe the axioms, but at the end of the day they are actually pretty alien to "category theory". They are completely finitary objects (finitely much algebraic data, over a number field), and to study them you use combinatorics and topology and representation theory and little bits of number theory: far from the abstract nonsense!

[Scott Morrison]

Regarding the category of uniform spaces, @Mario Carneiro, @Patrick Massot, I agree that's completely boring. We did it because Patrick asked to see how it was done. I agree it was annoying that afternoon that we ran into some still-mysterious Lean 'feature' involving unwanted unfolding. But besides that I thought that exercise was mostly a success. Reid and I got distracted at the end of the discussion trying to work out how to use reflective subcategories, but the file at the end was what Patrick had asked for, modulo one sorry (that was actually about uniform spaces).

[Mario Carneiro]

Fair enough. I would hope that these applications are not some giant years-from-now endpoint though; you should be able to give some near term applications as well. Without applications it's far too easy to build things the wrong way and not realize it's useless until you actually get to that application at the end of the road

[Mario Carneiro]

But I think you won't be surprised that I can't tell the difference between "modular tensor categories" and "category theory" :P

[Scott Morrison]

Regarding sheaf-y stuff. I think a great test case is whether the stuff you're building works for sheaves of topological rings. This is not some esoteric corner case: people have to think about these constantly. And they are a great example where you can't just spend all your time thinking about the underlying sheaf of types, because that's not enough! (There are presheaves of topological rings, whose underlying presheaf of types satisfies the sheaf condition, but does not itself.) I'm worried that if you don't attempt to do this at the correct level of generality, then there's going to be endless repetition (sheaves of types, sheaves of rings, sheaves of topological spaces, sheaves of topological rings), and you'll find yourself having to talk about gluing separately and with slight variations in all the cases, and it will turn into a nightmare. But this isn't my subject, so perhaps I'm mistaking the fact that every source for this stuff uses category theoretic language to describe the sheaf condition for necessity.... :-)

[Reid Barton]

I still worry a bit that I don't know a math definition which encompasses both this example of sheaves of topological rings (on a topological space or whatever) and also sheaves on a general site.

[Reid Barton]

But I think you won't be surprised that I can't tell the difference between "modular tensor categories" and "category theory" :P

Next you'll be telling me you can't tell the difference between "model categories" and "category theory", sheesh!

[Kevin Buzzard]

Unfortunately I'm just as ignorant here. I've only ever had to use the most basic notions of category theory in my day job (representable functors). What's the problem with sheaves of topological rings on a site?

[Johan Commelin]

That a continuous bijection doesn't need to be a homeomorphism

[Johan Commelin]

So you can't ask for some equilizer to be an iso in Type. It really has to be an iso in Top or TopRing.

[Kevin Buzzard]

I understand that -- my question is what is the problem with sheaves of (insert category here) on a site?

[Johan Commelin]

I guess there is not that much of a problem, but it means yet another variable in the API.

[Kevin Buzzard]

Another universe variable? Is that the issue? Why don't we just put everything in the same universe like in normal maths?

[Scott Morrison]

No, no universe variables. :-)

[Scott Morrison]

Johan just meant that it's literally an extra variable to the definition of a sheaf: you have to specify the category the sections live in.

[Scott Morrison]

and you need to ask that the sheaf condition diagram is an equalizer in that category, rather than doing something elementwise.

[Kevin Buzzard]

I feel like I am always specifying this variable in practice. It was like when the CS people were going "oh noes, you're going to have to say which ring this is a module over" and I was just thinking "that's OK, I know which ring it's a module over"

[Scott Morrison]

or, alternatively, for every different target category you need to write a different version of the sheaf condition, which includes an extra field effectively spelling out: this bijection of the underlying types is actually an isomorphism.

[Scott Morrison]

I'd assumed way back that everyone would be unhappy with writing out different versions of the sheaf condition for different target categories. (Because then you have to repeat and reprove theorems about sheaves in different target categories.)

[Kevin Buzzard]

I defined a scheme, and that part was pretty easy. But proving that anything at all was a scheme involved some serious messing around with sheaves (and in particular proving that some explicit presheaf satisfied the sheaf axiom). We now have perfectoid spaces, but proving that anything at all is a perfectoid space will be just the same, except that we will have to prove that something is a sheaf of topological rings. So it's on the horizon.

[Kevin Buzzard]

this bijection of the underlying types is actually an isomorphism.

Yes, I remember you pointing this out when I was moaning about 10 different notations for "I am an equiv of this kind of structure"

[Scott Morrison]

That one is easy to fix. :-)

[Scott Morrison]

(As long as you're willing to work in a fixed universe, but I don't think that will be a problem for you. :-)

[Kenny Lau]

namespace sheaf_glue

variables {I : Type u} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
variables (φ : Π (i j : I), equiv ((F i).res_subset ((S i) ⊓ (S j)) inf_le_left) ((F j).res_subset ((S i) ⊓ (S j)) inf_le_right))
variables (Hφ1 : ∀ i, φ i i = equiv.refl (res_subset (F i) (S i ⊓ S i) _))
variables (Hφ2 : ∀ i j k,
  ((φ i j).res_subset ((S i) ⊓ (S j) ⊓ (S k)) inf_le_left).trans
    ((φ j k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_right) inf_le_right)) =
  (φ i k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_left) inf_le_right))

@[reducible] def compat (W : opens X) : Type (max u v) :=
{ f : Π i, (F i).eval ((S i) ⊓ W) inf_le_left //
  ∀ i j, (φ i j).1.map ((S i) ⊓ (S j) ⊓ W) inf_le_left
    ((F i).res ((S i) ⊓ W) _ _ (le_trans inf_le_left inf_le_left)
      (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)
      (f i)) =
    (F j).res ((S j) ⊓ W) _ _ (le_trans inf_le_left inf_le_right)
      (le_inf (le_trans inf_le_left inf_le_right) inf_le_right)
      (f j) }

def res (U V : opens X) (HVU : V ≤ U) (f : compat S F φ U) : compat S F φ V :=
⟨λ i, (F i).res (S i ⊓ U) _ (S i ⊓ V) _ (inf_le_inf (le_refl _) HVU) (f.1 i), λ i j,
calc  (φ i j).1.map (S i ⊓ S j ⊓ V) inf_le_left
        (res (F i) (S i ⊓ V) inf_le_left (S i ⊓ S j ⊓ V)
          (le_trans inf_le_left inf_le_left)
          (le_inf (le_trans inf_le_left inf_le_left)
              inf_le_right)
          (res (F i) (S i ⊓ U) inf_le_left (S i ⊓ V) inf_le_left
              (inf_le_inf (le_refl _) HVU)
              (f.1 i)) : (F i).eval (S i ⊓ S j ⊓ V) (le_trans _ _))
    = (φ i j).1.map (S i ⊓ S j ⊓ V) inf_le_left
        (res (res_subset (F i) (S i ⊓ S j) inf_le_left) (S i ⊓ S j ⊓ U) inf_le_left
          (S i ⊓ S j ⊓ V)
          inf_le_left
          (inf_le_inf (le_refl _) HVU)
          (res (F i) (S i ⊓ U) inf_le_left (S i ⊓ S j ⊓ U)
            (le_trans inf_le_left inf_le_left)
            (le_inf (le_trans inf_le_left inf_le_left)
                inf_le_right)
            (f.1 i) : (F i).eval (S i ⊓ S j ⊓ U) (le_trans inf_le_left inf_le_left))) :
  by rw [res_res_subset, res_res, res_res]
... = (res (F j) (S j ⊓ V) inf_le_left (S i ⊓ S j ⊓ V)
        (le_trans inf_le_left inf_le_right)
        (le_inf (le_trans inf_le_left inf_le_right)
          inf_le_right)
        (res (F j) (S j ⊓ U) inf_le_left (S j ⊓ V) inf_le_left
          (inf_le_inf (le_refl _) HVU)
          (f.1 j)) : (F j).eval (S i ⊓ S j ⊓ V) _) :
  by rw [(φ i j).1.commutes, f.2 i j, res_res_subset, res_res, res_res]⟩

theorem locality (U : opens X) (OC : covering U) (s t : sheaf_glue.compat S F φ U)
  (H : ∀ i : OC.γ, sheaf_glue.res S F φ U (OC.Uis i) (subset_covering i) s =
    sheaf_glue.res S F φ U (OC.Uis i) (subset_covering i) t) :
  s = t :=
subtype.eq $ funext $ λ i, (F i).locality _ _ _ _ (opens.covering_inf_left U (S i) OC) $ λ j,
by have := H j; simp only [sheaf_glue.res, subtype.mk.inj_eq] at this; exact congr_fun this i

noncomputable def gluing.aux1 (U : opens X) (OC : covering U) (s : Π i : OC.γ, sheaf_glue.compat S F φ (OC.Uis i))
  (H : ∀ i j : OC.γ, sheaf_glue.res S F φ _ _ inf_le_left (s i) = sheaf_glue.res S F φ _ _ inf_le_right (s j))
  (i : I) : (F i).eval (S i ⊓ U) inf_le_left :=
(F i).glue _ _ (opens.covering_inf_left U (S i) OC) (λ j, (s j).1 i) $ λ j k,
have h1 : S i ⊓ OC.Uis j ⊓ (S i ⊓ OC.Uis k) ≤ S i ⊓ (OC.Uis j ⊓ OC.Uis k),
by rw [inf_assoc, inf_left_comm (OC.Uis j), ← inf_assoc, inf_idem]; exact le_refl _,
have h2 : S i ⊓ (OC.Uis j ⊓ OC.Uis k) ≤ S i ⊓ OC.Uis j,
from inf_le_inf (le_refl _) inf_le_left,
have h3 : S i ⊓ (OC.Uis j ⊓ OC.Uis k) ≤ S i ⊓ OC.Uis k,
from inf_le_inf (le_refl _) inf_le_right,
have (F i).res (S i ⊓ OC.Uis j) _ (S i ⊓ (OC.Uis j ⊓ OC.Uis k)) inf_le_left h2 ((s j).1 i) =
  (F i).res (S i ⊓ OC.Uis k) _ (S i ⊓ (OC.Uis j ⊓ OC.Uis k)) inf_le_left h3 ((s k).1 i),
from congr_fun (congr_arg subtype.val (H j k)) i,
calc  _
    = (F i).res (S i ⊓ OC.Uis j) _ ((S i ⊓ OC.Uis j) ⊓ (S i ⊓ OC.Uis k)) _ _ ((s j).1 i) : rfl
... = (F i).res (S i ⊓ (OC.Uis j ⊓ OC.Uis k)) _ ((S i ⊓ OC.Uis j) ⊓ (S i ⊓ OC.Uis k)) _ h1
        ((F i).res (S i ⊓ OC.Uis j) _ (S i ⊓ (OC.Uis j ⊓ OC.Uis k)) inf_le_left h2 ((s j).1 i)) : (res_res _ _ _ _ _ _ _ _ _ _).symm
... = (F i).res (S i ⊓ OC.Uis k) _ ((S i ⊓ OC.Uis j) ⊓ (S i ⊓ OC.Uis k)) _ inf_le_right ((s k).1 i) : by rw [this, res_res]

theorem gluing.aux2 (U : opens X) (OC : covering U) (s : Π i : OC.γ, sheaf_glue.compat S F φ (OC.Uis i))
  (H : ∀ i j : OC.γ, sheaf_glue.res S F φ _ _ inf_le_left (s i) = sheaf_glue.res S F φ _ _ inf_le_right (s j)) (i j : I) :
  (φ i j).1.map (S i ⊓ S j ⊓ U) inf_le_left
      ((F i).res (S i ⊓ U) _ (S i ⊓ S j ⊓ U) (le_trans inf_le_left inf_le_left)
        (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)
        (gluing.aux1 S F φ U OC s H i)) =
    (F j).res (S j ⊓ U) _ (S i ⊓ S j ⊓ U) (le_trans inf_le_left inf_le_right)
      (by rw inf_assoc; exact inf_le_right)
      (gluing.aux1 S F φ U OC s H j) :=
(F j).locality _ _ _ _ (opens.covering_inf_left _ _ OC) $ λ k,
calc  ((F j).res_subset (S i ⊓ S j) inf_le_right).res (S i ⊓ S j ⊓ U) inf_le_left ((S i ⊓ S j) ⊓ OC.Uis k) inf_le_left
        (inf_le_inf (le_refl _) (subset_covering k))
        ((φ i j).1.map (S i ⊓ S j ⊓ U) inf_le_left
          ((F i).res (S i ⊓ U) _ (S i ⊓ S j ⊓ U) _
            (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)
            (gluing.aux1 S F φ U OC s H i)))
    = (φ i j).1.map (S i ⊓ S j ⊓ OC.Uis k) inf_le_left
        ((F i).res ((opens.covering_inf_left U (S i) OC).Uis k) _ _ (le_trans inf_le_left inf_le_left)
          (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)
          ((F i).res (S i ⊓ U) _ ((opens.covering_inf_left U (S i) OC).Uis k) inf_le_left
            (inf_le_inf (le_refl _) (subset_covering k))
            (gluing.aux1 S F φ U OC s H i))) : by rw [← (φ i j).1.commutes, res_res_subset, res_res, res_res]
... = (F j).res ((opens.covering_inf_left U (S j) OC).Uis k) _ ((S i ⊓ S j) ⊓ OC.Uis k) _
        (by rw inf_assoc; exact inf_le_right)
        ((F j).res (S j ⊓ U) _ ((opens.covering_inf_left U (S j) OC).Uis k) inf_le_left
          (inf_le_inf (le_refl _) (subset_covering k))
          (gluing.aux1 S F φ U OC s H j)) : by erw [res_glue, res_glue]; exact (s k).2 i j
... = (F j).res (S i ⊓ S j ⊓ U) _ ((S i ⊓ S j) ⊓ OC.Uis k) _ _
        ((F j).res (S j ⊓ U) _ (S i ⊓ S j ⊓ U) _ _ (gluing.aux1 S F φ U OC s H j)) : by rw [res_res, res_res]; refl

theorem gluing.aux3 (U : opens X) (OC : covering U) (s : Π i : OC.γ, sheaf_glue.compat S F φ (OC.Uis i))
  (H : ∀ i j : OC.γ, sheaf_glue.res S F φ _ _ inf_le_left (s i) = sheaf_glue.res S F φ _ _ inf_le_right (s j)) (i : OC.γ) :
  sheaf_glue.res S F φ U (OC.Uis i) (subset_covering i) ⟨λ i, gluing.aux1 S F φ U OC s H i, gluing.aux2 S F φ U OC s H⟩ = s i :=
subtype.eq $ funext $ λ j, by dsimp only [gluing.aux1, sheaf_glue.res];
change (F j).res _ _ ((opens.covering_inf_left U (S j) OC).Uis i) _ _ _ = _;
erw res_glue

theorem gluing (U : opens X) (OC : covering U) (s : Π i : OC.γ, sheaf_glue.compat S F φ (OC.Uis i))
  (H : ∀ i j : OC.γ, sheaf_glue.res S F φ _ _ inf_le_left (s i) = sheaf_glue.res S F φ _ _ inf_le_right (s j)) :
  ∃ t : sheaf_glue.compat S F φ U, ∀ i : OC.γ, sheaf_glue.res S F φ U (OC.Uis i) (subset_covering i) t = s i :=
⟨⟨λ i, gluing.aux1 S F φ U OC s H i, gluing.aux2 S F φ U OC s H⟩, λ i, gluing.aux3 S F φ U OC s H i⟩

end sheaf_glue

def sheaf_glue {I : Type u} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π (i j : I),
    equiv ((F i).res_subset ((S i) ⊓ (S j)) inf_le_left) ((F j).res_subset ((S i) ⊓ (S j)) inf_le_right))
  (Hφ1 : ∀ i, φ i i = equiv.refl (res_subset (F i) (S i ⊓ S i) _))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ⊓ (S j) ⊓ (S k)) inf_le_left).trans
      ((φ j k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_right) inf_le_right)) =
    (φ i k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)) :
  sheaf_on_opens.{max u v} X (opens.Union S) :=
{ F :=
  { F := sheaf_glue.compat S F φ,
    res := sheaf_glue.res S F φ,
    Hid := λ U, funext $ λ f, subtype.eq $ funext $ λ i, by dsimp only [sheaf_glue.res, id]; rw res_self,
    Hcomp := λ U V W HWV HVU, funext $ λ f, subtype.eq $ funext $ λ i, by symmetry; apply res_res; exact inf_le_left },
  locality := sheaf_glue.locality S F φ,
  gluing := sheaf_glue.gluing S F φ }

[Kenny Lau]

and I never used the cocycle conditions

[Kevin Buzzard]

Maybe you need them to prove the universal property?

[Kevin Buzzard]

This is not proved even for presheaves.

[Kevin Buzzard]

As far as I know, the universal property is simply the data of an isomorphism from the glued sheaf, restricted to an open subset S i, with the sheaf F i.

[Kenny Lau]

that is indeed what you gave me

[Kevin Buzzard]

I guess an isomorphism of sheaves is an isomorphism of presheaves. Maybe you need it for one of the maps. To write down from F i (S i) to the product over j of F j (S i \cap S j) you can use phi i j, but to prove that these sections are compatible will involve phi j k so that's where it will be.

[Kevin Buzzard]

To write down the map the other way I don't see how to do it without using the sheaf axiom.

[Kevin Buzzard]

So maybe the universal property isn't even true if you glue presheaves naively.

[Patrick Massot]

Regarding the category of uniform spaces, I agree that's completely boring. We did it because Patrick asked to see how it was done. I agree it was annoying that afternoon that we ran into some still-mysterious Lean 'feature' involving unwanted unfolding. But besides that I thought that exercise was mostly a success. Reid and I got distracted at the end of the discussion trying to work out how to use reflective subcategories, but the file at the end was what Patrick had asked for, modulo one sorry (that was actually about uniform spaces).

Scott, I'm sorry my message sounded more aggressive than I intended. But I still claim it doesn't work. I tried to include that file in current mathlib (latest nightly) and the definition of completion_functor doesn't work anymore. It seems that condition map_id' was filled in automatically in Edinburgh but isn't today. And I have no clue how I could try to prove it (although I'm sure it has no mathematical content). Same applies to one item of the adj definition. I guess a bit part of the issue is documentation of the API

[Patrick Massot]

And if you want to get back part of the unfolding craziness you can replace the last tactic block by an invocation of the structure skeketon hole command.

[Patrick Massot]

You'll see subtype uniform_continuous appearing everywhere

[Kenny Lau]

@[simp] lemma sheaf_glue_res_val {I : Type u} (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π i j, equiv ((F i).res_subset ((S i) ⊓ (S j)) inf_le_left) ((F j).res_subset ((S i) ⊓ (S j)) inf_le_right))
  (U HU V HV HVU s i) : ((sheaf_glue S F φ).res U HU V HV HVU s).1 i = (F i).res _ _ _ _ (inf_le_inf (le_refl _) HVU) (s.1 i) := rfl

def universal_property (I : Type u) (S : I → opens X) (F : Π (i : I), sheaf_on_opens.{v} X (S i))
  (φ : Π i j, equiv ((F i).res_subset ((S i) ⊓ (S j)) inf_le_left) ((F j).res_subset ((S i) ⊓ (S j)) inf_le_right))
  (Hφ1 : ∀ i, φ i i = equiv.refl (F i))
  (Hφ2 : ∀ i j k,
    ((φ i j).res_subset ((S i) ⊓ (S j) ⊓ (S k)) inf_le_left).trans
      ((φ j k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_right) inf_le_right)) =
    (φ i k).res_subset ((S i) ⊓ (S j) ⊓ (S k)) (le_inf (le_trans inf_le_left inf_le_left) inf_le_right))
  (i : I) :
  equiv (res_subset (sheaf_glue S F φ) (S i) $ opens.subset_Union S i) (F i) :=
{ to_fun :=
  { map := λ U H s, (F i).res _ _ _ _ (le_inf H (le_refl _)) (s.1 i),
    commutes := λ U HU V HV HVU s, by rw [res_res, res_res_subset]; dsimp only [res, sheaf_glue, sheaf_glue.res]; rw ← presheaf.Hcomp'; refl },
  inv_fun :=
  { map := λ U H s, ⟨λ j, (φ i j).1.1 (S j ⊓ U) (le_inf (le_trans inf_le_right H) inf_le_left)
        ((F i).res _ _ _ (le_trans inf_le_right H) inf_le_right s),
      λ j k, begin
        have h1 : S j ⊓ S k ⊓ U ≤ S i ⊓ S j := le_inf (le_trans inf_le_right H) (le_trans inf_le_left inf_le_left),
        have h2 : S i ⊓ S j ⊓ S k ≤ S j ⊓ S k := by rw inf_assoc; exact inf_le_right,
        have h3 : S j ⊓ S k ⊓ U ≤ S i ⊓ S j ⊓ S k := by rw  [inf_comm, inf_assoc]; exact inf_le_inf H (le_refl _),
        have h4 : S j ⊓ S k ⊓ U ≤ S i ⊓ S k := le_inf (le_trans inf_le_right H) (le_trans inf_le_left inf_le_right),
        rw [← res_res_subset (F j) _ _ _ _ _ h1, ← (φ i j).1.2],
        rw ← equiv.res_subset_apply (φ j k) (S i ⊓ S j ⊓ S k) h2 (S j ⊓ S k ⊓ U) h3,
        rw ← equiv.res_subset_apply (φ i j) (S i ⊓ S j ⊓ S k) inf_le_left (S j ⊓ S k ⊓ U) h3,
        rw [← equiv.trans_apply, Hφ2 i j k, equiv.res_subset_apply, res_res_subset, res_res],
        rw [← res_res_subset (F k) _ _ _ _ _ h4, ← (φ i k).1.2, res_res_subset, res_res],
      end⟩,
    commutes := λ U HU V HV HVU s, subtype.eq $ funext $ λ j, by dsimp only [res_res_subset, sheaf_glue_res_val];
      rw [← res_res_subset (F j), ← (φ i j).1.2, res_res_subset, res_res, res_res] },
  left_inv := morphism.ext $ λ V HV s, subtype.eq $ funext $ λ j, have _, from s.2 i j, calc
      _ = (φ i j).1.map (S j ⊓ V) (le_inf (le_trans inf_le_right HV) inf_le_left)
            ((F i).res V HV (S j ⊓ V) (le_trans inf_le_right HV) inf_le_right
              ((F i).res (S i ⊓ V) _ V HV (le_inf HV (le_refl _)) (s.1 i))) : rfl
    ... = (φ i j).1.map (S j ⊓ V) _
            ((F i).res (S i ⊓ V) _ (S j ⊓ V) _ _ (s.1 i)) : by rw res_res
    ... = (φ i j).1.map (S j ⊓ V) _
            (((F i).res_subset (S i ⊓ S j) _).res ((S i ⊓ S j) ⊓ V) inf_le_left _ _
              (by rw [inf_assoc, inf_left_comm, inf_of_le_right HV]; exact le_refl _)
              ((F i).res (S i ⊓ V) _ ((S i ⊓ S j) ⊓ V) (le_trans inf_le_left inf_le_left)
                (le_inf (le_trans inf_le_left inf_le_left) inf_le_right)
                (s.1 i))) : by rw [res_res_subset, res_res]
    ... = s.1 j : by rw [(φ i j).1.2, s.2 i j, res_res_subset, res_res, res_self],
  right_inv := morphism.ext $ λ V HV s, by dsimp only [morphism.comp, morphism.id, id];
    erw [Hφ1, equiv.refl_apply (F i), res_res, res_self] }

[Kenny Lau]

it's computable!

[Kevin Buzzard]

I claim that the following would not be computable: if instead of S : I -> opens X we had done everything for s : set (opens X), and then we wanted to move back to S : I -> opens X, then s would be range S and we would start to have to make choices of a "canonical" element of I for every element of s.

[Mario Carneiro]

This is true. This passing back and forth is necessary if you want to support I in another universe

[Mario Carneiro]

You can support I in a lower universe if you use ulift, and maybe that's enough for one-universe man, but for higher universes I don't think it's possible without having some kind of super sheaf property

[Scott Morrison]

@Patrick Massot, there were some other files changed in that branch, so just bringing forward the one file wasn't going to work. I've merged master back into that branch, and it works again.

[Kevin Buzzard]

You can support I in a lower universe if you use ulift, and maybe that's enough for one-universe man, but for higher universes I don't think it's possible without having some kind of super sheaf property

Is there a way of formalising I : Type v <= u in Lean?

[Kevin Buzzard]

I am definitely one-universe man; I don't want to be ostracised by my ZFC chums.

[Mario Carneiro]

use max u v in place of u

[Mario Carneiro]

You realize that sheafs don't fit in one universe?

[Kevin Buzzard]

Of course they don't.

[Kevin Buzzard]

We never consider "the set of sheaves on X". We know how to treat sheaves.

[Mario Carneiro]

so... not really one universe then

[Kevin Buzzard]

We have sets and classes. Sheaves are a class.

[Kevin Buzzard]

It just means that you can't do certain things with them. Sets are a class. Groups are a class. This is fine.

[Mario Carneiro]

I'm quite familiar with "large category theory". It's not fun to do in strict ZFC

[Kevin Buzzard]

I'm not necessarily saying I believe this, but I know lots of people who do, and some of them get upset when people start going on about universes. I just want to make sure that these ZFC people have a voice.

[Mario Carneiro]

In fact, you have to get even more into universes if you are in strict ZFC mode - you just have more notions of universe and almost-universe

[Kevin Buzzard]

To be honest I can quite believe you. I've never had to worry about this though. People in other disciplines might.

[Mario Carneiro]

At the very least, it's hard to do category theory on small and large categories in lean without at least one universe variable and probably two

[Mario Carneiro]

unless you want two completely separate but parallel theories

[Kevin Buzzard]

Well we're making two completely separate but parallel theories of presheaves.

[Mario Carneiro]

I think that's more of a test - I don't see a good reason for both to exist in perpetuity

[Mario Carneiro]

Unless of course we decide they aren't really the same thing but they are just "spelled the same in maths"

[Mario Carneiro]

Which TBH may very well be the conclusion, especially for the really abstract sheaves on sites

[Kevin Buzzard]

@Scott Morrison Kenny has shown that it's possible to glue sheaves of types using a wicked trick which started this thread off. Before he did this, I had an absolutely miserable time trying to glue sheaves of types, because porting open sets from one subset to another was painful. Kenny has introduced the idea of defining a sheaf on a subset to be a sheaf on the whole space. Mario has introduced this total space idea which also made stuff easier. In my mind these two shortcuts are decisive; I had a nightmare working with this stuff before these two ideas, and it was much much easier working with them afterwards. They are distinct techniques -- Kenny's stops you from having to move from open set to open set, and Mario's fixes some possible type issues with U intersect V not being defeq to V intersect U.

What I fear about the "full category theory approach" (a presheaf is a functor) is that there will not be an analogue of these tricks, and there will be inevitable pain in making and using the API.

What I fear about the low-level approach is that we are now going to have to have glueing sheaves of groups extending glueing sheaves of types, then glueing sheaves of topological rings extending 5 other things, and so on.

There might be a middle approach, where one defines a sheaf to be a map from a complete lattice (or whatever) to the objects of a category, plus some extra data, rather than a functor. If one wants to use functors the question is whether glueing is still viable. Maybe there's just a straightforward analogue of Kenny's trick? Mario's trick would I think involve being able to identify the isomorphic full subcategories opens U \cap V of opens U and opens U \cap V of opens X. I don't think an equivalence is enough. Do you believe me or have I made a slip? Maybe you shouldn't take some of these things too seriously. Someone is going to have to sit down and work this stuff out and see if it actually works, or whether Lean 3 is not actually up to the task.

Given that I want sheaves of topological rings, this for me is an important issue.

[Mario Carneiro]

My trick doesn't work if the homs aren't Props

[Mario Carneiro]

and it's also a bit shaky on general target categories

[Mario Carneiro]

If you have categories on the domain and codomain, I don't think there is a viable alternative to the category theory approach

[Kevin Buzzard]

So glueing etale sheaves, which is super-important, will be interesting to do in Lean.

[Kevin Buzzard]

There's an explicit section about this in Milne when he's dealing with DVRs. I'll dig it up later today.

[Kevin Buzzard]

Although maybe there's a way to make the etale site work with Props? @Reid Barton @Johan Commelin what do you think?

[Mario Carneiro]

The basic trick is, if there is only one hom between objects, you can typically avoid mentioning it at all (not even enforcing its existence) with the right choice of types

[Mario Carneiro]

by comparison the category approach has you not mentioning anything except the homs, and leave the objects implicit

[Mario Carneiro]

generally this tends to be shorter because the names are shorter (proof names are relatively longer than hom names)

[Mario Carneiro]

and there are more operations with notation

[Kevin Buzzard]

It will be much easier for me to understand if I work on examples. This is why I tried Reid's CDGA exercise and this is why I got a student to do group cohomology (she finished last night by the way, we have group cohomology done in the traditional "hands-on" way with cocycles and coboundaries plus the proof of the long exact sequence of terms of low degree in the Hochschild-Serre spectral sequence). I'm working up to homological algebra by taking baby steps. I think defining etale cohomology of schemes will be a stress-test for the system. There will be universe issues, there will be this perennial debate about how to do sheaves, there will be CDGA-like issues when doing cohomology, all this stuff that we half-understand and where the community sometimes has more than one opinion on the best way to proceed. This could very naturally turn into a multi-person project which might teach us quite interesting things about how easy it is to do stuff which is crucial to e.g. Deligne's proof of the Weil conjectures, in Lean.

[Johan Commelin]

Although maybe there's a way to make the etale site work with Props? Reid Barton Johan Commelin what do you think?

My intuition says that it doesn't work. If L/K is a separable field extension, then you really don't want the hom-set L → L over K to be a Prop.

[Kevin Buzzard]

Aah yes, I was wondering if there was some way to cheat and fix things, but this is a pretty convincing example.

[Kevin Buzzard]

Does anyone here understand the pro-etale site?

[Kevin Buzzard]

[this a new Scholze thing]

[Mario Carneiro]

So if I understand it correctly you are talking about a "restriction map" that applies a field automorphism without changing the object?

[Kevin Buzzard]

Yes I guess so.

[Kevin Buzzard]

Spec(complexes) is a cover of Spec(reals); a cover of one object by one bigger object

[Kevin Buzzard]

Aah that's not the point.

[Kevin Buzzard]

The map Spec(complexes) -> Spec(reals) is an etale map, so the analogue of an "open subset" in the etale site. And complex conjugation is a perfectly good map which one can restrict along. An example of an etale sheaf on Spec(reals) would be an abelian group A plus an action of Gal(complexes/reals). Its global sections would be the fixed points for the action, the sections on the "open set" Spec(complexes) would be A, and the restriction map corresponding to complex conjugation would be the map coming from the non-trivial element of the Galois group.

[Kevin Buzzard]

The sheaf axiom says that if I have an element of A which is fixed under complex conjugation then it's a global section, that's why the global sections are the invariants for the action.

[Kevin Buzzard]

Open sets having automorphism groups gives rise to their sections having automorphism groups acting on them.

[Kevin Buzzard]

An etale sheaf of abelian groups on Spec(Q) is the same as an abelian group with an action of Gal(Q-bar/Q).

[Patrick Massot]

@Scott Morrison For the purpose of clarifying this discussion, I just pushed https://github.com/leanprover-community/mathlib/commit/e4308313b2b992d159d177771bc5ac581a20d331 which removes the sorry in the completion adjunction. Is this what I was meant to do? Or should I skip the intermediate lemma I created in the category language?

[Kenny Lau]

@Kevin Buzzard should the stalk be def-eq to the stalk or another quotient?

[Johan Commelin]

We already have stalks in mathlib.

[Kenny Lau]

where?

[Kenny Lau]

also what I was asking is: should the stalk [of a "sheaf on opens" as I have defined it] be definitionally equal to the stalk of the underlying sheaf, or should I make it another type consisting of a quotient?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/search?q=stalk&unscoped_q=stalk

[Kenny Lau]

How do I access that page from, say, the repo?

[Johan Commelin]

What do you mean?

[Kenny Lau]

never mind, I figured it out

[Kevin Buzzard]

A stalk is only defined up to canonical isomorphism so in some sense it's hard to answer the question. But defeq is good, right?

[Scott Morrison]

@Reid Barton

I still worry a bit that I don't know a math definition which encompasses both this example of sheaves of topological rings (on a topological space or whatever) and also sheaves on a general site.

I think https://stacks.math.columbia.edu/tag/00VL does it (right at the bottom) --- he uses Yoneda to say a presheaf F of Xs is a sheaf if all the Hom(X, F(-)) presheafs of sets are sheaves.

[Reid Barton]

Hmm, that does sound plausible

[David Michael Roberts]

Does anyone here understand the pro-etale site?

Mike Shulman and I are having a good discussion about pro-ét(*) by email. We have some ideas, but not clear how helpful they will be in this context. What did you want to know?

[Kevin Buzzard]

How to formalise it

[Johan Commelin]

0. Formalise the definition of the category of schemes.
1. Formalise the definition of a site.
2. Formalise the definition of a pro-étale morphism.
3. Show that pro-étale morphisms with suitable covers form a site.
But certainly you had something more in mind...

[Kevin Buzzard]

It's all the stuff about Postnikov towers converging in the hypercomplete infinity-topos in Bhatt-Scholze. There are some set-theoretic issues which I've never got my head around.

[Jesse Michael Han]

i thought pro-et(*) site was profinite sets with the coherent coverage, which would be easier to do

[Johan Commelin]

@Jesse Michael Han I guess that pro-et(k) is G-sets, where G is the profinite absolute Galois group of k. So pro-et(*) depends a bit on what you mean with *. I guess Kevin is interested in pro-et(S) for more general schemes S, and then the connection with profinite sets becomes even less clear. But profinite sets are certainly a good intuition.

[Kevin Buzzard]

It's the fpqc coverings that scare me.

[Kenny Lau]

What on earth is the right way to glue schemes / sheaves?

[Kevin Buzzard]

I've been distracted by writing a proof from first principles that every positive integer is uniquely the product of primes as part of an educational project, but my instinct is that your way is the easiest way to put into Lean but Scott's way via categories is "the way that mathematicians think it should be done" because mathematicians prefer the fancy structure. You were lucky here though -- opens X is a set. The class of etale morphisms Y -> X is not a set. The traditional fix is to only use the set of etale morphisms Y -> X where Y has some sort of cardinality constraints on it. I am still not really clear how to do this in Lean.