## Stream: maths

### Topic: breaking equality with sheaves

#### Kevin Buzzard (Jun 21 2019 at 16:47):

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

As part of the schemes project we would like to glue sheaves on open subsets. In short, given an open cover $U_i$ of $X$ and sheaves on each $U_i$ which are compatible in some precise way, one can glue the sheaves together to get a sheaf on $X$. I tried to formalise this the naive way, and formalising the compatibility was a real nightmare, because a sheaf is on a topological space so I had to really work with types $U_i$ and I had to constantly be moving between the type $U_i\cap U_j$, the open subset $U_i\cap U_j$ of $U_i$, the open subset $U_i\cap U_j$ of $U_j$and the open subset $U_i\cap U_j$ of $X$; all of these four objects show up. One of the compatibilities one needs is a "cocycle identity" which involves three subsets $U_i$, $U_j$ and $U_k$, and it was pretty horrible. Kenny suggested a completely insane way around this. He defined a sheaf on an open subset $U$ of $X$ to simply be a sheaf on $X$! It is true that given a sheaf on an open subset $U\subseteq X$ one can push it forward to get a sheaf on $X$, given a sheaf on $X$ one can pull it back to get a sheaf on an open subset $U$, but it is also true that two sheaves on $X$ which are not equal (resp isomorphic), can become equal (resp isomorphic) when restricted to $U$. In short, Kenny has proposed a definition of a sheaf on $U$ for which Lean's = type is wrong -- it does not correctly capture the notion of equality of sheaves. Kenny went on to define morphisms of sheaves-on-$U$ (using his definition) and a notion of equiv which is the correct definition. So we do have the correct notion of isomorphism, and the sheaves-on-$U$ form a category which is equivalent to the correct category. This category has the extraordinary (to me) property that the notion of equality on it is incorrect. However I have just formalised the statement of the universal property which the glued sheaf has to satisfy (its restriction to the $U_i$ should be isomorphic to the sheaf $\mathcal{F}_i$ we started with -- not equal to it) and at least the statement looks fine. Am I going to run into trouble later? One way of thinking about this is that a sheaf is a functor, so we have made some functor category, and we are interested in restricting this functor to a subcategory to get a new functor category, and I want to define it to be the actual restriction, but Kenny has just defined it to be the original functor and has basically said screw equality. #### Kenny Lau (Jun 21 2019 at 17:47): we don't ever want to say that two (at least set-valued-) sheaves are equal right #### 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 #### 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 #### Kevin Buzzard (Jun 21 2019 at 17:57): Perhaps your argument is that equality of sheaves is never ok #### Kenny Lau (Jun 21 2019 at 17:57): that is indeed my argument #### 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 #### Kevin Buzzard (Jun 21 2019 at 17:58): But I have become more and more confused about what "the same" means recently #### 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 #### 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. #### 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. #### Kevin Buzzard (Jun 21 2019 at 18:31): OK I'm convinced :-) #### 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. #### 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. #### 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. #### 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. #### 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 #### 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. #### 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 #### 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. #### 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. #### 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 #### Mario Carneiro (Jun 21 2019 at 21:48): random meaning not uniquely defined #### 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? #### 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 #### 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? #### Kevin Buzzard (Jun 21 2019 at 21:51): There is more than one way. #### Kevin Buzzard (Jun 21 2019 at 21:51): You don't know about the 6 functor formalism? ;-) #### Kevin Buzzard (Jun 21 2019 at 21:52): https://en.wikipedia.org/wiki/Six_operations #### Mario Carneiro (Jun 21 2019 at 21:52): mathematician naming at its best #### Kevin Buzzard (Jun 21 2019 at 21:52): At least there are 6 of them. #### 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. #### 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. #### 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? #### 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. #### Mario Carneiro (Jun 21 2019 at 21:53): oh it's backwards? #### 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. #### Mario Carneiro (Jun 21 2019 at 21:54): I want the original one you said, sheaf on U -> sheaf on X #### Kevin Buzzard (Jun 21 2019 at 21:54): That one is just G(V)=F(V) #### Kevin Buzzard (Jun 21 2019 at 21:55): wait, notation #### 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. #### Kevin Buzzard (Jun 21 2019 at 21:55): The trivial thing is going from X to U. U is a subset of X here. #### 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 #### 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 #### 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. #### 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 :-/ #### Mario Carneiro (Jun 21 2019 at 21:58): where 0 is an empty type? #### Kevin Buzzard (Jun 21 2019 at 21:58): 0 is an initial object. #### Kevin Buzzard (Jun 21 2019 at 21:58): I'm thinking about sheaves taking values in some arbitrary category really. #### Mario Carneiro (Jun 21 2019 at 21:58): so we can't really avoid some variation here #### Kevin Buzzard (Jun 21 2019 at 21:58): I'm thinking about sheaves taking values in the category of abelian groups, truth be told. #### Kevin Buzzard (Jun 21 2019 at 21:59): I think the extension by 0 is OK. #### 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!" #### 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 #### 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 ;-) #### Mario Carneiro (Jun 21 2019 at 22:01): is all this pain just to build the API? #### Kevin Buzzard (Jun 21 2019 at 22:01): Kenny built an API for sheaves on U just being sheaves on X. #### 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  #### 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. #### Mario Carneiro (Jun 21 2019 at 22:03): wait so you still have a separate definition? This seems like a lot of duplication #### Kevin Buzzard (Jun 21 2019 at 22:03): Not that I care, but you might. #### 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  #### 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 #### Mario Carneiro (Jun 21 2019 at 22:04): The res function need not take a proof arg, nor eval #### Kevin Buzzard (Jun 21 2019 at 22:05): Right! #### Kevin Buzzard (Jun 21 2019 at 22:05): https://github.com/ramonfmir/lean-scheme/blob/master/src/sheaves/sheaf.lean #### Kevin Buzzard (Jun 21 2019 at 22:05): That's the definition of a sheaf. #### Kevin Buzzard (Jun 21 2019 at 22:06): It uses the file presheaf.lean in the same directory, plus epsilon about open coverings. #### 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  #### Kevin Buzzard (Jun 21 2019 at 23:06): I think your definition of presheaf is essentially the definition of a functor #### Kevin Buzzard (Jun 21 2019 at 23:07): To Type #### Reid Barton (Jun 21 2019 at 23:07): it had better be! #### 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 #### Mario Carneiro (Jun 21 2019 at 23:07): which I think means products? #### 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 #### 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 #### 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. #### Mario Carneiro (Jun 21 2019 at 23:09): the point I want to make involves res' #### Kevin Buzzard (Jun 21 2019 at 23:10): And this total trick #### Mario Carneiro (Jun 21 2019 at 23:10): once again, untyped to the rescue #### 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 #### 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 #### 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. #### 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  #### 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? #### 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 #### Mario Carneiro (Jun 21 2019 at 23:15): All I'm doing is layering a more convenient API on top #### 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. #### Mario Carneiro (Jun 21 2019 at 23:16): You can change Type to a category here without changing anything #### 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 #### 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 #### 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 #### 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. #### 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 #### 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 #### Mario Carneiro (Jun 21 2019 at 23:19): Make this definition in the generality that you actually need #### 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. #### 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. #### Kevin Buzzard (Jun 21 2019 at 23:20): That's what we'll need when we start doing etale cohomology. #### 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. #### 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. #### Kevin Buzzard (Jun 21 2019 at 23:22): Not least because you might be out of date in 5 years anyway. #### 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 #### Mario Carneiro (Jun 21 2019 at 23:24): like "what we need for the current major milestone" #### Kevin Buzzard (Jun 21 2019 at 23:24): For all I know they're doing sheaves on infinity,1 categories nowadays. #### 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 #### 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. #### 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? #### 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. #### 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. #### 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)]  #### 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 #### 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 #### 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 #### 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 $\mathcal{O}_X$-modules, where $\mathcal{O}_X$ is the traditional name for the standard sheaf of rings on a scheme, the structure sheaf (namely the sheaf of functions on the scheme). I am unclear about why Mario is unhappy about the definition containing random junk. #### Mario Carneiro (Jun 22 2019 at 07:35): It can always be done, but you get some thing that's not in the category in general #### Mario Carneiro (Jun 22 2019 at 07:36): which is not actually a problem in most cases #### 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 #### 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 #### Mario Carneiro (Jun 22 2019 at 07:38): I will grant that consistently using a "weird equiv" will mostly make this decision invisible #### 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 #### 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. #### 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! #### 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? #### Kenny Lau (Jun 22 2019 at 12:29): it's the cocycle condition right #### Kevin Buzzard (Jun 22 2019 at 12:30): https://github.com/anca797/group-cohomology #### Kevin Buzzard (Jun 22 2019 at 12:30): @Anca Ciobanu 's definition of a 1-cocycle is in that link. #### Kevin Buzzard (Jun 22 2019 at 12:31): She's doing 3rd year project with me. #### Kevin Buzzard (Jun 22 2019 at 12:31): We're just trundling along learning about cocycles. #### Kevin Buzzard (Jun 22 2019 at 12:31): So can you make a cocycle from something which people call the cocycle condition? #### 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. #### Kevin Buzzard (Jun 22 2019 at 12:33): We're nearly there. #### 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 $\mathbb{R}^n$, and then the transition functions $\phi$ can be seen as taking values in $GL(n)$. #### Kevin Buzzard (Jun 22 2019 at 12:36): So there's your homework @Kenny Lau #### Reid Barton (Jun 22 2019 at 12:36): It's not group cohomology though, it's some kind of nonabelian Cech cohomology ($H^1$) #### 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 #### 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. #### 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. #### 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? #### Johan Commelin (Jun 22 2019 at 18:41): You can certainly do that locally, I guess. #### Reid Barton (Jun 22 2019 at 18:47): But can you glue the local instances into global instances? #### Johan Commelin (Jun 22 2019 at 19:08): They need to satisfy a cocycle condition, I guess (-; #### Kevin Buzzard (Jun 22 2019 at 20:09): Fortunately I think that cocycle condition is vacuous for some reason, possibly proof irrelevance #### 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 #### 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? #### 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. #### 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? #### Kevin Buzzard (Jun 22 2019 at 21:02): I am unclear about this foundational issue. #### 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 #### 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. #### Kevin Buzzard (Jun 22 2019 at 21:09): Me trying to glue presheaves #### 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. #### 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. #### 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. #### 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 #### 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? #### Kenny Lau (Jun 22 2019 at 22:08): change universes u v to universes v u on L10 #### Kevin Buzzard (Jun 22 2019 at 22:08): Many thanks Kenny. #### 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? #### Kenny Lau (Jun 22 2019 at 22:18): I mean it doesn't compile right #### Kevin Buzzard (Jun 22 2019 at 22:18): That's right. I need to take infinite unions at this point. #### Kevin Buzzard (Jun 22 2019 at 22:19): But I only have [semilattice_inf] #### 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. #### 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)  #### Kevin Buzzard (Jun 22 2019 at 22:24): What mathematical object is that called in Lean? #### 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? #### Kevin Buzzard (Jun 22 2019 at 22:26): How close is this to a topological space? #### Kevin Buzzard (Jun 22 2019 at 22:27): Is it some sort of bundled topological space? #### Kevin Buzzard (Jun 22 2019 at 22:28): Oh, is it precisely opens X or something? #### Kevin Buzzard (Jun 22 2019 at 22:29): I could even try and prove this! #### 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? #### Reid Barton (Jun 22 2019 at 23:01): Sounds like you just have a complete lattice #### 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. #### Kevin Buzzard (Jun 22 2019 at 23:19): @Reid Barton is there this: def complete_lattice.Union : Π {I : Type 37}, (I → α) → α  ? #### 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 → α) #### 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 ? #### Kenny Lau (Jun 22 2019 at 23:22): I'm not very sure what you want to do. Isn't this just supr? #### 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. #### Kevin Buzzard (Jun 22 2019 at 23:22): I don't know anything about lattices. #### Kevin Buzzard (Jun 22 2019 at 23:22): The API is huge and I've never looked at it. #### 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 ;-) #### 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". #### Kevin Buzzard (Jun 22 2019 at 23:25): @Kenny Lau #check complete_lattice.supr -- unknown  #### Kenny Lau (Jun 22 2019 at 23:25): #check lattice.supr  #### Kevin Buzzard (Jun 22 2019 at 23:26): Is complete_lattice.supr a hole in mathlib? @Mario Carneiro ? #### 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. #### 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? #### Kevin Buzzard (Jun 22 2019 at 23:50): @Reid Barton #### 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. #### Kevin Buzzard (Jun 22 2019 at 23:59): I need to learn your language. #### Kevin Buzzard (Jun 23 2019 at 00:00): Oh I guess I know exactly where to look in the mathlib API. #### 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. #### 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 #### 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?? #### 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? #### 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? #### Kevin Buzzard (Jun 23 2019 at 00:28): Why is this happening? #### 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? #### Reid Barton (Jun 23 2019 at 00:47): You put the [complete_lattice \a] to the right of the colon #### 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. #### Kevin Buzzard (Jun 23 2019 at 00:53): I am writing some completely mechanical code, made possible because of excellent naming conventions @Mario Carneiro #### 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. #### 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? #### Kevin Buzzard (Jun 23 2019 at 00:57): Is that the language that the simp lemmas will be in? #### 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 #### 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? #### Mario Carneiro (Jun 23 2019 at 01:11): this is a naming bug which we haven't done anything about yet #### Mario Carneiro (Jun 23 2019 at 01:12): the lattice.lattice thing is obviously not good #### Mario Carneiro (Jun 23 2019 at 01:12): I think far too much stuff ended up in the lattice namespace, including lattice itself #### 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? #### 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? #### 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. #### Mario Carneiro (Jun 23 2019 at 01:19): What are you doing? #### Mario Carneiro (Jun 23 2019 at 01:19): you shouldn't need to write anything remotely close to either of those #### Mario Carneiro (Jun 23 2019 at 01:19): you should write <= and be done with it #### 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. #### Mario Carneiro (Jun 23 2019 at 01:20): lattice is a top level namespace like category_theory #### Mario Carneiro (Jun 23 2019 at 01:20): it encloses most of the lattice-related constants #### Mario Carneiro (Jun 23 2019 at 01:20): but like I said, I think it should be removed #### Mario Carneiro (Jun 23 2019 at 01:20): Most of the time people open lattice for this reason #### Mario Carneiro (Jun 23 2019 at 01:21): I'm amused you think complete lattices are a CS thing #### 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 #### Kevin Buzzard (Jun 23 2019 at 01:23): They don't deserve a maths name #### Mario Carneiro (Jun 23 2019 at 01:23): Huh? that's pretty standard in mathlib #### Kevin Buzzard (Jun 23 2019 at 01:24): I know but I tell my undergraduates to use maths notation for mathsy stuff #### Mario Carneiro (Jun 23 2019 at 01:25): what notation are you going to give complete_lattice? That's plain text in maths #### 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 #### 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 #### Mario Carneiro (Jun 23 2019 at 01:26): I'm sure if you had written complete lattices it would use L as well #### Kevin Buzzard (Jun 23 2019 at 01:26): That's an interesting suggestion #### Kevin Buzzard (Jun 23 2019 at 01:27): I tend to use the notation that mathematicians use you see #### 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 #### Mario Carneiro (Jun 23 2019 at 01:27): and I don't care enough to do anything about it #### Kevin Buzzard (Jun 23 2019 at 01:27): But I've never seen a mathematician talking about compete lattices in the number theory seminar #### Kevin Buzzard (Jun 23 2019 at 01:28): The maths stuff gets maths names and the weird stuff can have computer science names. #### Kevin Buzzard (Jun 23 2019 at 01:28): Maybe the maths conventions should just have one universe too #### Kevin Buzzard (Jun 23 2019 at 01:29): :-) #### 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 #### 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 #### 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 #### Mario Carneiro (Jun 23 2019 at 01:31): I just want library-wide consistency #### 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 #### Kevin Buzzard (Jun 23 2019 at 01:41): I can't appeal to alpha-equivalence? ;-) #### 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. #### Mario Carneiro (Jun 23 2019 at 01:43): based solely on your statements, yes #### 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 #### 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 #### 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" #### Mario Carneiro (Jun 23 2019 at 01:46): I did something like that in the sheaf axioms #### Kevin Buzzard (Jun 23 2019 at 01:47): but I sort-of feel that Assia would be frowning. #### 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 #### 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 #### Kevin Buzzard (Jun 23 2019 at 01:48): Let's call it 37 in that case. #### Mario Carneiro (Jun 23 2019 at 01:48): that will definitely compromise the meaning of the statement #### Kevin Buzzard (Jun 23 2019 at 01:48): only in your mind #### Kevin Buzzard (Jun 23 2019 at 01:49): We know what we're doing in the maths department #### 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 #### Mario Carneiro (Jun 23 2019 at 01:49): like gluing #### Kevin Buzzard (Jun 23 2019 at 01:49): OK just make it to option. #### Mario Carneiro (Jun 23 2019 at 01:49): sure, but again I'm not talking about totalization #### Mario Carneiro (Jun 23 2019 at 01:50): what does the theorem say if you apply it to a set with no lub? #### 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. #### Mario Carneiro (Jun 23 2019 at 01:50): what if there is no lub? #### Kevin Buzzard (Jun 23 2019 at 01:50): I promise there is a lub #### Mario Carneiro (Jun 23 2019 at 01:51): if it's a semilattice_inf there may not be a lub #### Kevin Buzzard (Jun 23 2019 at 01:51): well there are lubs in the only model I'm interested in, which is opens #### 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 #### Kevin Buzzard (Jun 23 2019 at 01:52): And I say that that's your problem #### Kevin Buzzard (Jun 23 2019 at 01:52): because I promise I will never run that code in the absence of an upper bound #### 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. #### 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 #### 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 #### 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 #### 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. #### 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 #### Mario Carneiro (Jun 23 2019 at 02:46): it can cause some unification problems #### Mario Carneiro (Jun 23 2019 at 02:47): but I can't diagnose that problem based on the error alone. What's the context? #### 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. #### Mario Carneiro (Jun 23 2019 at 02:48): that is the rule, and the lattice theorems don't follow it #### Kevin Buzzard (Jun 23 2019 at 02:49): https://github.com/kbuzzard/xena/blob/1284a71aa327040494f13babb336c73d41680787/Examples/sheaf_on_opens_total_glueing.lean#L274 #### 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? #### 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? #### Mario Carneiro (Jun 23 2019 at 02:52): what the heck is going on in your file? What is thing? #### 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 #### 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 #### Mario Carneiro (Jun 23 2019 at 02:53): If you fill everything with sorry instead it should work #### 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 #### 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. #### 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. #### 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 #### 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. #### 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. #### 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 #### 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" #### Kevin Buzzard (Jun 23 2019 at 02:56): You and I have different ideas about fun. #### 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 #### 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. #### Mario Carneiro (Jun 23 2019 at 02:57): I think this might be proven in the complete_lattice.lean file #### 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. #### 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? #### 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. #### Mario Carneiro (Jun 23 2019 at 02:59): some of this is architectural stuff you should ask Johannes #### 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 #### 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 #### 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. #### Mario Carneiro (Jun 23 2019 at 03:03): First you want to prove it's a lattice #### Kevin Buzzard (Jun 23 2019 at 03:03): golly it's 4am #### Mario Carneiro (Jun 23 2019 at 03:03): then you prove it's a complete lattice #### Kevin Buzzard (Jun 23 2019 at 03:03): First you want to prove it's a lattice How did you know that? #### Kevin Buzzard (Jun 23 2019 at 03:03): My algorithm is buggy here. #### Mario Carneiro (Jun 23 2019 at 03:03): because that's the way the hierarchy is set up #### Kevin Buzzard (Jun 23 2019 at 03:04): But how can I work that out for myself? #### Mario Carneiro (Jun 23 2019 at 03:04): it's actually broken up into quite a few more pieces than that #### Mario Carneiro (Jun 23 2019 at 03:04): look at the extends clauses #### 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. #### 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 #### 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 #### 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 #### 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. #### 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 #### 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 #### 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) #### 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? :-/ #### 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 #### Kevin Buzzard (Jun 23 2019 at 03:39): Oh I just have to fill in random fields and hope. #### Kevin Buzzard (Jun 23 2019 at 03:39): All I know is that Lean wants me to prove ?m_1 etc #### 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? #### 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. #### 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?

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

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

