Zulip Chat Archive

Stream: maths

Topic: breaking equality with sheaves


view this post on Zulip Kevin Buzzard (Jun 21 2019 at 16:47):

A sheaf of types F\mathcal{F} on a topological space XX is, for every open set VXV\subseteq X, a type F(V)\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 UiU_i of XX and sheaves on each UiU_i which are compatible in some precise way, one can glue the sheaves together to get a sheaf on XX. 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 UiU_i and I had to constantly be moving between the type UiUjU_i\cap U_j, the open subset UiUjU_i\cap U_j of UiU_i, the open subset UiUjU_i\cap U_j of $U_j$$ and the open subset UiUjU_i\cap U_j of XX; all of these four objects show up. One of the compatibilities one needs is a "cocycle identity" which involves three subsets UiU_i, UjU_j and UkU_k, and it was pretty horrible.

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

In short, Kenny has proposed a definition of a sheaf on UU 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-UU (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-UU 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 UiU_i should be isomorphic to the sheaf Fi\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.

view this post on Zulip Kenny Lau (Jun 21 2019 at 17:47):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:56):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:57):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:57):

Perhaps your argument is that equality of sheaves is never ok

view this post on Zulip Kenny Lau (Jun 21 2019 at 17:57):

that is indeed my argument

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:58):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:58):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 17:59):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 18:02):

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.

view this post on Zulip Sebastien Gouezel (Jun 21 2019 at 18:30):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 18:31):

OK I'm convinced :-)

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 18:33):

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.

view this post on Zulip Sebastien Gouezel (Jun 21 2019 at 18:39):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 18:40):

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

view this post on Zulip Sebastien Gouezel (Jun 21 2019 at 18:41):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:03):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:24):

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.

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:45):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:47):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:48):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:48):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:48):

random meaning not uniquely defined

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:49):

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?

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:50):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:51):

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?

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:51):

There is more than one way.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:51):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:52):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:52):

mathematician naming at its best

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:52):

At least there are 6 of them.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:52):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:52):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:53):

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

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

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:53):

oh it's backwards?

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

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:54):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:54):

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

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

wait, notation

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

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.

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

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:55):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:56):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:57):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:57):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:58):

where 0 is an empty type?

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:58):

0 is an initial object.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:58):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 21:58):

so we can't really avoid some variation here

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:58):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 21:59):

I think the extension by 0 is OK.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:00):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:00):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:01):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:01):

is all this pain just to build the API?

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:01):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:02):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:03):

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.

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:03):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:03):

Not that I care, but you might.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:04):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:04):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:04):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:05):

Right!

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:05):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:05):

That's the definition of a sheaf.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 22:06):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 22:52):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:06):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:07):

To Type

view this post on Zulip Reid Barton (Jun 21 2019 at 23:07):

it had better be!

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:07):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:07):

which I think means products?

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:08):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:09):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:09):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:09):

the point I want to make involves res'

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:10):

And this total trick

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:10):

once again, untyped to the rescue

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:11):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:12):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:13):

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.

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:14):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:14):

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?

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:15):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:15):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:15):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:16):

You can change Type to a category here without changing anything

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:16):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:16):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:17):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:18):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:18):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:18):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:19):

Make this definition in the generality that you actually need

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:19):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:20):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:20):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:20):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:22):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:22):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:23):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:24):

like "what we need for the current major milestone"

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:24):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:25):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:27):

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.

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:27):

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

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:28):

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.

view this post on Zulip Kevin Buzzard (Jun 21 2019 at 23:29):

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.

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:35):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:38):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:56):

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

view this post on Zulip Mario Carneiro (Jun 21 2019 at 23:58):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 07:30):

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 OX\mathcal{O}_X-modules, where OX\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.

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:35):

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

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:36):

which is not actually a problem in most cases

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:37):

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

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:37):

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

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:38):

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

view this post on Zulip Mario Carneiro (Jun 22 2019 at 07:39):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 07:41):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 07:41):

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!

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:29):

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?

view this post on Zulip Kenny Lau (Jun 22 2019 at 12:29):

it's the cocycle condition right

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:30):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:30):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:31):