#### Mario Carneiro (Jun 23 2019 at 04:32):

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

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

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

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

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

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

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

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


#### Mario Carneiro (Jun 23 2019 at 05:13):

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

#### Kevin Buzzard (Jun 23 2019 at 05:13):

thing.{v} α

got it

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

#### Mario Carneiro (Jun 23 2019 at 05:15):

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

#### Kevin Buzzard (Jun 23 2019 at 05:15):

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

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

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

#### Kevin Buzzard (Jun 23 2019 at 05:18):

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

#### Mario Carneiro (Jun 23 2019 at 05:18):

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

#### Kevin Buzzard (Jun 23 2019 at 05:18):

That's an interesting analogue

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

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

#### Mario Carneiro (Jun 23 2019 at 05:20):

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

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

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

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

sure you can

#### Mario Carneiro (Jun 23 2019 at 05:22):

do you have an example?

#### Kevin Buzzard (Jun 23 2019 at 05:22):

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

Yes

#### Mario Carneiro (Jun 23 2019 at 05:23):

The definition I gave of gluing and locality uses subsets

#### Kevin Buzzard (Jun 23 2019 at 05:23):

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

#### Mario Carneiro (Jun 23 2019 at 05:23):

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

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

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

#### Mario Carneiro (Jun 23 2019 at 05:25):

what are the types of the relevant objects?

#### 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  #### 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. #### Mario Carneiro (Jun 23 2019 at 05:27): This is a theorem, though, right? #### Kevin Buzzard (Jun 23 2019 at 05:27): I don't know. #### Mario Carneiro (Jun 23 2019 at 05:27): you wrote := sorry so I assume so #### Mario Carneiro (Jun 23 2019 at 05:28): this is supposed to follow from the axioms of sheaves #### Kevin Buzzard (Jun 23 2019 at 05:28): I don't know if it's true. It's a conjecture. #### 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. #### Kevin Buzzard (Jun 23 2019 at 05:31): Exercise 1.22 of one of the early chapters. #### Mario Carneiro (Jun 23 2019 at 05:31): the proof args make me weep #### Kevin Buzzard (Jun 23 2019 at 05:31): Just tell me how to do it. #### 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. #### Kevin Buzzard (Jun 23 2019 at 05:32): Probably chapter 2, I think section 2.1 is sheaves. #### Johan Commelin (Jun 23 2019 at 05:32): @Kevin Buzzard Did you just pull an all-nighter gluing sheaves :lol: #### 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 #### 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. #### Kevin Buzzard (Jun 23 2019 at 05:34): Kevin Buzzard Did you just pull an all-nighter gluing sheaves :lol: My partner is away :-) #### 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. #### Kevin Buzzard (Jun 23 2019 at 05:36): In the opens case, not in the lattice case. #### 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? #### Kevin Buzzard (Jun 23 2019 at 06:12): I rolled my own sup from supr #### 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? #### Mario Carneiro (Jun 23 2019 at 06:24): you can use ulift bool #### 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. #### 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. #### 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? #### Mario Carneiro (Jun 23 2019 at 06:42): Why does thing still take two universe args? #### Kevin Buzzard (Jun 23 2019 at 06:42): I'm scared Mario #### Mario Carneiro (Jun 23 2019 at 06:43): I'm still not clear on exactly what the goal is #### Kevin Buzzard (Jun 23 2019 at 06:43): I am not sure that sets are enough for glueing #### Mario Carneiro (Jun 23 2019 at 06:43): You aren't using sets #### Mario Carneiro (Jun 23 2019 at 06:43): I managed to prove that sheaf has a comap operation, will show #### Kevin Buzzard (Jun 23 2019 at 06:43): I'll formalise the thing I'm not sure whether to believe. #### Mario Carneiro (Jun 23 2019 at 06:44): https://gist.github.com/digama0/2ee44987e8613b41c24536ddcde86d35 #### Mario Carneiro (Jun 23 2019 at 06:45): That's equivalent to the theorem that you can make a sheaf on a subset #### Kevin Buzzard (Jun 23 2019 at 06:49): infixr  ↪⊓⨆ :25 := semilattice_inf_lub_emb  I'm liking that. #### 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. #### Mario Carneiro (Jun 23 2019 at 06:52): That's the goal #### 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... #### 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. #### 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. #### Kevin Buzzard (Jun 23 2019 at 07:10): But is it a presheaf over a complete lattice? #### 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. #### 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 #### Johan Commelin (Jun 23 2019 at 07:13): You can still just work over complete lattices. #### 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. #### Johan Commelin (Jun 23 2019 at 07:14): The definition of presheaf and functor or defeq up to eta for records... #### 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. #### Kevin Buzzard (Jun 23 2019 at 07:25): You have to "sheafify". #### Kevin Buzzard (Jun 23 2019 at 07:26): Apply the adjoint functor to the forgetful functor from sheaves to presheaves. #### 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 #### Mario Carneiro (Jun 23 2019 at 07:27): I don't know why presheaf is stated using a Top argument #### Kevin Buzzard (Jun 23 2019 at 07:27): You can't make sheaves on an arbitrary category. #### Kevin Buzzard (Jun 23 2019 at 07:28): You need a notion of covering. This is what a site is. #### Mario Carneiro (Jun 23 2019 at 07:28): okay, how's that work? #### Kevin Buzzard (Jun 23 2019 at 07:28): https://en.wikipedia.org/wiki/Grothendieck_topology #### Mario Carneiro (Jun 23 2019 at 07:29): Wait, this is about the domain category #### Kevin Buzzard (Jun 23 2019 at 07:29): If you work with categories then that is the correct thing to use. #### Mario Carneiro (Jun 23 2019 at 07:29): mathlib presheaves are on top spaces #### 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 #### Mario Carneiro (Jun 23 2019 at 07:29): The category here is the target, replacing Type #### 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. #### Mario Carneiro (Jun 23 2019 at 07:30): I don't #### Kevin Buzzard (Jun 23 2019 at 07:30): No? #### Mario Carneiro (Jun 23 2019 at 07:30): I'm just considering top spaces for now, because that's what mathlib presheaves are #### Mario Carneiro (Jun 23 2019 at 07:30): I just want to know why it's bundled #### Mario Carneiro (Jun 23 2019 at 07:31): mathlib presheaves could also be generalized to preorder categories, but that's work for another day #### Mario Carneiro (Jun 23 2019 at 07:31): or general categories, and then you have this site business #### 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? #### Kevin Buzzard (Jun 23 2019 at 07:32): It might be best to do presheaf_on_opens first #### Mario Carneiro (Jun 23 2019 at 07:32): sheaf_on_opens U := sheaf {V // V <= U} #### Mario Carneiro (Jun 23 2019 at 07:33): or more generally a sheaf on some object isomorphic to that #### Kevin Buzzard (Jun 23 2019 at 07:33): So you really want to carry the subtype around? #### Mario Carneiro (Jun 23 2019 at 07:33): That's why I defined comap, because subtype.val is an inf_sup_emb #### 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 #### 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. #### 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. #### 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} #### 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 #### 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 #### 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  #### Mario Carneiro (Jun 23 2019 at 07:40): they are too pointed #### 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}  #### 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}  #### Mario Carneiro (Jun 23 2019 at 07:51): there's that too #### Kevin Buzzard (Jun 23 2019 at 07:54): instance {α : Type u} [semilattice_inf α] (U : α) : semilattice_inf {V // V ≤ U} := sorry  :-( #### Mario Carneiro (Jun 23 2019 at 07:56): it's not hard to prove #### Kevin Buzzard (Jun 23 2019 at 07:57): I just thought it would happen by magic #### 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. #### Kevin Buzzard (Jun 23 2019 at 07:57): instance {α : Type u} [semilattice_inf α] (U : α) : has_inf {V // V ≤ U} := by apply_instance -- fails  #### Kevin Buzzard (Jun 23 2019 at 07:58): but semilattice_inf extends has_inf #### Mario Carneiro (Jun 23 2019 at 08:04): you have to define that too #### 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  #### 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 #### 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.