She's doing 3rd year project with me.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:31):

We're just trundling along learning about cocycles.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:31):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:33):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:33):

We're nearly there.

view this post on Zulip Reid Barton (Jun 22 2019 at 12:35):

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 Rn\mathbb{R}^n, and then the transition functions ϕ\phi can be seen as taking values in GL(n)GL(n).

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:36):

So there's your homework @Kenny Lau

view this post on Zulip Reid Barton (Jun 22 2019 at 12:36):

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

view this post on Zulip Reid Barton (Jun 22 2019 at 12:37):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:38):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 12:38):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 17:59):

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?

view this post on Zulip Johan Commelin (Jun 22 2019 at 18:41):

You can certainly do that locally, I guess.

view this post on Zulip Reid Barton (Jun 22 2019 at 18:47):

But can you glue the local instances into global instances?

view this post on Zulip Johan Commelin (Jun 22 2019 at 19:08):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 20:09):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 20:10):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 20:59):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:01):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:02):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:02):

I am unclear about this foundational issue.

view this post on Zulip Kenny Lau (Jun 22 2019 at 21:03):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:05):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:09):

Me trying to glue presheaves

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:32):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:51):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 21:59):

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.

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

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:07):

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

view this post on Zulip Kenny Lau (Jun 22 2019 at 22:08):

change universes u v to universes v u on L10

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:08):

Many thanks Kenny.

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

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?

view this post on Zulip Kenny Lau (Jun 22 2019 at 22:18):

I mean it doesn't compile right

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:18):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:19):

But I only have [semilattice_inf]

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

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:23):

which is this:

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:24):

What mathematical object is that called in Lean?

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:25):

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?

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:26):

How close is this to a topological space?

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

Is it some sort of bundled topological space?

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

Oh, is it precisely opens X or something?

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 22:29):

I could even try and prove this!

view this post on Zulip Reid Barton (Jun 22 2019 at 23:00):

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

view this post on Zulip Reid Barton (Jun 22 2019 at 23:01):

Sounds like you just have a complete lattice

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:02):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:19):

@Reid Barton is there this:

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

?

view this post on Zulip Reid Barton (Jun 22 2019 at 23:20):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:21):

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 ?

view this post on Zulip Kenny Lau (Jun 22 2019 at 23:22):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:22):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:22):

I don't know anything about lattices.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:22):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:23):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:24):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:25):

@Kenny Lau

#check complete_lattice.supr -- unknown

view this post on Zulip Kenny Lau (Jun 22 2019 at 23:25):

#check lattice.supr

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:26):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:28):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:50):

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

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:50):

@Reid Barton

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:59):

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.

view this post on Zulip Kevin Buzzard (Jun 22 2019 at 23:59):

I need to learn your language.

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

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:03):

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.

view this post on Zulip Reid Barton (Jun 23 2019 at 00:13):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:14):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:21):

import order.complete_lattice

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

Is that a poorly-named function in mathlib?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:28):

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:28):

Why is this happening?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:43):

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?

view this post on Zulip Reid Barton (Jun 23 2019 at 00:47):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:48):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:53):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:56):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 00:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:06):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:06):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:11):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:12):

the lattice.lattice thing is obviously not good

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:12):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:12):

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

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

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?

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

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:19):

What are you doing?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:19):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:19):

you should write <= and be done with it

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:19):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:20):

lattice is a top level namespace like category_theory

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:20):

it encloses most of the lattice-related constants

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:20):

but like I said, I think it should be removed

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:20):

Most of the time people open lattice for this reason

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:21):

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

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

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

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

They don't deserve a maths name

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:23):

Huh? that's pretty standard in mathlib

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:24):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:25):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:25):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:26):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:26):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:26):

That's an interesting suggestion

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:27):

I tend to use the notation that mathematicians use you see

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:27):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:27):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:27):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:28):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:28):

Maybe the maths conventions should just have one universe too

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:29):

:-)

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:29):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:30):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:31):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:31):

I just want library-wide consistency

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:33):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:41):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:42):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:43):

based solely on your statements, yes

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:44):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:45):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:46):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:46):

I did something like that in the sheaf axioms

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:47):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:47):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:47):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:48):

Let's call it 37 in that case.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:48):

that will definitely compromise the meaning of the statement

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:48):

only in your mind

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:49):

We know what we're doing in the maths department

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:49):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:49):

like gluing

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:49):

OK just make it to option.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:49):

sure, but again I'm not talking about totalization

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:50):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:50):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:50):

what if there is no lub?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:50):

I promise there is a lub

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:51):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:51):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:51):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:52):

And I say that that's your problem

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:52):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 01:53):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:54):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:56):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 01:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:34):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:46):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:46):

it can cause some unification problems

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:47):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:47):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:48):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:49):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:50):

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:50):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:52):

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

view this post on Zulip Jesse Michael Han (Jun 23 2019 at 02:52):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:53):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:53):

If you fill everything with sorry instead it should work

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:53):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:54):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:54):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:54):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:54):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:55):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:55):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:56):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:56):

You and I have different ideas about fun.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:56):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:57):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:57):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:58):

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

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 02:58):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 02:59):

some of this is architectural stuff you should ask Johannes

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:01):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:02):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:02):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:03):

First you want to prove it's a lattice

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:03):

golly it's 4am

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:03):

then you prove it's a complete lattice

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:03):

First you want to prove it's a lattice

How did you know that?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:03):

My algorithm is buggy here.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:03):

because that's the way the hierarchy is set up

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:04):

But how can I work that out for myself?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:04):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:04):

look at the extends clauses

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:04):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:06):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:08):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:10):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:12):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:16):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:17):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 03:18):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:34):

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? :-/

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:37):

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

why u hate me Lean

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:39):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 03:39):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 04:03):

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 04:04):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 04:08):

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 04:14):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 04:32):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 04:32):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 04:32):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:06):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:06):

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?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:10):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:11):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:12):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:13):

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'

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:13):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:13):

thing.{v} α

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:13):

got it

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:14):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:15):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:15):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:17):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:17):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:18):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:18):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:18):

That's an interesting analogue

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:19):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:20):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:20):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:21):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:21):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:21):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:21):

sure you can

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:22):

do you have an example?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:22):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:23):

Yes

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:23):

I had not realised this

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:23):

The definition I gave of gluing and locality uses subsets

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:23):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:23):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:24):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:24):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:25):

what are the types of the relevant objects?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:25):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:26):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:27):

This is a theorem, though, right?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:27):

I don't know.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:27):

you wrote := sorry so I assume so

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:28):

this is supposed to follow from the axioms of sheaves

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:28):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:30):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:31):

Exercise 1.22 of one of the early chapters.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:31):

the proof args make me weep

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:31):

Just tell me how to do it.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:31):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:32):

Probably chapter 2, I think section 2.1 is sheaves.

view this post on Zulip Johan Commelin (Jun 23 2019 at 05:32):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 05:32):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:34):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:34):

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

My partner is away :-)

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:36):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 05:36):

In the opens case, not in the lattice case.

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

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:12):

I rolled my own sup from supr

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:13):

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?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:24):

you can use ulift bool

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:24):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:25):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:38):

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?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:42):

Why does thing still take two universe args?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:42):

I'm scared Mario

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:43):

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

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

I am not sure that sets are enough for glueing

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:43):

You aren't using sets

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:43):

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

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

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:44):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:45):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:49):

infixr ` ↪⊓⨆ `:25 := semilattice_inf_lub_emb

I'm liking that.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:51):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 06:52):

That's the goal

view this post on Zulip Johan Commelin (Jun 23 2019 at 06:53):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 06:54):

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

view this post on Zulip Johan Commelin (Jun 23 2019 at 06:59):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:10):

But is it a presheaf over a complete lattice?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:11):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:13):

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

view this post on Zulip Johan Commelin (Jun 23 2019 at 07:13):

You can still just work over complete lattices.

view this post on Zulip Johan Commelin (Jun 23 2019 at 07:13):

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

view this post on Zulip Johan Commelin (Jun 23 2019 at 07:14):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:25):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:25):