#### Kevin Buzzard (Jun 23 2019 at 09:38):

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

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

#### Kevin Buzzard (Jun 23 2019 at 09:39):

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

#### Kevin Buzzard (Jun 23 2019 at 09:39):

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

#### Mario Carneiro (Jun 23 2019 at 09:40):

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

#### Kevin Buzzard (Jun 23 2019 at 09:40):

I was having trouble getting this to work.

#### Kevin Buzzard (Jun 23 2019 at 09:40):

Which lines do you think I can delete?

#### Mario Carneiro (Jun 23 2019 at 09:40):

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

#### Mario Carneiro (Jun 23 2019 at 09:41):

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

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

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

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


Thanks.

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

#### Kevin Buzzard (Jun 23 2019 at 10:14):

Do we have frames in mathlib?

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

can we glue sheaves on sites?

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

We can't glue anything on anything right now

#### Kevin Buzzard (Jun 23 2019 at 10:18):

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

#### Kevin Buzzard (Jun 23 2019 at 10:18):

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

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

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

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

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

#### Mario Carneiro (Jun 23 2019 at 12:52):

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

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


#### Kenny Lau (Jun 23 2019 at 13:25):

I have |no idea| what I was doing

#### Kenny Lau (Jun 23 2019 at 13:31):

I should extract defs/lemmas

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