You have to "sheafify".

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:26):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:26):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:27):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:27):

You can't make sheaves on an arbitrary category.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:28):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:28):

okay, how's that work?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:28):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:29):

Wait, this is about the domain category

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:29):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:29):

mathlib presheaves are on top spaces

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:29):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:29):

The category here is the target, replacing Type

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:30):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:30):

I don't

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:30):

No?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:30):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:30):

I just want to know why it's bundled

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:31):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:31):

or general categories, and then you have this site business

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:32):

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?

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:32):

It might be best to do presheaf_on_opens first

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:32):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:33):

or more generally a sheaf on some object isomorphic to that

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:33):

So you really want to carry the subtype around?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:33):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:35):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:35):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:36):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:37):

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}

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:38):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:39):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:40):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:40):

they are too pointed

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:46):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:47):

universes u v

open lattice

variables {α : Type u} [semilattice_inf α]

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:51):

there's that too

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:54):

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

:-(

view this post on Zulip Mario Carneiro (Jun 23 2019 at 07:56):

it's not hard to prove

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:57):

I just thought it would happen by magic

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 07:58):

but semilattice_inf extends has_inf

view this post on Zulip Mario Carneiro (Jun 23 2019 at 08:04):

you have to define that too

view this post on Zulip Mario Carneiro (Jun 23 2019 at 08:04):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 08:05):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:37):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:38):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:39):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:39):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:39):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:40):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:40):

I was having trouble getting this to work.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:40):

Which lines do you think I can delete?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:40):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:41):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:42):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:49):

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.

view this post on Zulip Mario Carneiro (Jun 23 2019 at 09:57):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 09:58):

Thanks.

view this post on Zulip Reid Barton (Jun 23 2019 at 10:13):

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.

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

Do we have frames in mathlib?

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

can we glue sheaves on sites?

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

We can't glue anything on anything right now

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 10:18):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 10:18):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 10:22):

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

view this post on Zulip Mario Carneiro (Jun 23 2019 at 10:22):

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

view this post on Zulip Jesse Michael Han (Jun 23 2019 at 12:39):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 12:51):

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?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 12:52):

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

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:24):

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 }

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:25):

I have |no idea| what I was doing

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:31):

I should extract defs/lemmas

view this post on Zulip Johan Commelin (Jun 23 2019 at 17:54):

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.

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 18:11):

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

view this post on Zulip Kevin Buzzard (Jun 23 2019 at 18:12):

That's quite some calc by the way!

view this post on Zulip Patrick Massot (Jun 24 2019 at 08:41):

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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 08:42):

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

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 08:46):

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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 08:57):

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

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:06):

@Patrick Massot I'm sad to hear that story

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:07):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:09):

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

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:10):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:10):

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

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:11):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:11):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:12):

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

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:13):

The moment homs are not Props, basically.

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:13):

right

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:13):

Your glue and universal_property theorems look like that

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:14):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:15):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 09:15):

try it both ways and let the best infrastructure win

view this post on Zulip Scott Morrison (Jun 24 2019 at 10:35):

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.

view this post on Zulip Scott Morrison (Jun 24 2019 at 10:37):

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

view this post on Zulip Scott Morrison (Jun 24 2019 at 10:40):

The file we wrote that afternoon is here.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:30):

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?

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:30):

This deserves a new thread really.

view this post on Zulip Mario Carneiro (Jun 24 2019 at 11:36):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 11:37):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 11:39):

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

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:40):

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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:42):

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.

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

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

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

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.

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

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?

view this post on Zulip Reid Barton (Jun 24 2019 at 11:50):

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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:51):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 11:51):

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

view this post on Zulip Reid Barton (Jun 24 2019 at 11:55):

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

view this post on Zulip Reid Barton (Jun 24 2019 at 11:59):

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

view this post on Zulip Reid Barton (Jun 24 2019 at 12:02):

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

view this post on Zulip Reid Barton (Jun 24 2019 at 12:04):

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.

view this post on Zulip Scott Morrison (Jun 24 2019 at 22:37):

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!

view this post on Zulip Scott Morrison (Jun 24 2019 at 22:41):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 22:44):

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

view this post on Zulip Mario Carneiro (Jun 24 2019 at 22:46):

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

view this post on Zulip Scott Morrison (Jun 24 2019 at 22:54):

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

view this post on Zulip Reid Barton (Jun 24 2019 at 22:57):

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.

view this post on Zulip Reid Barton (Jun 24 2019 at 22:59):

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!

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 06:46):

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?

view this post on Zulip Johan Commelin (Jun 25 2019 at 07:56):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 07:56):

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.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 07:58):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 08:01):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:08):

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

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:09):

No, no universe variables. :-)

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:09):

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.

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:10):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:10):

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"

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:11):

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.

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:12):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:12):

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.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:14):

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"

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:17):

That one is easy to fix. :-)

view this post on Zulip Scott Morrison (Jun 25 2019 at 08:17):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 08:31):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 08:32):

and I never used the cocycle conditions

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:37):

Maybe you need them to prove the universal property?

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:37):

This is not proved even for presheaves.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:39):

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.

view this post on Zulip Kenny Lau (Jun 25 2019 at 08:41):

that is indeed what you gave me

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:42):

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.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:43):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 08:43):

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

view this post on Zulip Patrick Massot (Jun 25 2019 at 09:34):

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

view this post on Zulip Patrick Massot (Jun 25 2019 at 09:41):

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.

view this post on Zulip Patrick Massot (Jun 25 2019 at 09:42):

You'll see subtype uniform_continuous appearing everywhere

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

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

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

it's computable!

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:41):

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.

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:43):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:44):

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

view this post on Zulip Scott Morrison (Jun 25 2019 at 10:45):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:50):

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?

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:51):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:51):

use max u v in place of u

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:51):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:52):

Of course they don't.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:52):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:52):

so... not really one universe then

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:52):

We have sets and classes. Sheaves are a class.

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

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:53):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:54):

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.

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:54):

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

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

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:56):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:57):

unless you want two completely separate but parallel theories

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 10:57):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:58):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 10:59):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:00):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:12):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:14):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:16):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:16):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:18):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:18):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:19):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:20):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:22):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:22):

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

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:23):

and there are more operations with notation

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:29):

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.

view this post on Zulip Johan Commelin (Jun 25 2019 at 11:29):

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.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:35):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:37):

Does anyone here understand the pro-etale site?

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:37):

[this a new Scholze thing]

view this post on Zulip Mario Carneiro (Jun 25 2019 at 11:37):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:38):

Yes I guess so.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:38):

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

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:39):

Aah that's not the point.

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 11:42):

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.

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

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.

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

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

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

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

view this post on Zulip Patrick Massot (Jun 25 2019 at 11:49):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 18:59):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:02):

We already have stalks in mathlib.

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:03):

where?

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:04):

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?

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:05):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:06):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:08):

What do you mean?

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:09):

never mind, I figured it out

view this post on Zulip Kevin Buzzard (Jun 25 2019 at 21:18):

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?

view this post on Zulip Scott Morrison (Jun 25 2019 at 22:52):

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

view this post on Zulip Reid Barton (Jun 26 2019 at 02:41):

Hmm, that does sound plausible

view this post on Zulip David Michael Roberts (Jul 02 2019 at 04:21):

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?

view this post on Zulip Kevin Buzzard (Jul 02 2019 at 06:32):

How to formalise it

view this post on Zulip Johan Commelin (Jul 02 2019 at 07:16):

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

view this post on Zulip Kevin Buzzard (Jul 02 2019 at 08:22):

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.

view this post on Zulip Jesse Michael Han (Jul 02 2019 at 10:06):

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

view this post on Zulip Johan Commelin (Jul 02 2019 at 13:12):

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

view this post on Zulip Kevin Buzzard (Jul 02 2019 at 16:52):

It's the fpqc coverings that scare me.

view this post on Zulip Kenny Lau (Jul 04 2019 at 15:39):

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

view this post on Zulip Kevin Buzzard (Jul 04 2019 at 16:13):

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.


Last updated: May 19 2021 at 00:40 UTC