#### Kevin Buzzard (Jun 23 2019 at 18:11):

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

#### Kevin Buzzard (Jun 23 2019 at 18:12):

That's quite some calc by the way!

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

#### Kevin Buzzard (Jun 24 2019 at 08:42):

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

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

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

#### Johan Commelin (Jun 24 2019 at 09:06):

@Patrick Massot I'm sad to hear that story

#### Kevin Buzzard (Jun 24 2019 at 09:07):

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

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

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

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

#### Kevin Buzzard (Jun 24 2019 at 09:11):

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

#### Mario Carneiro (Jun 24 2019 at 09:11):

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

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

#### Kevin Buzzard (Jun 24 2019 at 09:13):

The moment homs are not Props, basically.

right

#### Mario Carneiro (Jun 24 2019 at 09:13):

Your glue and universal_property theorems look like that

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

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

#### Mario Carneiro (Jun 24 2019 at 09:15):

try it both ways and let the best infrastructure win

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

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

#### Scott Morrison (Jun 24 2019 at 10:40):

The file we wrote that afternoon is here.

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

#### Kevin Buzzard (Jun 24 2019 at 11:30):

This deserves a new thread really.

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

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

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

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

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

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

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

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

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

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

#### Mario Carneiro (Jun 24 2019 at 11:51):

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Johan Commelin (Jun 25 2019 at 07:56):

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

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

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

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

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

#### Scott Morrison (Jun 25 2019 at 08:09):

No, no universe variables. :-)

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

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

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

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

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

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

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

#### Scott Morrison (Jun 25 2019 at 08:17):

That one is easy to fix. :-)

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

#### 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 φ }  #### Kenny Lau (Jun 25 2019 at 08:32): and I never used the cocycle conditions #### Kevin Buzzard (Jun 25 2019 at 08:37): Maybe you need them to prove the universal property? #### Kevin Buzzard (Jun 25 2019 at 08:37): This is not proved even for presheaves. #### 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. #### Kenny Lau (Jun 25 2019 at 08:41): that is indeed what you gave me #### 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. #### 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. #### Kevin Buzzard (Jun 25 2019 at 08:43): So maybe the universal property isn't even true if you glue presheaves naively. #### 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 #### 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. #### Patrick Massot (Jun 25 2019 at 09:42): You'll see subtype uniform_continuous appearing everywhere #### 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] }


it's computable!

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

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

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

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

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

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

#### Mario Carneiro (Jun 25 2019 at 10:51):

use max u v in place of u

#### Mario Carneiro (Jun 25 2019 at 10:51):

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

#### Kevin Buzzard (Jun 25 2019 at 10:52):

Of course they don't.

#### Kevin Buzzard (Jun 25 2019 at 10:52):

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

#### Mario Carneiro (Jun 25 2019 at 10:52):

so... not really one universe then

#### Kevin Buzzard (Jun 25 2019 at 10:52):

We have sets and classes. Sheaves are a class.

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

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

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

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

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

#### Mario Carneiro (Jun 25 2019 at 10:57):

unless you want two completely separate but parallel theories

#### Kevin Buzzard (Jun 25 2019 at 10:57):

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

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

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

#### Mario Carneiro (Jun 25 2019 at 11:00):

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

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

#### Mario Carneiro (Jun 25 2019 at 11:14):

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

#### Mario Carneiro (Jun 25 2019 at 11:16):

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

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

#### Kevin Buzzard (Jun 25 2019 at 11:18):

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

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

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

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

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

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

#### Mario Carneiro (Jun 25 2019 at 11:23):

and there are more operations with notation

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

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

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

#### Kevin Buzzard (Jun 25 2019 at 11:37):

Does anyone here understand the pro-etale site?

#### Kevin Buzzard (Jun 25 2019 at 11:37):

[this a new Scholze thing]

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

Yes I guess so.

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

#### Kevin Buzzard (Jun 25 2019 at 11:39):

Aah that's not the point.

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

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

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

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

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

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

#### Kenny Lau (Jun 25 2019 at 18:59):

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

#### Johan Commelin (Jun 25 2019 at 19:02):

We already have stalks in mathlib.

where?

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

#### Johan Commelin (Jun 25 2019 at 19:05):

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

#### Kenny Lau (Jun 25 2019 at 19:06):

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

#### Johan Commelin (Jun 25 2019 at 19:08):

What do you mean?

#### Kenny Lau (Jun 25 2019 at 19:09):

never mind, I figured it out

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

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

#### Reid Barton (Jun 26 2019 at 02:41):

Hmm, that does sound plausible

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

#### Kevin Buzzard (Jul 02 2019 at 06:32):

How to formalise it

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

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

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

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

#### Kevin Buzzard (Jul 02 2019 at 16:52):

It's the fpqc coverings that scare me.

#### Kenny Lau (Jul 04 2019 at 15:39):

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

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