sheaves and sites

Stream: maths

[Johan Commelin]

Lol, I'm quite sure that the definition of coverage is wrong. I should demand that the collection of covers contains the singletons {id : U ⟶ U} for every U : X.

[Johan Commelin]

If I'm right, this is also missing on nLab.

[Johan Commelin]

I retract this. There is a comment on nLab pointing out that you don't need to demand that identity morphisms cover. It doesn't change your category of sheaves.

[Kenny Lau]

did you say nlab...

[Kenny Lau]

man you've gone too far...

[Johan Commelin]

opens X is now a site!
https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L245

[Johan Commelin]

This is one of the ugliest proofs I've written in a long time.

[Johan Commelin]

Also, I would like to get some feedback on the definition of the covers for opens X. This is the actual data that goes into a site. The rest doesn't matter, because it's only proofs. (They should of course be faster then what I have now.)
Basically, there are at least three (equivalent) ways to specify the data of covers:
1) covers := λ U Us, U.val = ⨆u∈Us, (u:over _).left.val — take the union in set X
2) covers := λ U Us, U = ⨆u∈Us, (u:over _).left — take the "union" in opens X
3) covers := λ U Us, U = limits.sigma (λ u∈Us, (u:over _)) — take the "union" as a colimit in the category over U
Do people already see reasons to choose/discard one of these options?

[Johan Commelin]

I currently have option (2). But maybe option (3) is actually better, even though it is high-brow; because it would tie in better to all the facts that we (will) have about functors/limits/etc...

[Reid Barton]

I wonder whether using actual families (instead of set everywhere) would make your life easier

[Reid Barton]

Maybe this isn't actually causing any difficulty

[Johan Commelin]

Hmm, I had that before, and it actually became harder... also, you run into more universe issues, I think.

[Johan Commelin]

sheaf.lean is now sorry-free. In particular, I have defined the site on a basis of a topology.

[Kevin Buzzard]

@Ramon Fernandez Mir you might be interested in this. @Johan Commelin where is this work? Is it on github?

[Johan Commelin]

My todo-list:

• Clean up the proofs
• Prove that continuous functions to some space T form a sheaf on X
• Generalise to sheaves with values in C (e.g., C = CommRing or Ab)
• Define stalks
• Build an API around everything

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean

[Johan Commelin]

@Scott Morrison Would you mind testing your most powerful version of obviously on (parts) of the proofs at the bottom of sheaf.lean? As you can see I'm mostly doing what tidy would do, except that I sprinkle an occasional rw into the mix.

[Johan Commelin]

(If you have time for this...)

[Scott Morrison]

Hi @Johan Commelin , we should combine/adapt the stuff I wrote on bundled presheaves at some point, with a category structure based on:

structure Presheaf :=
(X : Top.{v})
(𝒪 : (opens X)ᵒᵖ ⥤ C)

structure Presheaf_hom (F G : Presheaf.{u v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((opens.map f).op ⋙ F.𝒪))

[Scott Morrison]

Am I right that you haven't got this yet?

[Scott Morrison]

I think most of the other stuff I'd done previously on sheaves is all obsolete by your recent progress.

[Johan Commelin]

(I don't have stalks yet :lol:)

[Johan Commelin]

Why would you want the bundled presheaves?

[Johan Commelin]

To define morphisms of ringed spaces?

[Johan Commelin]

I think I would first do that unbundled.

[Johan Commelin]

Hmmm, I just realised that I don't even know what it means to be a sheaf with values in C when working on an arbitrary site.
I can make sense of it

• if the site has pullbacks, or
• if C is concrete in the sense that it comes with a forgetful functor to Type.

[Johan Commelin]

@Mario Carneiro Do you have any tips on what the right "go-for-it" route would be in this case?

[Johan Commelin]

We want sheaves of rings.
There are 23 definitions that are all math-equivalent.

[Harry Gindi]

There's no way to do it as a ring object in sheaves?

[Johan Commelin]

That is one of the 23 possibilities (-;

[Johan Commelin]

But then you need to connect it to all the useful things that we know already about rings.

[Johan Commelin]

This is math-trivial, of course

[Harry Gindi]

A lot of them aren't true for sheafy rings

[Johan Commelin]

But now you actually need to justify it to a computer.

[Johan Commelin]

Sure, but there is an extremely large bunch of trivialities that are true

[Harry Gindi]

Is there any way to work with sheaves directly as nonclassical types?

[Harry Gindi]

so that all of the theorems for rings that don't use classical assertions hold?

[Johan Commelin]

What exactly do you mean?

[Johan Commelin]

Working internally in some topos?

[Johan Commelin]

Or you want to lift all constructive results into every topos?

[Johan Commelin]

Nothing like that currently exists. And pulling it off would be quite a non-trivial project.

[Harry Gindi]

Yeah, I agree

[Johan Commelin]

@Scott Morrison Do you think the current definition of sheaf is ok?

def sheaf (X : Type u) [𝒳 : site.{u} X] :=
{ F : presheaf X (Type u) // nonempty (site.sheaf_condition F) }

I need the ugly nonempty because is.iso is not a Prop. What is the correct Lean-idiom for this?

[Scott Morrison]

Why not just use a sigma type?

[Scott Morrison]

The category of presheaves will not care about the evidence you provide

[Johan Commelin]

I want to use full_subcategory

[Johan Commelin]

But maybe I shouldn't?

[Scott Morrison]

so use sigma_category, which I think hasn't landed in mathlib

[Scott Morrison]

but is the same idea, it just ignores the extra data

[Scott Morrison]

If you think about it, this is a perfectly sensible thing to do categorically:

[Johan Commelin]

Ok... I see. Which branch do I need to merge into sheaf to do that?

[Johan Commelin]

Yeah, the idea is obvious. I just didn't want to roll my own tooling.

[Scott Morrison]

you can have something that acts as a full subcategory, but actually makes many copies of the objects that you're keeping, according to the different ways to witness that you want them ...

[Johan Commelin]

/me is lazy...

[Scott Morrison]

I think it's only in lean-category-theory

[Scott Morrison]

so it's not just merging a branch

[Johan Commelin]

Aaah, then I'll leave a TODO above the current definition.

[Harry Gindi]

Is there documentation for what a sigma-category is?

[Scott Morrison]

Copy and paste

instance sigma_category (Z : C → Type w₁) : category.{(max u₁ w₁) v₁} (Σ X : C, Z X) :=
{ hom  := λ X Y, X.1 ⟶ Y.1,
  id   := λ X, 𝟙 X.1,
  comp := λ _ _ _ f g, f ≫ g }

def sigma_category_inclusion (Z : C → Type u₁) : (Σ X : C, Z X) ⥤ C :=
{ obj := λ X, X.1,
  map' := λ _ _ f, f }

instance full_σ        (Z : C → Type u₁) : full    (sigma_category_inclusion Z)    := by obviously
instance faithful_σ    (Z : C → Type u₁) : faithful (sigma_category_inclusion Z)   := by obviously

[Scott Morrison]

into full_subcategory.lean?

[Harry Gindi]

does it have a non-type-theoretic analogue?

[Johan Commelin]

Sure, but I don't know if it actually occurs.

[Scott Morrison]

Sure. Say you have a set of objects C, and a function f : C \to Set. Make a new category with objects (X, Y), where Y is in f(X), and whose morphisms (X, Y) to (X', Y') are just the C-morphisms from X to X'.

[Johan Commelin]

It would be like taking the category of groups with all functions as morphisms

[Scott Morrison]

Does it have a name?

[Scott Morrison]

It just makes f(X) many copies of the object X.

[Harry Gindi]

it looks like it's related to the 'anafunctor' version of a subcategory?

[Johan Commelin]

@Harry Gindi Here is a math question that I don't know the answer to. In what generality do people speak of sheaves on a site $X$ with values in a category $C$?
What assumptions do I need to make on $X$ and/or $C$? Is there some grand theory that unifies everything?

[Harry Gindi]

people sometimes say "sheaves of X" in all kinds of cases, but it only makes sense when X is a subcategory of algebras for some algebraic theory rel set

[Johan Commelin]

Well, if the site $X$ has pullbacks, then I guess the sheaf condition makes sense in every category $C$ with equalizers, right?

[Harry Gindi]

yes, but it is usually the wrong thing

[Johan Commelin]

Ok, so it works but is useless.

[Harry Gindi]

I think so, yes

[Johan Commelin]

Ok, I'll have to think a bit about how to move this forward. I'm not sure if I'm ready for defining all the stuff related to algebraic theories.

[Harry Gindi]

It might make more sense if you could relativize algebraic stuff to like parameterized types?

[Harry Gindi]

I don't know, it's really alien to me

[Harry Gindi]

probably the easiest way is as you said

[Harry Gindi]

when the category is concrete, being a sheaf with values in C is the same thing as asking that the underlying sheaf of sets is a sheaf

[Harry Gindi]

I don't know how well that works with e.g. a sheaf of complexes

[Harry Gindi]

which is like the most important application of sheafy stuff in alg. geom, I think

[Scott Morrison]

You have to be pretty careful with this statement. It's not just "concrete" (e.g. topological rings have a faithful functor to Set) You also need that the forgetful functor is continuous and reflects isos.

[Scott Morrison]

At some point I wrote down the statement, but never attempted to prove it:

variables {V : Type (u+1)} [𝒱 : large_category V] [has_products.{u+1 u} V] (ℱ : V ⥤ (Type u))
          [faithful ℱ] [category_theory.limits.preserves_limits ℱ] [reflects_isos ℱ]
include 𝒱

-- This is a good project!
def sheaf.of_sheaf_of_types
  (presheaf : (opens X)ᵒᵖ ⥤ V)
  (underlying_is_sheaf : is_sheaf (presheaf ⋙ ℱ)) : is_sheaf presheaf := sorry

[Scott Morrison]

(This won't be compatible with Johan's version of presheaves and sheaves, of course.)

[Harry Gindi]

I wonder if a good way to do this is with internal objects in a topos after all

[Harry Gindi]

then you could try to follow Hakim's thesis

[Johan Commelin]

I challenge you to try it :smiley:

[Harry Gindi]

I don't understand how you can say something like categories of nonclassical types satisfyinf Giraud's axioms are categories of sheaves on a site

[Johan Commelin]

What do you mean?

[Harry Gindi]

like, we might want to work internally to some Grothendieck topos

[Harry Gindi]

and the objects there would hopefully be of type "type"

[Johan Commelin]

Sure. And Type is equivalent to sheaves on unit

[Johan Commelin]

No, for an arbitrary topos the type of the objects wouldn't be Type

[Johan Commelin]

They would be of type X, where X is your topos.

[Harry Gindi]

then how can you transfer results from type type to type sheafy type

[Johan Commelin]

And so you have to develop all of type theory internal to topoi. And this hasn't been done yet in Lean. And I don't think it has been done in any theorem prover.

[Johan Commelin]

To do that "transfer" you would have to build quite a bit of machinery.

[Harry Gindi]

exactly, it looks daunting

[Johan Commelin]

Very daunting

[Johan Commelin]

It would take Mario a whole summer, I'm afraid.

[Harry Gindi]

one way to do it, maybe, would be to try to prove that any nonclassical theorem in type type holds when you substitute type X for type type when X is a topos?

[Harry Gindi]

it's not easy

[Harry Gindi]

It would probably be highly rewarding in terms of work saved

[Harry Gindi]

I should probably look in e.g. the elephant to see if there is a statement of such a theorem

[Mario Carneiro]

I'm afraid I have no idea about the math in this area

[Mario Carneiro]

I'm not sure how much of it is important to the modeling question

[Mario Carneiro]

Hmmm, I just realised that I don't even know what it means to be a sheaf with values in C when working on an arbitrary site.
I can make sense of it
* if the site has pullbacks, or
* if C is concrete in the sense that it comes with a forgetful functor to Type.

Are these two definitions related to each other? Harry says this is not the right notion in some categories?

[Mario Carneiro]

If there is a reasonable categorical interpretation of the sheaf operations or what not then that seems like a good place to start

[Mario Carneiro]

but it sounds like a "sheaf of rings" is not a sheaf over Ring as I would hope, but rather a ring object in sheaves... unfortunately I don't know any way of relating rings and ring objects in a suitably algorithmic way

[Mario Carneiro]

that is, you can define a group object, ring object etc but nothing about these definitions will connect them to the usual algebraic classes, and there won't be a general procedure for inputting a universal algebra and getting a predicate in category theory language

[Mario Carneiro]

and "internalization" is not something we can currently do in a nice way, although maybe a tactic could do it in the future

[Johan Commelin]

@Mario Carneiro Thanks for your input. I think Harry is saying that it would be best to go for the option with concrete categories, and Scott already gave a mockup of the statement.

[Johan Commelin]

You are right that a sheaf of rings is a ring object in sheaves. (At least that is one way to define it.)

[Harry Gindi]

I asked a colleague of mine who specializes in topos theory (and has lots of experience with Lean, but the HOTT branch)

[Harry Gindi]

oh yeah, he's here, Jonas

[Harry Gindi]

@Jonas Frey

[Johan Commelin]

I imagine that a bunch of these problems would go away when using HoTT + univalence

[Harry Gindi]

@Mario Carneiro I was saying that the notion of a sheaf with values in a category that isn't 'algebraic' in some sense is bad

[Mario Carneiro]

so what does "algebraic" mean here?

[Harry Gindi]

admits a finite limit sketch over set, I believe

[Mario Carneiro]

like what are some simple examples?

[Harry Gindi]

sheaves of categories are bad, for example

[Mario Carneiro]

I'm not really sure what the applications are here, what kinds of sheaves are good?

[Harry Gindi]

the right notion for a sheaf of categories has additional coherence conditions (cocycle conditions) that make them stacks

[Mario Carneiro]

but I presume these don't come up in the usual cases for some reason?

[Harry Gindi]

good categories for sheaves: groups, rings, abgroups, things of that nature

[Harry Gindi]

yeah, basically

[Mario Carneiro]

So is the "data" of a sheaf all present in an arbitrary category?

[Mario Carneiro]

or does pullbacks suffice?

[Mario Carneiro]

and somehow in a "good" category these operations have additional properties that make it work

[Harry Gindi]

(deleted)

[Harry Gindi]

sorry, all products

[Harry Gindi]

because you can have infinite covering families

[Mario Carneiro]

I think the easy route would be to define what a sheaf is in an arbitrary category with the constructions needed in the definition itself, and then add appropriate regularity conditions for the theorems (or just prove the theorems in particular categories when needed)

[Mario Carneiro]

I would imagine that it will be easy to retrofit the theorems with more generality as needed

[Harry Gindi]

Scott's version works better than that

[Harry Gindi]

it hits all of the ones we care about

[Mario Carneiro]

I'm not sure how well "concrete categories" in the literal sense of functors to Type work in lean

[Mario Carneiro]

Scott can say better than me

[Harry Gindi]

the key feature of sheaves and presheaves is exactly that they are set-valued and the sheaf condition says something about sets

[Harry Gindi]

having a continuous conservative functor to sets is always satisfied when the category is monadic over sets

[Kevin Buzzard]

In the perfectoid project we need sheaves of topological rings

[Harry Gindi]

hmm, how are those even defined?

[Harry Gindi]

that was exactly the example Scott said would be problematic (topological groups)

[Kevin Buzzard]

well we only need them on topological spaces, so I think there are no technical issues...

[Harry Gindi]

Are they pro-rings like completions?

[Harry Gindi]

Can I see where these are defined in ordinary mathematical language?

[Kevin Buzzard]

Actually there might be some topological issue. Wait a minute, I'll dig up a reference

[Kevin Buzzard]

https://www2.math.uni-paderborn.de/fileadmin/Mathematik/People/wedhorn/Lehre/AdicSpaces.pdf remark 8.19 on p80

[Kevin Buzzard]

The map from F(U) to the stuff in prod_i F(U_i) which agree on overlaps needs to be a homeo rather than just continuous

[Kevin Buzzard]

I think that this is probably exactly the sheaf axiom for top rings

[Harry Gindi]

Yeah, I think you could get away with this because they're adic rings

[Kevin Buzzard]

I am not sure this has anything to do with it

[Kevin Buzzard]

I think that the point is that to check that a presheaf of top rings is a sheaf, it does not suffice to check that the underlying presheaf of rings is a sheaf

[Kevin Buzzard]

there is epsilon more to it than this.

[Harry Gindi]

well, continuous maps between adic rings are the natural transformations between pro-objects

[Kevin Buzzard]

These rings are not adic rings in general

[Harry Gindi]

ah

[Kevin Buzzard]

They are what used to be called "f-adic", which is _not_ "adic + ...", it's "has a subring which is adic + ..."

[Harry Gindi]

mhm

[Kevin Buzzard]

They're now called Huber rings

[Kevin Buzzard]

(terminology due to Scholze)

[Mario Carneiro]

When I said concrete categories in the literal sense I was comparing to categories that are built on actual sets and functions

[Harry Gindi]

yeah, this looks like a special situation that isn't usually covered in the classical theory, I think

[Mario Carneiro]

in which case the forgetful functor is implicit

[Mario Carneiro]

there is quite a lot you can do with concrete categories built like this

[Harry Gindi]

in that case, Kevin, maybe the answer is to do a common generalization that covers the usual situation and the one for perfectoid spaces.

[Harry Gindi]

There are also simplicial sheaves, which have a separate homotopy-theoretic component

[Harry Gindi]

but that way lies madness

[Harry Gindi]

and you'd end up trying to do everything in this article: https://ncatlab.org/nlab/show/model+structure+on+simplicial+presheaves#injectiveprojective__localglobal__presheavessheaves

[Johan Commelin]

@Mario Carneiro I hope the following code is parseable

T : Top,
U : opens X,
Us : covering_family U,
this : Π (u : over U), u ∈ Us → (opens.to_Top.obj (u.left) ⟶ T)
⊢ opens.to_Top.obj (⨆ (u : over U) (H : u ∈ Us), u.left) ⟶ T

Do you know if we have any stuff in topology that would help here?

[Johan Commelin]

What this is saying is: I have a bunch of functions to T defined on us that cover U. Now I want to build a function U to T.

[Johan Commelin]

Of course we need that they agree on overlaps. This is hidden in my context, but it looks ugly, so I didn't paste it.

[Johan Commelin]

Ok, so here is a more precise question: how do I check continuity locally?

[Mario Carneiro]

as with opens, I think you want a covering_family U to be a type

[Harry Gindi]

Can sieves make life easier?

[Harry Gindi]

because then you might just prove that every covering family determines a sieve

[Mario Carneiro]

why do sheaf and sieve and stack and site all sound so similar? the alliteration is killing me

[Johan Commelin]

because then you might just prove that every covering family determines a sieve

I am already using sieves.

[Harry Gindi]

ah, I see, that's good. Much easier to state the sheaf condition that way!

[Johan Commelin]

Mario, I was quite happy with covering_family being a set. But maybe it should be a type.

[Johan Commelin]

ah, I see, that's good. Much easier to state the sheaf condition that way!

Sure, but now I need to actually prove that something is a sheaf :scream:

[Mario Carneiro]

that statement parses, but it isn't provable without stuff about compatibility

[Harry Gindi]

test case: Every representable is a sheaf wrt the topology generated by universal epimorphic families?

[Johan Commelin]

@Mario Carneiro Hence my more precise question...

[Johan Commelin]

@Harry Gindi Indeed. I'm proving that continuous functions X → T form a sheaf on X, for a given T.

[Johan Commelin]

So it is not as general as your test case.

[Harry Gindi]

I guess then you'd first have to define universal epimorphic families :mischievous:

[Johan Commelin]

Feel free to join in :joy_cat:

[Harry Gindi]

Talk is cheap, that's why I do it so often

[Kenny Lau]

let's just define the spectrum of a ring fist

[Kenny Lau]

(sorry, I'm a more concrete guy)

[Johan Commelin]

I'm working on it Kenny. I'm trying to define ringed spaces.

[Harry Gindi]

Hom_CRing(R, -): Ring->Set; where's my big novelty check

[Johan Commelin]

Harry, one of the first things you learn when working with provers is that there are lots of definitions that are math-trivially equivalent. But proving that they are equivalent in Lean is often very hard.

[Johan Commelin]

I'm quite sure that there is value in defining a functor from Ring^op to LRS.

[Harry Gindi]

I know, I'm being silly. This definition I just gave is meaningless even outside a theorem prover

[Harry Gindi]

Just saw this on MathOverflow, could be a useful guide: https://rawgit.com/iblech/internal-methods/master/notes.pdf

[Harry Gindi]

especially if you decide to go down the internal logic route

[Reid Barton]

@Johan Commelin, not sure how much progress you made on your gluing continuous functions question, but step 1 is to just construct the glued function even as a function, i.e., disregarding the topology of X, and then check that the glued function actually restricts to the original guys

[Reid Barton]

then step 2 would be to check continuity, possibly you can use continuous_subtype_nhds_cover for this

[Reid Barton]

You might find https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/homotopy_theory/topological_spaces/inter_union.lean a useful guide though there I was only interested in the case of two (closed) subsets

[Johan Commelin]

Ok, thanks for the tips.

[Reid Barton]

Step 1 will require choice

[Johan Commelin]

I'm currently trying to build a function.

[Johan Commelin]

And I haven't come to the point yet where I need choice. But I think I'm close

[Patrick Massot]

I think this was already discussed here, with a student of Kevin

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Topology.20-.20Beginner/near/130051069

[Kevin Buzzard]

@Luca Gerolla wanted to define a continuous function on a closed interval [0,1] by glueing continuous functions on [0,1/2] and [1/2,1]

[Patrick Massot]

exactly

[Patrick Massot]

hopefully this is what I linked to

[Harry Gindi]

I can't get that link to work on mobile

[Johan Commelin]

Thanks @Patrick Massot, your memory is better than mine.

[Reid Barton]

I realize that maybe it's not very obvious what the module I linked to is doing--it's showing that for $A_0$, $A_1$ closed subsets of a space X, there is a pushout square in Top involving $A_0 \cap A_1$, $A_0$, $A_1$, $A_0 \cup A_1$. For open subsets you would use the other lemma from topology I mentioned, and then it's the same as checking the sheaf condition I guess.

[Harry Gindi]

@Reid Barton you have to use AC to construct glued maps?

[Harry Gindi]

that's surprising to me

[Harry Gindi]

or is this "choice" different from the axiom of choice?

[Reid Barton]

You could construct a glued map on the quotient type (the disjoint union of the subsets) modulo (points with the same image in X) without choice

[Reid Barton]

Ah, it is a bit different from the axiom of choice

[Reid Barton]

In Lean, basically, choice = nonconstructive

[Harry Gindi]

so how do intuitionists glue maps?

[Reid Barton]

You need choice to go from "for each x there exists a y such that ..." to a function mapping x to the corresponding y, even if you know that the corresponding y is also unique. So in that sense it's not exactly analogous to the axiom of choice in ZFC

[Reid Barton]

I don't know. I guess you could try to replace "subset of X" by "map to X whose fibers are subsingletons", but I don't know how far you would get with that.

[Johan Commelin]

I think I want my covers to be defined as U = colimit u \in Us. Then this sort of problems would go away.

[Reid Barton]

I have this picture in my mind of $A_0 \times \{0\} \cup (A_0 \cap A_1) \times [0, 1] \cup A_1 \times \{1\}$ projecting to $A_0 \cup A_1 \subset X$, and not admitting a continuous section over $A_0 \cup A_1$. Don't know if it means anything though.

[Mario Carneiro]

I think I gave a proof that gluing in arbitrary topological spaces requires choice using roughly that example

[Reid Barton]

@Mario Carneiro had a nice example arguing that you really need something noncomputable to glue functions which is ... right.

[Mario Carneiro]

where by "choice" I mean unique choice

[Mario Carneiro]

lean doesn't really distinguish between AC, unique choice and LEM

[Mario Carneiro]

they all follow from the same axiom

[Harry Gindi]

Can you glue maps of locales without choice?

[Ramon Fernandez Mir]

I've actually been looking into it. It's in the sheaf branch on the community mathlib.

[Johan Commelin]

So now I have this goal:

(⨆ (u : {x // x ∈ Us}), (u.val).left) = ⨆ (u : over U) (H : u ∈ Us), u.left

@Mario Carneiro will say: "I told you that covering_family U should be a type." But it's not (at the moment). How do I solve silly goals like this?

[Johan Commelin]

@Ramon Fernandez Mir Good to see you!

[Mario Carneiro]

There is a rewrite rule for this

[Johan Commelin]

I want rewrite_search...

[Mario Carneiro]

supr_subtype

[Luca Gerolla]

@Luca Gerolla wanted to define a continuous function on a closed interval [0,1] by glueing continuous functions on [0,1/2] and [1/2,1]

Indeed, I was dealing with continuous functions on two closed sets $V, U$ (where $U, V$ cover the overall domain $X$) agreeing on their intersection $U \cap V$ and I needed to construct a continuous function $X \to Y$. The code (mainly done by Mario and Kevin) is at https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Topology/Material/pasting_lemma.lean.
Although dealing with a general covering I don't know if it can be of any help.

[Kenny Lau]

@Luca Gerolla wrong thread?

[Mario Carneiro]

I don't think so

[Kenny Lau]

what's Luca doing on an nlab thread...

[Johan Commelin]

He's on a thread about gluing functions.

[Kenny Lau]

\cap $\cap$

[Johan Commelin]

His post is about gluing functions.

[Luca Gerolla]

Also continous_if (from mathlib - topology.continuity) turned out very useful when I had just and ite function.
Look forward to seeing the solution to this more general pasting :)

[Johan Commelin]

@Scott Morrison Here is something that I find a bit annoying to do. I'm trying to prove that the following functor preserves colimits:

def to_Top : opens X ⥤ Top :=
{ obj := λ U,
          { α := U.val,
            str := subtype.topological_space },
  map := λ U V i, ⟨λ x, ⟨x.1, (plift.down (ulift.down i)) x.2⟩,
    (embedding.continuous_iff embedding_subtype_val).mpr continuous_subtype_val ⟩ }

Here is what I have so far:

def to_Top.preserves_colimits : preserves_colimits (@to_Top X _) :=
{ preserves := λ J _ K c hc,
  { desc := λ s, _ } }

The local context is now:

X : Type u,
_inst_1 : topological_space X,
J : Type u,
_x : small_category J,
K : J ⥤ opens X,
c : limits.cocone K,
hc : limits.is_colimit c,
s : limits.cocone (K ⋙ to_Top)
⊢ (functor.map_cocone to_Top c).X ⟶ s.X

The annoying thing is the pair c, hc. I would much rather work with hc : has_colimit K and c : colimit K. Because then I can use facts about how this colimit is defined. Of course I can build a unique isomorphism between the c that I got from Lean and the one that I'm interested in. But I wonder if it would make sense to change the setup a bit...

[Johan Commelin]

I've pushed all that I have so far. Now I need to start packing to catch a train.

[Johan Commelin]

If anyone has good ideas, or wants to refactor this, please go ahead!

[Johan Commelin]

I'm just trying to push this category stuff to the limit (no pun intended)

[Reid Barton]

I think we can just add a lemma for that.
You're saying you want to prove: if F : C -> D and C already has_colimits, then to prove F preserves colimits it suffices to consider the ones provided by the has_colimits instance.

[Johan Commelin]

Yes, but why not just always condider the one provided by has_colimit K, where K is a diagram.

[Patrick Massot]

I'm just trying to push this category stuff to the limit (no pun intended)

When we'll have that to_dual tactic, you'll be able to pull this category stuff to the colimit without any extra effort!

[Reid Barton]

Because the concept of preserving colimits doesn't depend on a choice of colimits

[Johan Commelin]

I see... you're probably right. I don't yet fully grasp the details of the API

[Johan Commelin]

But your suggested lemma would also fix this problem.

[Kevin Buzzard]

@Johan Commelin @Kenny Lau -- @Ramon Fernandez Mir asks me exactly what you are going to be doing regarding Spec of a ring. Ramon is supposed to be completely refactoring the scheme project as part of his MSc thesis; I got him to look at locally ringed spaces but now these are done modulo the assertion that the category of rings has all colimits. Then Kenny mentioned Spec -- I think it would just be less nervy for us if we knew exactly what you guys were planning on doing and what Ramon can do (he has written thousands of lines of Coq code but is new to Lean). Currently we need that colimits exist in the category of commutative rings, and that the spectrum of a ring is a locally ringed space (which of course is a lot of work, even though it's in some sense done already). The first step towards this is that the spectrum of a ring has a presheaf of rings on the basis of open sets $D(f)$. Shall I tell him to do this or will someone else do it by the weekend? It would be good if we could work together on this (although of course there is plenty plenty to do -- e.g. this Gamma Spec adjointness is a goal I have in mind for Ramon, something Johan suggested months ago -- and products of schemes is another thing).

[Kevin Buzzard]

Of course I know all of this is already done in the schemes project -- the point is that we want to do it as a test of the category theory stuff; in the past we did it all "by hand".

[Kevin Buzzard]

I think I know how to prove that colimits exist in the category of commutative rings -- can I get Ramon to do this or @Kenny Lau are you likely do just randomly do this at some point in the next few days?

[Kevin Buzzard]

It will be quite a good stress test of Johannes' multivariable polynomial work I think.

[Johan Commelin]

@Kevin Buzzard Yes, collaboration is good. I have no intention to "mow away the grass" before Ramon's feet.
Here is a question for you: do you intend to make things mathlib-ready? Is the endgoal a PR to mathlib?

My goal is to get a theory of sheaves that is ready for the perfectoid project.

[Johan Commelin]

Concerning colimits in CommRing: do all of them exist? Or only the directed ones?

[Kevin Buzzard]

I convinced myself this afternoon that they all existed

[Johan Commelin]

Sheaves of rings seems to be a bit of an issue. I'm not yet sure how to define them. Once we have those, I'll leave it up to Ramon to define LRS. I will not touch Spec or anything close to it (-;

[Reid Barton]

They do all exist

[Johan Commelin]

I do intend to define stalks. So I might get close to LRS...

[Kevin Buzzard]

via some big standard universal construction -- given a diagram in CommRing, let T0 be the polynomial ring over Z with variables the disjoint union of all the rings in the diagram, and then quotient out by the relations making all of the canonical maps ring homs

[Johan Commelin]

I would not mind at all if Ramon works on a branch of community mathlib and regularly pull and pushes to the sheaf branch.

[Kevin Buzzard]

The "bad" news is that this all seems to be some special case of some big theory due to Lawvere and we could spend forever formalising that instead

[Kevin Buzzard]

(existence of limits and colimits in some big gneerality for some algebraic categories or something)

[Johan Commelin]

Right. So we just do rings by hand first. Like you did schemes by hand first. This seems to be what Mario would tell us to do anyway.

[Kevin Buzzard]

Right -- so @Kenny Lau are you happy if @Ramon Fernandez Mir proves existence of colimits in the category of commutative rings?

[Kevin Buzzard]

In a relatively "hands-on" way, not using Lawvere anything

[Johan Commelin]

Be aware that Scott already has some general machinery in this direction. I guess you only need coproducts and coequalisers.

[Kevin Buzzard]

I am not 100% sure whether this makes life any easier in this case

[Kevin Buzzard]

in the sense that now instead of making one gigantic commutative polynomial ring in a huge set of variables and quotienting out by an ideal generated by terms of two types and then proving something about it, you'll have to build two such rings and prove something about each of them.

[Johan Commelin]

It would be useful to know that coproducts are defeq to tensor products, I assume...

[Kevin Buzzard]

funny isn't it. For products and subobjects you feel like you've made progress. But colimits are quotients so it's always going to be a pain I think. I don't even really understand what the coproduct of an arbitrary set of rings looks like -- it seems to be some sort of direct limit of finite tensor products -- but of course we haven't built direct limits yet so there's a danger of going round in circles here.

[Kevin Buzzard]

Here is a question for you: do you intend to make things mathlib-ready? Is the endgoal a PR to mathlib?

I don't even know if Mario would be interested in hosting schemes (and I've not asked) -- my goal is to take the crappy code which I wrote so I could learn how to write Lean code, and replace it with code which is sufficiently respectable to get a publication. I've not thought about mathlib at all.

[Johan Commelin]

I think there are two options:

• either stuff like this goes into mathlib,
• or the Lean community comes up with a good strategy to have decentralised libraries that work together nicely as dependencies of other projects.

[Mario Carneiro]

The construction you sketched is clearly a composition of two constructions, why not formalize that?

[Johan Commelin]

@Mario Carneiro Do you want schemes in mathlib?

[Mario Carneiro]

I want polished code in mathlib

[Johan Commelin]

Do you want polished schemes in mathlib?

[Mario Carneiro]

sure, if that interests yous

[Mario Carneiro]

there seem to be a lot of intermediate steps though

[Johan Commelin]

It interests mes and about 65% of all Field medalists.

[Johan Commelin]

There's a lot of intermediate steps because I'm trying to write reusable code.

[Reid Barton]

I'm not sure which construction Mario is referring to

[Mario Carneiro]

via some big standard universal construction -- given a diagram in CommRing, let T0 be the polynomial ring over Z with variables the disjoint union of all the rings in the diagram, and then quotient out by the relations making all of the canonical maps ring homs

[Mario Carneiro]

we already have the first part, and the second part should generalize to "given a bunch of functions(?) make them all ring homs"

[Scott Morrison]

I think, unfortunately, that eventually we will want to do all the varieties of colimits in CommRing separately.

[Scott Morrison]

We should do the general colimit, we should also do the filtered colimit (which is much easier), we should do coproducts, we should do binary coproducts. General nonsense says you don't need to prove any comparison theorems relating these, happily.

[Scott Morrison]

Later, various bits of general machinery about algebraic categories will give us the filtered colimits "for free"

[Scott Morrison]

but someone should do the construction in CommRing first as a warmup.

[Scott Morrison]

I don't know the Lawvere stuff; maybe later there's some generality that gives us all colimits in CommRing too?

[Kevin Buzzard]

Ok so Ramon and I will take on the task of general colimits. I'm a bit unsure about whether working in this generality will actually cause problems when we want to prove that the stalks for an affine scheme are local, but let's wait and see!

[Scott Morrison]

Are you sure you don't want to do filtered colimits first, @Kevin Buzzard? They are both easier to construct, and more useful! (Because they're all that's needed for stalks, and will make arguments about stalks easier.)

[Kevin Buzzard]

The way Johan or you had set up locally ringed spaces relied on the fact that CommRing had colimits

[Kevin Buzzard]

I don't know what a filtered colimit is. I know what a directed set is. Is it sort-of the same thing?

[Kevin Buzzard]

aah I now know that a filtered colimit is a categorification of a directed set

[Kevin Buzzard]

So I guess I don't know where to stop here. Why not just do colimits over a directed partial order? They are both easier to construct, and more useful! (Because they're all that's needed for stalks, and will make arguments about stalks easier.)

[Kevin Buzzard]

And Kenny did them already :P

[Reid Barton]

Well, filtered is the right level of generality for the fact that you can compute the colimit in Set

[Kevin Buzzard]

but colimits in Set are completely different to colimits in CommRing

[Kevin Buzzard]

or am I misunderstanding? (presumably)

[Reid Barton]

General ones are, but filtered ones are not

[Kevin Buzzard]

Oh I see!

[Scott Morrison]

I will add filtered colimits (in the simplest sense, not Reid's kappa-filtered ones) to the limits branch shortly. (Just the definition!)

[Scott Morrison]

@Johan Commelin, Johannes asked me to rebase the limits branch; prepare for trouble. :-)

[Kevin Buzzard]

So @Ramon Fernandez Mir would be interested in this. People seem to be suggesting that the definition here https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/presheaves/locally_ringed.lean which uses arbitrary colimits is not wise?

[Scott Morrison]

Yes

[Scott Morrison]

That isn't wise. :-)

[Kevin Buzzard]

and instead of stalk_at one should use something else?

[Scott Morrison]

I think stalk_at will be exactly the same

[Scott Morrison]

We'll just change the typeclass provided, from has_colimits to has_filtered_colimits

[Kevin Buzzard]

I see. And that doesn't break anything else?

[Kevin Buzzard]

When teaching is finished I'm going to be cloning this repo finally

[Scott Morrison]

Magic will then notice that the category of open sets containing x is filtered, and so use the has_filtered_colimits instance,

[Kevin Buzzard]

at the minute cloning it would lead me astray

[Scott Morrison]

which will provide an nice construction of the colimit (as a quotient of a disjoint union, just like in Set), rather than the huge one in terms of tensor products.

[Kevin Buzzard]

Would magic work for sheaves on a basis? For sheaves on a site?

[Scott Morrison]

That I don't know.

[Kevin Buzzard]

I had never seen the construction of a colimit in CommRing until today, when I figured it out for myself. I did not use tensor products. What trick did I miss?

[Kevin Buzzard]

I just made a polynomial ring over Z with variables the disjoint union of all the rings in the diagram

[Kevin Buzzard]

and then quotiented

[Kevin Buzzard]

I understand that for two rings a coproduct is the tensor product

[Kevin Buzzard]

but I couldn't see how this generalised to infinitely many rings

[Kevin Buzzard]

it seemed to be a direct limit of tensor produts, but to make direct limits you want to take coproducts again

[Scott Morrison]

oh, okay, maybe I didn't think very hard about the infinite diagram case, either :-)

[Scott Morrison]

(I had never thought about any of this (nor knew what a site was, etc) until Lean came along. :-)

[Reid Barton]

Well... it's the filtered colimit of all the ways to take a coproduct of finitely many of the rings

[Reid Barton]

and filtered colimits are easy

[Kevin Buzzard]

Is there a general story?

[Reid Barton]

That said, the construction you gave is the simplest one and it has essentially nothing to do with rings in particular

[Kevin Buzzard]

Reducing a general colimit to a filtered colimit?

[Kevin Buzzard]

I still don't know whether we should just stick to filtered (0,1)-categories

[Kevin Buzzard]

i.e. directed sets (I should stop looking at nlab)

[Kevin Buzzard]

Oh, Reid's argument perhaps resolves this -- if it works over set then take it

[Reid Barton]

Directed colimits will be somewhat easier notationally and you don't need them unless you want stalks for some site which is not itself a poset. I think.

[Kevin Buzzard]

I think the etale site is the simplest example of this that I know

[Reid Barton]

Er, don't need filtered colimits unless ..., of course.

[Kevin Buzzard]

and next year when we're doing etale cohomology we'll need etale sites

[Reid Barton]

I think it is safe to assume that by the time we want to do etale cohomology we will have filtered colimits of rings

[Reid Barton]

You can actually build filtered colimits from directed ones, so it doesn't lose any great generality to work with directed ones for some purposes

[Kevin Buzzard]

Magic will then notice that the category of open sets containing x is filtered, and so use the has_filtered_colimits instance,

There's something I can't get to add up here. Say there's a has_colimits instance and also a simpler has_filtered_colimits instance. Now let's say I'm trying to take a colimit and it happens to be filtered. If Lean uses the has_colimits instance then the colimit will be constructed in one way, but if Magic notices that the colimit is filtered then it could construct it using the simpler filtered colimit construction. The two constructions will give canonically isomorphic, but probably not defeq, objects, and doesn't this give rise to a diamond?

[Scott Morrison]

I have to admit I don't know how bad a problem this is going to be!

[Reid Barton]

You also don't necessarily have to put your filtered colimits into the type class system. You can just define and use them directly.

[Harry Gindi]

the general statement comes from the theory of locally presentable categories

[Harry Gindi]

every object can be given as a filtered colimit of finite pushouts of compact (i.e. finitely (resp Kappa)-presentable) objects, iirc the statement correctly

[Harry Gindi]

and iirc CRing has only a single generator, Z[x]

[Harry Gindi]

You don't need to work with Lawvere theories to do this stuff, you might be fine doing the locPres machinery and then proving algebraic categories you care about are LocPres

[Harry Gindi]

standard reference is Adamek-Rosicky

[Harry Gindi]

It seems a lot less complicated than doing Lawvere theories generally

[Harry Gindi]

The general argument is useful in other places, iirc. Grothendieck first used this style of argument in the Tohoku paper

[Harry Gindi]

proving that the category of abelian sheaves has enough injectives, but I forget the details

[Johan Commelin]

@Kevin Buzzard Maybe we should change the definition of stalk a tiny little bit, and write filtered_colimit instead of colimit. That would take care of your issue, I think.

[Kevin Buzzard]

This is a diamond-like issue but one level up. With diamonds you might end up with two objects which are equal but the proof isn't rfl. Here the objects are not even equal, merely canonically isomorphic

[Johan Commelin]

I see what you mean. And I think this is showing that the current type class system might not be a good fit for categorical stuff (wait till we want to do higher-categorical stuff...). But maybe we can just ignore the issue for now, and hope that Lean 4 will solve this issue before we hit serious problems.

[Johan Commelin]

This is pretty ugly:

def extend : presheaf X C :=
{ obj := λ U, limit ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F),
  map := λ U V i,
    show (limits.limit (functor.op (comma.fst (full_subcategory_inclusion B) (functor.of_obj U)) ⋙ F) ⟶
        limits.limit (functor.op (comma.fst (full_subcategory_inclusion B) (functor.of_obj V)) ⋙ F)),
    begin
      have foo := limit.pre ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F) (extend.aux i),
      dsimp [extend.aux] at foo,
      convert foo,
      swap 3, assumption
    end }

[Reid Barton]

Why isn't the map field just an application of limit.pre?

[Reid Barton]

what goal is the last line solving?

[Reid Barton]

My guess is that representing slice categories as comma categories is actually not a good idea in Lean, because the isomorphism (punit -> a) = a is not enough of an equality

[Reid Barton]

Did you actually manage to prove the map_id and map_comp fields?

[Johan Commelin]

Not yet, still working on it.

[Johan Commelin]

Note that I'm not taking a slice category, although it almost is.

[Johan Commelin]

This is opens in B that are contained in U, but U is not in B.

[Reid Barton]

Oh, I see

[Reid Barton]

If these are presheaves of sets, then there's an easier way to write the formula

[Reid Barton]

it's the same as the right Kan extension, right?

[Johan Commelin]

Hmmm... I think so.

[Johan Commelin]

If you want to help, please do so.

[Johan Commelin]

Lean is fighting back hard (-;

[Johan Commelin]

Maybe we should do it for a general map between sites, in that case.

[Reid Barton]

If E is the extended presheaf then we should have E(U) = Hom(yU, E) = Hom(R(yU), F) where R is the restriction of a presheaf on C to a presheaf on B

[Reid Barton]

so E is the composition y, then R, then Hom(-, F)

[Reid Barton]

Yes, that might help as well... at least for clarity

[Johan Commelin]

Ok, I think this is a nice way to do it!

[Johan Commelin]

I don't yet see why it is the same thing as in my special case

[Johan Commelin]

Aah, U is the colimit of all the Ui ∈ B that are contained in U. Now pull this through Hom(_, F) and you get a limit.

[Reid Barton]

You might find it useful to borrow https://github.com/leanprover-community/mathlib/blob/adjunctions/category_theory/presheaf.lean#L85

[Reid Barton]

I think you will want to apply it twice

[Reid Barton]

In your setup you have a functor B -> C, right?

[Johan Commelin]

What do you mean?

[Johan Commelin]

B is a basis, and it has an inclusion into opens X.

[Johan Commelin]

I have a presheaf on B

[Reid Barton]

Okay so let's call opens X C for now

[Johan Commelin]

Aaah, C was my category of coefficients so far

[Reid Barton]

ah

[Johan Commelin]

But maybe I should stop worrying about coefficients, and only focus on Type.

[Reid Barton]

Well this formula won't work unless the values are in Type

[Johan Commelin]

Right, so I should forget about C

[Johan Commelin]

And sheaves of rings will require some extra thought

[Reid Barton]

Okay, in that case let me just use the names from the thing I linked above, so you have a functor C -> D

[Reid Barton]

If you apply restricted_yoneda to it, you get a functor D -> Set^C^op

[Reid Barton]

and if you apply restricted_yoneda to that, you get a functor Set^C^op -> Set^D^op

[Reid Barton]

and that should be the right Kan extension along the original functor

[Reid Barton]

the thing I called "Ry" earlier is another, possibly better way to write restricted_yoneda

[Johan Commelin]

Sorry, as student entered my office. So I have to wait a while with this thing.

[Johan Commelin]

@Reid Barton Hmmm... morphisms of sites seem to be non-trivial. I don't think I want to do them now, unless you want to join in. We would need to explain Lean this definition https://ncatlab.org/nlab/show/flat+functor#SiteValuedFunctors

[Reid Barton]

Right... so concretely I guess your actual goal is to show that the extended presheaf is actually a sheaf?

[Reid Barton]

You might want to pick a fact to prove, and work backwards from there

[Reid Barton]

Otherwise you can enter a swamp of things you could formalize and choices of definitions you could make

[Johan Commelin]

Right. I want to get an equivalence of categories between sheaf B and sheaf X. That is a concrete goal that I definitely want to reach.

[Johan Commelin]

@Reid Barton So which approach would you suggest now? Maybe the one with Kan extensions is best? Because it will generalise later on?

[Johan Commelin]

Hmmm, I'm being called for an early dinner. See you later.

[Johan Commelin]

:rolling_on_the_floor_laughing: This error is hilarious:

type mismatch at application
  set.{u} (over.{u u} U)
term
  over.{u u} U
has type
  Type u
but is expected to have type
  Type u

[Johan Commelin]

@Reid Barton How does this look?

def restrict : presheaf X ⥤ category_theory.presheaf B :=
{ obj := λ F, (full_subcategory_inclusion B).op ⋙ F,
  map := λ _ _ f, whisker_left _ f }

def extend : category_theory.presheaf B ⥤ presheaf X :=
{ obj := λ F, yoneda.op ⋙ restrict.op ⋙ yoneda.obj F,
  map := λ F G f, whisker_left _ $ whisker_left _ $ yoneda.map f }

I think you gave a very good suggestion!

[Johan Commelin]

@Reid Barton I think it makes sense to merge your presheaf.lean with parts of my sheaf.lean. What would be the best approach? Should I merge your branch into mine?

[Johan Commelin]

I would like to prove that restrict and extend form an adjunction anyway.

[Reid Barton]

@Johan Commelin Feel free to merge my branch into yours of course, though I will note that I intend to try out a redesign of adjunctions at some point

[Johan Commelin]

I'm not sure if I'm using things in the right way. I'm trying to write

let G1 := (equiv_of_iso D).trans (equiv.subtype_equiv_of_subtype.{(u+1) (u+1)} Eeq),

where D : F.obj ≅ {p // horrible p} is isomorphisms between a type and a subtype in the category Type u which I turn into an equiv.
I then want to replace the horrible right hand side with a subtype of something else, so I thought, lets use transitivity of equiv and feed it Eeq, which is:

Eeq : (limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃
  Π (a : {x // x ∈ c}), F.obj ((a.val).left) :=
  equiv.trans.{u+1 u+1 u+1} (equiv_of_iso.{u} E)
    (equiv.Pi_congr_right.{u u+1 u+1}
       (λ (Ui : {x // x ∈ c}),
          equiv_of_iso.{u}
            (nat_iso.app.{u+1 u+1 u u} (yoneda_lemma.{u u} X) ((Ui.val).left, F) ≪≫
               ulift_trivial.{u} ((evaluation_uncurried.{u u u+1 u} Xᵒᵖ (Type u)).obj ((Ui.val).left, F))))),

The left hand side of Eeq should be exactly the type of the p in {p // horrible p}.

I get the following error:

type mismatch at application
  equiv.subtype_equiv_of_subtype.{u+1 u+1} Eeq
term
  Eeq
has type
  (limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃
    Π (a : {x // x ∈ c}), F.obj ((a.val).left)
but is expected to have type
  (limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃ ?m_1

I have tried looking at universes. I have enable pp.all. And I'm clueless. Any suggestions?

[Kevin Buzzard]

Is it a typeclass issue? That sometimes causes errors that look like that. Lean can't infer a typeclass and so gives up and prints an unhelpful error message

[Kevin Buzzard]

I mean equiv.subtype_equiv_of_subtype -- does it have some secret inputs that it can't find?

[Johan Commelin]

Also, why is p not an explicit argument in

def subtype_equiv_of_subtype {p : α → Prop} : Π (e : α ≃ β), {a : α // p a} ≃ {b : β // p (e.symm b)}
| ⟨f, g, l, r⟩ :=
  ⟨subtype.map f $ assume a ha, show p (g (f a)), by rwa [l],
   subtype.map g $ assume a ha, ha,
   assume p, by simp [map_comp, l.comp_eq_id]; rw [map_id]; refl,
   assume p, by simp [map_comp, r.comp_eq_id]; rw [map_id]; refl⟩

[Johan Commelin]

Well, in general it can't infer that p.

[Kevin Buzzard]

I'm explicitly talking about typeclasses

[Chris Hughes]

What universe is ?m_1 expected to be in?

[Johan Commelin]

Type u

[Mario Carneiro]

I think Johannes has a bad habit of making lots of things implicit that can't be inferred when used directly

[Mario Carneiro]

I guess that p is inferrable if you use it as a rewrite, or apply it to something

[Johan Commelin]

But in my case a smart elaborator should even be able to infer it, because I'm composing with another equiv.

[Johan Commelin]

Can I rewrite along equivs?

[Mario Carneiro]

I think? calc for sure

[Chris Hughes]

Isn't Π (a : {x // x ∈ c}), F.obj ((a.val).left) Type (u + 1). If I'm not mistaken?

[Johan Commelin]

Hmmm, it says rewrite tactic failed, lemma is not an equality nor a iff

[Mario Carneiro]

hm, I guess that is probably a // TODO(Leo) somewhere

[Mario Carneiro]

obviously it's not high on the list of priorities

[Johan Commelin]

The F.obj ((a.val).left) is Type u, and the product is over c : set (over U) where U : X and X : Type u

[Johan Commelin]

I hope that doesn't bump up universes...

[Mario Carneiro]

that sounds fine

[Mario Carneiro]

you can just check, of course

[Chris Hughes]

If F.obj ((a.val).left is Type u, then Π (a : {x // x ∈ c}), F.obj ((a.val).left) is Type (u + 1) right?

[Chris Hughes]

No it isn't

[Mario Carneiro]

another trick you can try is by convert at the type mismatch

[Mario Carneiro]

it should home in on the mismatched part

[Johan Commelin]

How exactly should I do that?

[Mario Carneiro]

something like subtype_equiv_of_subtype (by convert Eeq) or refine subtype_equiv_of_subtype _, convert Eeq

[Johan Commelin]

Cool! That finds the following unsolved goal:

⊢ presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}

[Johan Commelin]

That's progress at least.

[Kevin Buzzard]

I am loving convert. I use it a lot when doing basic UG maths -- "this is basically the answer, now let's see what pieces we have to pick up"

[Johannes Hölzl]

@Johan Commelin rw only work with = (maybe also ==, and <-> only works due to propext). Rewriting with equiv is hard, one needs to prove that the motive (i.e. context in which the right-hand side appears) can be transported along the equiv. Even ignoring dependencies, parametricity is necessary as it shows that there is no choice involved.

[Johan Commelin]

Right. That is about what I expected.

[Johannes Hölzl]

To rewrite along a equiv we could use the param-branch https://github.com/leanprover-community/mathlib/commits/param and transfer.

[Johannes Hölzl]

One example why it is a problem is:

We want to rewrite e : α ≃ β in {a : α // p a}, but what would be the goal? We get something like{b : β // p (f⁻¹ b)}. But in many cases p itself is also parametric, i.e. we have actually {b : β // @p α (f⁻¹ b)} (not really, as p is describing a term and not a constant, but I hope you get the idea) Now when we can try to adopt the structure of p s.t. α is completely replaced by β, and then f isn't occurring anymore

[Johannes Hölzl]

This adoption mechanism is the kind of rewrite transfer is intended to do

[Johannes Hölzl]

and param provides us with the necessary relations

[Johan Commelin]

I see. But I suspect that param isn't yet ready for prime time.

[Patrick Massot]

You need to ask @Cyril Cohen about this

[Cyril Cohen]

@Johannes Hölzl @Johan Commelin @Patrick Massot param is not ready yet, the translation of recursors was not as straightforward as I thought.

[Johan Commelin]

What do you do when Lean doesn't want to plug a morphism in the category C into your contravariant functor F : Cᵒᵖ ⥤ Type u?
You use convert, and let tidy clean up the mess! :tada:

functor.map F (by convert Ui.val.hom; tidy)

[Johan Commelin]

What's up, @Kenny Lau?

[Reid Barton]

Cool! That finds the following unsolved goal:

⊢ presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}

This is probably true by refl

[Johan Commelin]

invalid apply tactic, failed to unify
  presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}
with
  ?m_3 = ?m_3

[Johan Commelin]

instance : has_coproducts.{(u+1) u} (presheaf X) := limits.has_coproducts_of_has_colimits

[Johan Commelin]

So, I changed that instance, and now I get

tactic failed, there are no goals to be solved
state:
no goals

[Johan Commelin]

Aaah, lol, that is because I should now remove the refl.

[Reid Barton]

Oh, I didn't notice "coproducts" rather than "colimits". Still I'm confused. What are the two instances which are not defeq, but equal by tidy?

[Johan Commelin]

No, they aren't equal by tidy either

[Reid Barton]

Or rather, what did you change that instance to?

[Reid Barton]

well, the right hand side of that goal I guess

[Johan Commelin]

Exactly

[Reid Barton]

But I see

instance functor_category_has_coproducts [has_coproducts.{u v} C] : has_coproducts.{(max u v) v} (K ⥤ C) :=
limits.has_coproducts_of_has_colimits

[Reid Barton]

... I'm really confused now

[Reid Barton]

Ohh, maybe I get what is going on. I think all this duplication between colimit classes is biting you

[Reid Barton]

Well, I'm still not sure why that would be a problem either really

[Reid Barton]

But I still think the duplication is silly anyways

[Johan Commelin]

Which duplication do you mean exactly?

[Reid Barton]

Good question

[Reid Barton]

I was thinking of has_colimits_of_shape and has_colimits being unrelated

[Reid Barton]

But now I see there's also has_colimits which is also unrelated

[Reid Barton]

Gah, has_coproducts

[Reid Barton]

Anyways, I'm still confused by the original fact that you replaced an instance by, as far as I can tell, its definition and it changed the behavior of refl

[Johan Commelin]

Well, I didn't even need refl anymore. convert now took care of everything.

[Reid Barton]

because congr, which convert uses, will try closing goals with refl for you

[Johan Commelin]

Currently I'm trying to prove the equivalence of different formulations of the sheaf condition. Math-proof: apply Yoneda; QED. Lean-proof: :scream: :scream: :boom:

[Reid Barton]

by convert x should be the same as by exact x

[Johan Commelin]

which apparently is not the same as x

[Reid Barton]

OK, I got to the same place where you were before changing the instance.

[Reid Barton]

It's kind of hard to understand what's going on because all the has_blah things are classes, which means they aren't printed except with pp.implicit, which also prints a bunch of other stuff I don't care about...

[Reid Barton]

I wish you could jump from names in the goal window to their definitions...

[Johan Commelin]

Right, we should but the "interactive" back in the goal window :grinning:

[Reid Barton]

My conclusion is that I don't know what is wrong exactly, but all these different has_* need to be rethought (probably there should be far fewer of them)

[Reid Barton]

Apparently your instances which were not the same reduce to something like the following

[Reid Barton]

On one side, we have the colimit of a functor on a discrete category defined using the instance that says the category of types has colimits

[Reid Barton]

On the other side, we're doing something like building a colimit cone from a coproduct thing, which in turn is built from the original colimit somehow

[Reid Barton]

both of these constructions being nontrivial

[Reid Barton]

so that they don't just cancel out

[Reid Barton]

I haven't even seen this file limits/products.lean before

[Johan Commelin]

Thanks for looking into this! Apparently it's trickier than I thought...

[Reid Barton]

There are so many instances and it's hard to tell which ones are used where.

[Reid Barton]

for example, functor_category_has_coproducts uses limits.has_coproducts_of_has_colimits which needs a limits.has_colimits_of_shape.{u v} (discrete β) instance. Does it come from has_colimits_of_shape_of_has_coproducts_of_shape or functor_category_has_colimits_of_shape?

[Reid Barton]

either way, it will eventually end up at has_coproducts_of_shape for the original category which comes from has_coproducts_of_shape_of_has_coproducts which uses has_coproducts which comes from an unnamed instance with definition has_coproducts_of_has_colimits which finally comes from the one true has_colimits instance for Type. I think.

[Reid Barton]

So that's how you end up with the has_colimits -> has_coproducts -> has_colimits double translation, which is not refl

[Johan Commelin]

It's really quite stupid, but I only realised yesterday that all the time I've been working with the wrong map f : presheaf X \functor presheaf Y.

[Johan Commelin]

We want something like this:

def map' : presheaf X ⥤ presheaf Y :=
{ obj := λ F,
  { obj := λ V, colimit ((comma.snd.{u u u u} (functor.of_obj V) f).op ⋙ F),
    map := λ V₁ V₂ j, colimit.pre ((comma.snd.{u u u u} (functor.of_obj V₂) f).op ⋙ F) (comma.map_left f $ functor.of_map j).op,
    map_id' := λ V,
    begin
      erw functor.of_map_id,
      erw colimit.pre_map,
      tidy,
    end },
  map := _ }

but I find it impossible to get this sorry-free.

[Reid Barton]

This is what I implemented in the adjunctions branch, I think?

[Johan Commelin]

This is what will give us the pullback of (pre)sheaves.

[Johan Commelin]

Aaah, did you?

[Johan Commelin]

I didn't look far enough, I'm afraid.

[Reid Barton]

I think it is yoneda_extension (F.comp yoneda)?

[Reid Barton]

at least, it seems to involve many of the same ingredients :)

[Johan Commelin]

In which file?

[Reid Barton]

another construction which I am not very happy about, though...

[Reid Barton]

presheaf.lean

[Johan Commelin]

Aaah, I see. Seems pretty non-trivial...

[Johan Commelin]

Also, why do you work with ≃ instead of ≅. Isn't that just as "bad"?

[Reid Barton]

Yeah, I did it in a round-about way, in retrospect

[Reid Barton]

In general I use equiv because it actually has useful lemmas and also it can relate different universes

[Reid Barton]

though I added a couple more lemmas for iso in the limits PR

[Johan Commelin]

Hmm, I feel like we should merge your presheaf.lean and my sheaf.lean. Or at least deduplicate.

[Reid Barton]

I intend to take a second stab at all the adjunctions and presheaf stuff at some point, but I'm not actively working on it at the moment

[Johan Commelin]

Ok, I'll move some stuff from my file to yours. So that sheaf.lean is only about sheaves.

[Johan Commelin]

If you start working on it again, please make sure to take a look at the sheaf branch version of your file.

[Reid Barton]

FWIW, my conclusion from my first attempt was that it's probably better to do all the constructions in a manifestly natural way, like Scott did in yoneda.lean for example, even though the result is probably pretty unreadable. Then you can add a simp lemma that explains what is actually happening on the level of objects

[Reid Barton]

Or at least, don't have a bunch of isomorphisms with the naturality conditions stated separately. That was a big mess

[Johan Commelin]

I see. That's what I've been trying to do. But I also got stuck.

[Johan Commelin]

The problem with doing things in a "manifestly natural way" is that you get sucked into ever deeper/wider/higher abstractions...

[Reid Barton]

it's true

[Reid Barton]

And that's sort of why I backed off from my previous comment. It's not obvious how to do this "category of elements" construction functorially

[Reid Barton]

The key is to somehow give these things usable and complete instances, so that the way to prove things about them is not to dsimp 100 things

[Reid Barton]

and that's where my current version of presheaf.lean sort of fell apart

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/adjunctions/category_theory/presheaf.lean#L310

[Johan Commelin]

@Reid Barton Does this mean that you think we should avoid adjunction.left_adjoint_of_equiv?

[Johan Commelin]

Yuchai! This is now sorry-free: https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/presheaf.lean#L59
But it is slower than slow! Not sure how to speed it up though. I'm chaining a bunch of rewrites. Are there strategies for speeding this up?

[Scott Morrison]

One thing that I find often works is to work out why the erw are necessary. This is sometimes unrewarding, but often it is because hidden inside implicit arguments there are things that should dsimp, but you forgot to write the appropriate rfl lemmas. Sometimes you get really lucky, and after diagnosing a problem like this you can not only change the erw to rw, but even to dsimp!

[Johan Commelin]

I see. (I've stopped using rw, because erw has more powerful magic (-;)

[Johan Commelin]

Is dsimp faster than erw?

[Scott Morrison]

Yes.

[Scott Morrison]

And erw can be slower than rw, in places where either work. (I think?)

[Scott Morrison]

Well, dsimp can be either faster or slower than erw. :-) But _usually_ it seems to be faster to avoid using erw.

[Johan Commelin]

@Scott Morrison Do you think we could have a [derive rfl-lemmas]?

[Scott Morrison]

I've just had a quick look at that proof, Johan, and I don't seem to be able to make much improvement. :-( There does seem to be a small problem changing between colimit and colim.obj.

[Johan Commelin]

So here is what I imagine derive rflsimp (or whatever) should do: it looks at the current definition, and (as far as I thought this through, which is not that far) it does two checks:

• the definition is an "abbreviation" (like def presheaf C := C \functor Type v. In this case it looks up all the rflsimp lemmas that it derived for C \functor D and defines copies in the presheaf namespace.
• the definition X is a structure. In this case it looks up all the fields. For a field foo it checks whether this is a Pi-type (?) and how many arguments the Pi takes. So if foo := λ a b c, bar(a,b,c) then it will create the appropriate simp-lemma (proved by rfl) that

@[simp] lemma X.foo (x : X) (a b c : some_type) :  x.foo a b c = bar(a,b,c) := rfl

Of course I don't know how to write meta-code. And of course this is probably a very simplified picture. But I think something like this should be possible, and I think it would result in three things:

• less boilerplate (especially in the category library!)
• less broken proofs, where tidy doesn't work, because somewhere someone forgot to state the obvious rfl-simp-lemma.
• less wasted time in hunting down the brokenness of the preceding point.

[Johan Commelin]

@Scott Morrison Thanks for looking into speeding things up. I added a rflsimp-lemma for colim.obj. Do you have any clue why the first line in that proof (with the comment) didn't simplify?

[Scott Morrison]

Nope, I couldn't work it out. The next "usual suspect" for simp not working is that the thing that needs to be simped is inside a function that looks superficially dependent but actually isn't when you think about it a bit. simp, which needs to build congruence lemmas to do "rewriting", can't work out what do to, but rw can. This is a "known problem" with simp, apparently.

[Scott Morrison]

You know how to use rewrite_search, don't you? :-)

[Keeley Hoek]

At some point Johan I made a thing which did this
It was a command called rfl_lemma I think. If you have access to rewrite_search you have access to it, too

[Keeley Hoek]

It only worked for structures though

[Johan Commelin]

@Scott Morrison @Keeley Hoek I don't have rewrite_search. Do you think it is ready to be tested by others? If so, what do I need to do to get started?

[Keeley Hoek]

You could always try it out! My understanding is that all you should have to do is add

lean-tidy = {git = "https://github.com/semorrison/lean-tidy", rev = "3a69d6241207f0c0758468dce666858027c54909"}

to your leanpkg.toml and run leanpkg configure. (I'm slightly worried though because lean-tidy obviously imports from mathlib, which you are working on... but I suspect it will work find (I think this is what Scott does to get his proofs using it).

[Keeley Hoek]

Then import tactic.rewrite_search. You can try to discharge goals with the rewrite_search tactic, but make sure you tag lemmas it is allowed to use with @[search]. There is much more complicated stuff you can do (including more specific tagging), but that's a start!

[Johan Commelin]

Thanks for the explanation!

[Scott Morrison]

I've actually never used it inside mathlib, I'm very curious if it works.

[Keeley Hoek]

ooh
Maybe it won't then

[Keeley Hoek]

something about "ambiguous import xxxx"

[Johan Commelin]

How far are we from a merge request of a (preliminary) version of rewrite_search?

[Johan Commelin]

@Keeley Hoek @Scott Morrison I followed the instructions and then ran leanpkg build. I'm getting tons of errors :stuck_out_tongue_wink:

[Keeley Hoek]

:D

[Keeley Hoek]

yeah, sorry
I think what you actually have to do is copy paste the lean-tidy repo over mathlib
but probably don't do that it will mess your history

[Johan Commelin]

@Scott Morrison @Keeley Hoek I can report that adding that Lean does not outright refuse that repo as a dependency of mathlib. However... there's tons and tons of errors. So it's not really usable in a sense.

[Johan Commelin]

After a long period of being distracted by other work, I've returned to the sheaves and sites project. Stuff is now happening on the sheaf-2 branch, which has less dependencies than sheaf.
I am currently struggling with defining a pretty non-constructive map. I have a gadget s which comes with a proof that I can perform a certain construction after some choice, and the result of the construction does not depend on the choice. But how do I actually do this?

def foo (c : covering_family U) (F : presheaf X) :
(matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) :=
λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from
{ val := λ V H,
  begin
    delta matching_sections at s,
    choose Ui H f using H,
    refine F.map _ (s.1 _ H),
  end,
  property := _ }

Here is what my goal window looks like

X : Type u,
_inst_1 : small_category X,
U : X,
c : covering_family U,
F : presheaf X,
V : over U,
s :
  {s // ∀ (Ui : over U) (H : Ui ∈ c) (Uj : over U) (H_1 : Uj ∈ c) (V : over U) (f : V ⟶ Ui) (g : V ⟶ Uj),
     F.map (f.left) (s Ui H) = F.map (g.left) (s Uj H_1)},
Ui : over U,
H : Ui ∈ c,
f : nonempty (V ⟶ Ui)
⊢ Ui.left ⟶ V.left

What I need to do is extract some hom f from V to Ui out of the current f : nonempty (_). I should then be able to close the goal with exact f.left. But I can only eliminate into Prop from nonempty. So how should I set things up?
All of this is at https://github.com/leanprover-community/mathlib/blob/sheaf-2/category_theory/sheaf.lean#L190-L199

[Reid Barton]

Are you going to need to prove the resulting construction is independent of the choice?

[Reid Barton]

The simple answer is to use choice again, in the form of classical.choice

[Reid Barton]

maybe the choose tactic could do this when the final Prop is a nonempty

[Reid Barton]

or you could use that \exists blah, blah, blah, true encoding

[Johan Commelin]

So nonempty blah is not Lean-equivalent to the \exists blah, blah, blah, true encoding?

[Johan Commelin]

The choose tactic doesn't help... :sad:

[Reid Barton]

it's not definitionally equivalent, much as p /\ true isn't definitionally equivalent to p

[Johan Commelin]

nonempty_of_exists is not an iff...

[Reid Barton]

You can just use choice f

[Johan Commelin]

Ok, I'll try that. Too bad that choose f does not work.

[Reid Barton]

Sometimes when there is going to be a lot of "can only eliminate into Prop" nonsense in a proof, I just put an apply choice at the start

[Reid Barton]

or not necessarily at the start of the whole argument, but at the start of some subargument to satisfy some lemma which wants to take an actual map rather than just an existence statement

[Johan Commelin]

Ok, that worked. But I still wonder why choose f didn't work. @Patrick Massot Any ideas why choose doesn't work on nonempty?
Here's the proof that I have now

noncomputable def foo (c : covering_family U) (F : presheaf X) :
(matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) :=
λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from
{ val := λ V H,
  begin
    delta matching_sections at s,
    choose Ui H f using H,
    refine F.map _ (s.1 _ H),
    exact (classical.choice f).left,
  end,
  property := _ }

[Kenny Lau]

because choose is skolemization?

[Johan Commelin]

I don't know what that means.

[Johan Commelin]

I love the marvellous power of the underscore:

noncomputable def foo (c : covering_family U) (F : presheaf X) :
(matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) :=
λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from
{ val := λ V H,
  begin
    choose Ui H f using H,
    refine F.map _ (s.1 _ H),
    exact (classical.choice f).left,
  end,
  property :=
  begin
    intros,
    show (F.map _ ≫ F.map _) _ = (F.map _ ≫ F.map _) _,
    repeat {rw ← F.map_comp},
    exact s.property _ _ _ _ _ (_ ≫ _) (_ ≫ _)
  end }

[Johan Commelin]

I'm hitting a nasty error again (probably I'm being bitten by choice).
Here is the error (code follows below):

type mismatch at application
  ⟨s_val, s_property⟩.val Ui H
term
  H
has type
  Ui_1 ∈ c_1
but is expected to have type
  Ui ∈ c
types contain aliased name(s): Ui U c
remark: the tactic `dedup` can be used to rename aliases

Code:

def quux (c : covering_family U) :
c.matching_sections ≅ c.generate_sieve.val.matching_sections :=
{ hom := foo c,
  inv := bar c,
  hom_inv_id' :=
  begin
    ext1 F,
    ext1 s,
    apply subtype.ext.mpr,
    funext,
    convert s.property _ _ _ _ _ _ (𝟙 _),
    tidy {trace_result := tt}
  end,
  inv_hom_id' :=
  begin
    ext1 F,
    ext1 s,
    apply subtype.ext.mpr,
    funext,
    dsimp [foo, bar],
    convert s.property _ _ _ _ _ _ (𝟙 _), -- This line fails
    tidy {trace_result := tt},
  end }

Context, just before the convert:

X : Type u,
_inst_1 : small_category X,
U : X,
c : covering_family U,
F : presheaf X,
s : (matching_sections ((generate_sieve c).val)).obj F,
V : over U,
H : V ∈ (generate_sieve c).val
⊢ F.map ((classical.choice _).left) (s.val (classical.some H) _) = s.val V H

[Johan Commelin]

@Kevin Buzzard Replying to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/What's.20new.20in.20Lean.20maths.3F/near/156491890 in this thread.
To be precise: I have no trouble at all extending a presheaf from a basis to the whole space. The problem is checking that it sends sheaves to sheaves. The difficulty is probably due to the fact that I do not have a usable API around the sheaf condition.
And I guess my sheaf condition is hard to work with right now because I'm trying to be quite general, doing sheaves on an arbitrary site.

[Kevin Buzzard]

Oh -- the proof involves some argument on stalks which for a general site is complicated? Are there universe issues or do you only work with small sites?

[Kevin Buzzard]

OK so I just spent 2 hours with Ramon going through this proof (sheaf on a basis extends to sheaf on site) again in the case of topological spaces. The ideas are all fresh in my mind at the minute so let me note them down in case there's anything helpful here.

Aah -- I now realise that actually I don't know how you're extending the presheaf at all. The way Ramon and I do it is that given a presheaf $F$ on a basis we can define the stalk $F_x$ at a point $x$ via a direct limit construction, and then we define a presheaf $F^+$ on the space by saying that its values on an open $U$ are a subtype of a big Pi type sending $x\in U$ to an element of the stalk $F_x$; it's the subtype consisting of functions which are locally a section of the presheaf-on-a-basis.

What both he and I did next was then immediately embarked on a proof that if $F$ is a sheaf on a basis then this extension is a sheaf. This gets really hairy. Say I have a bunch of local sections $s_i$ on opens $U_i$, which agree on overlaps. I want to glue them together to get a section $S$ of $F^+$. Well, a section of $F^+$ is just a subtype of a pi type, so we know how to define it. But the technicality is that to define this function $S$ we want to say $S(x)=s_i(x)$ where we choose some $i$ such that $x\in U_i$. As mathematicians we know that $S(x)$ is independent of the choice, but in computer science this is some classical.indefinite_description blah blah noncomputable crap and we're forced to deal with this. Ramon had written 0 API so at the end of it our goals had all these classical.indefinite_description terms in. He was able to battle past the first few, but checking that $S$ restricted to $s_i$ was really difficult, for a reason which I am only now beginning to understand properly.

The issue was that we didn't have the right API for this construction of extending a presheaf-on-a-basis to a presheaf on the space. A general presheaf on a space, when evaluated at some open $U$, is just some random type. But for a presheaf coming from a presheaf-on-a-basis this is far from being true -- the sections are subtypes of pi types, and the restriction maps are literally restrictions. This is all wrapped up in the definition of the construction of a presheaf from a presheaf-on-a-basis. I realised that if $F^+$ is a presheaf coming from a presheaf-on-a-basis then for $x\in U\subseteq X$ and $s\in F^+(X)$ a function, the fact that $(res_U s)(x)=s(x)$ seemed to be true by definition, but Lean would not definitionally unfold the restriction map from $F^+(X)$ to $F^+(U)$ as a restriction of functions. I had to explicitly push Lean in the right direction with lines like dunfold presheaf_on_basis_to_presheaf, dsimp; I was really surprised that this could make progress when a simple dsimp could not.

But we shouldn't have been doing this anyway. It seems to me that the correct thing to do is:

1) Define the construction presheaf_on_basis_to_presheaf
2) Define also the actual noncomputable function space, i.e. given $F$ a presheaf on a basis, and an open set $$U$ (not necc in the basis), define the space of functions sending an element $x$ of $U$ to an element of the stalk $F_x$, and have some coercion from $F^+(U)$ to this space of functions.
3) Crucially, prove (by rfl) that the restriction map on $F^+$ really is just restriction of functions. This is some key lemma which if you don't explicitly say it, can get buried. Prove it for values too -- prove that if $S\in F^+(U)$ and $V\subseteq U$ and $x\in V$ then $S(x)=res(S)(x)$. This is how you will eliminate res in practice. We were having to eliminate it using dunfold and then dsimp.
4) Also crucially, you should hide the classical.indefinite_descriptions. Given local sections $s_i$ which agree on overlaps, there's a non-computable function on $U$ which agrees with each $s_i$, but to define it at $x$ you have to choose
$i$ with $x\in U_i$. It's a theorem that the resulting function is independent of all choices. Define the noncomputable function and prove the theorem -- you will need it later!

We'd done none of this, and it was only when struggling through the proof that I began to understand what was missing.

I know you (Johan) are working in a far more complicated situation, but somehow these are the things which seem to me to be necessary to make things work smoothly. Ramon arrived in my office with a goal that had three classical.indefinite_descriptions on one side of an equality, and these are horrible to work with. The idea which Patrick showed so convincingly in his Nantes talk -- hide the nonconstructive stuff with a choose tactic and immediately go to the noncomputable function and the proof that it has the key property you want -- is a really important trick for getting things to run smoothly.

[Johan Commelin]

Thanks for these detailed comments! They will probably be helpful when I pick up my work on sheaves again in a couple of days!

[Kevin Buzzard]

How do you extend the presheaf on a basis in your generality?

[Kevin Buzzard]

Is it still a stalk-valued function?

[Johan Commelin]

You can take a limit over all basic opens contained in U.

[Kevin Buzzard]

Does that work for sites?

[Johan Commelin]

Yes, extending the presheaf is not too hard. What I'm missing is a good API for the sheaf condition.

[Kevin Buzzard]

What I learnt today was that there are special extra lemmas for presheaves which have come from a presheaf-on-a-basis, and those are what we needed to prove that sheaves go to sheaves.

[Johan Commelin]

Because it needs to work with abstract sites (where you don't know anything about the opens in your category) and then it should also work for concrete things like the open sets in a concrete topological space (and your presheaf has some concrete interpretation as functions)... somehow these two things don't play nicely together yet.

[Kevin Buzzard]

But your limit is different. You're taking a subset of a product perhaps.

[Kevin Buzzard]

Hmm. Maybe the ideas are still the same. I'm perhaps suggesting that you spend some time proving lemmas (by rfl) about the function sending an open U to the product of $F(U_i)$ where the $U_i$ range over the basis elements that are part of a cover. Then prove that if $V$ is a subset of $U$ then the restriction map is something like "restrict to the $U_i$ which map to $V$". Or something.

[Johan Commelin]

@Kevin Buzzard @Ramon Fernandez Mir Does this mean that you are now rapidly approaching a cleaned up version of schemes? When will there be code that we can look at?

[Mario Carneiro]

I would also like to see some code, I might be able to give some tips. I think you should define the glue construction for functions, i.e. if you have a bunch of functions that agree on overlaps then you get a function on the union. You can put your choices here and never see them again

[Kevin Buzzard]

https://github.com/ramonfmir/lean-scheme

[Kevin Buzzard]

We've only just started really, but we're moving along nicely.

[Kenny Lau]

do we have sheaves on sites yet? how far are we away from it?

[Kenny Lau]

import category_theory.limits.limits

universes v w u

namespace category_theory

inductive pullback_diagram : Type v
| base_left | base_right | target

namespace pullback_diagram

inductive hom : pullback_diagram → pullback_diagram → Type v
| id_base_left : hom base_left base_left
| id_base_right : hom base_right base_right
| id_target : hom target target
| to_target_left : hom base_left target
| to_target_right : hom base_right target

def id : Π X : pullback_diagram.{v}, hom X X
| base_left  := hom.id_base_left
| base_right := hom.id_base_right
| target     := hom.id_target

def comp : Π X Y Z : pullback_diagram.{v}, hom X Y → hom Y Z → hom X Z
| _ _ _ hom.id_base_left    g             := g
| _ _ _ hom.id_base_right   g             := g
| _ _ _ hom.id_target       g             := g
| _ _ _ hom.to_target_left  hom.id_target := hom.to_target_left
| _ _ _ hom.to_target_right hom.id_target := hom.to_target_right

instance : small_category pullback_diagram.{v} :=
{ hom := hom,
  id := id,
  comp := comp,
  comp_id' := λ X Y f, by cases f; refl,
  id_comp' := λ X Y f, by cases f; refl,
  assoc' := λ W X Y Z f g h, by cases f; cases g; cases h; refl }

def to_category {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
  pullback_diagram.{w} ⥤ C :=
{ obj := λ p, pullback_diagram.rec_on p X Y Z,
  map := λ p q h, @hom.rec_on (λ p' q' h', (pullback_diagram.rec_on p' X Y Z : C) ⟶ pullback_diagram.rec_on q' X Y Z) p q h
    (𝟙 X) (𝟙 Y) (𝟙 Z) f g,
  map_id' := λ p, by cases p; refl,
  map_comp' := λ p q r h1 h2, by cases h1; cases h2; dsimp only [category_struct.comp, comp]; simp only [category.comp_id, category.id_comp] }

def to_category_cone {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (W : C) (f' : W ⟶ X) (g' : W ⟶ Y) (h : f' ≫ f = g' ≫ g) :
  limits.cone (to_category f g) :=
{ X := W,
  π :=
  { app := λ p, pullback_diagram.rec_on p f' g' (f' ≫ f),
    naturality' := λ p q f, by cases f; dsimp only [functor.const, to_category]; simp only [category.comp_id, category.id_comp, h] } }

end pullback_diagram

@[class] def has_pullback (C : Type u) [category.{v} C] : Type (max u v) :=
limits.has_limits_of_shape pullback_diagram.{v} C

section has_pullback

variables {C : Type u} [𝒞 : category.{v} C] [P : has_pullback.{v} C]
include 𝒞 P

def pullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : C :=
(P (pullback_diagram.to_category f g)).cone.X

def pullback.fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ⟶ X :=
(P (pullback_diagram.to_category f g)).cone.π.app pullback_diagram.base_left

def pullback.snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ⟶ Y :=
(P (pullback_diagram.to_category f g)).cone.π.app pullback_diagram.base_right

def pullback.corec {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (W : C) (f' : W ⟶ X) (g' : W ⟶ Y) (h : f' ≫ f = g' ≫ g) : W ⟶ pullback f g :=
(P (pullback_diagram.to_category f g)).is_limit.lift (pullback_diagram.to_category_cone f g W f' g' h)

end has_pullback

class has_site (C : Type u) [category.{v} C] [has_pullback C] : Type (max u v) :=
(cov : Π U : C, set (set (Σ V, V ⟶ U)))
(iso_mem : ∀ {U V : C} (e : V ≅ U), { sigma.mk V e.1 } ∈ cov U)
(comp_mem : ∀ {U : C} (S : set (Σ V, V ⟶ U)) (HS : S ∈ cov U)
  (F : Π m : Σ V, V ⟶ U, m ∈ S → set (Σ V, V ⟶ m.1)),
  (∀ m hm, F m hm ∈ cov m.1) →
  { m | ∃ t ∈ S, ∃ u ∈ F t H, (⟨u.1, u.2 ≫ t.2⟩ : Σ V, V ⟶ U) = m } ∈ cov U)
(pullback_mem : ∀ {U} (S ∈ cov U) (V) (f : V ⟶ U),
  { m | ∃ t ∈ S, (⟨_, pullback.fst f t.2⟩ : Σ W, W ⟶ V) = m } ∈ cov V)

end category_theory

namespace lattice

class Sup_lattice (X : Type u) extends lattice X, has_Sup X :=
(le_Sup : ∀ {s : set X} {a : X}, a ∈ s → a ≤ Sup s)
(Sup_le : ∀ {s : set X} {a : X}, (∀ (b : X), b ∈ s → b ≤ a) → Sup s ≤ a)

class Sup_distrib_lattice (X : Type u) extends Sup_lattice X :=
(inf_Sup_le {} : ∀ {x : X} {s : set X}, x ⊓ lattice.Sup s ≤ lattice.Sup ((⊓) x '' s))

section Sup_lattice

instance complete_lattice.to_Sup_lattice {X : Type u} [complete_lattice X] : Sup_lattice X :=
{ .. (infer_instance : complete_lattice X) }

variables {X : Type u} [Sup_lattice X]

theorem le_Sup' {s : set X} {a : X} : a ∈ s → a ≤ Sup s :=
Sup_lattice.le_Sup

theorem Sup_le' {s : set X} {a : X} : (∀ (b : X), b ∈ s → b ≤ a) → Sup s ≤ a :=
Sup_lattice.Sup_le

theorem Sup_singleton' (x : X) : Sup {x} = x :=
le_antisymm (Sup_le' $ λ b hb, set.eq_of_mem_singleton hb ▸ le_refl _) $
le_Sup' $ set.mem_singleton x

end Sup_lattice

section Sup_discrete_lattice

instance complete_distrib_lattice.to_Sup_distrib_lattice {X : Type u} [complete_distrib_lattice X] : Sup_distrib_lattice X :=
{ inf_Sup_le := λ x s, by rw [inf_Sup_eq, Sup_image],
  .. (infer_instance : complete_distrib_lattice X) }

variables {X : Type u} [Sup_distrib_lattice X]

theorem inf_Sup {x : X} {s : set X} : x ⊓ lattice.Sup s = lattice.Sup ((⊓) x '' s) :=
le_antisymm Sup_distrib_lattice.inf_Sup_le $ Sup_le' $ λ b ⟨c, hcs, hxcb⟩, hxcb ▸ inf_le_inf (le_refl x) (le_Sup' hcs)

end Sup_discrete_lattice

end lattice

namespace category_theory

open lattice

variables {X : Type u}

class is_univalent (X : Type u) [category.{v} X] : Prop :=
(univalent : ∀ x y : X, ∀ e : x ≅ y, x = y)

theorem eq_of_iso [category.{v} X] [is_univalent X] {x y : X} (e : x ≅ y) : x = y :=
is_univalent.univalent x y e

instance is_univalent_partial_order [partial_order X] : is_univalent X :=
⟨λ x y e, le_antisymm e.1.1.1 e.2.1.1⟩

instance semilattice_inf.has_pullback [semilattice_inf X] : has_pullback X :=
λ F,
{ cone :=
  { X := F.obj pullback_diagram.base_left ⊓ F.obj pullback_diagram.base_right,
    π :=
    { app := λ p, pullback_diagram.rec_on p ⟨⟨inf_le_left⟩⟩ ⟨⟨inf_le_right⟩⟩
        ⟨⟨le_trans inf_le_left (F.map pullback_diagram.hom.to_target_left).down.down⟩⟩,
      naturality' := by intros; ext } },
  is_limit :=
  { lift := λ c, ⟨⟨le_inf (c.π.app pullback_diagram.base_left).down.down (c.π.app pullback_diagram.base_right).down.down⟩⟩,
    fac' := by intros; ext,
    uniq' := by intros; ext } }

instance Sup_lattice.has_site [Sup_distrib_lattice X] : has_site X :=
{ cov := λ U, { c | U ≤ Sup (sigma.fst '' c) },
  iso_mem := λ U V e, show U ≤ _, by rw [set.image_singleton, Sup_singleton']; exact e.2.1.1,
  comp_mem := λ U S HS F HF, le_trans HS $ Sup_le' $ λ x hx, let ⟨m, hmS, hmx⟩ := hx in
    hmx ▸ le_trans (HF m hmS) (Sup_le' $ λ y hy, let ⟨n, hnFS, hny⟩ := hy in
      le_Sup' ⟨⟨n.1, ⟨⟨le_trans n.2.1.1 m.2.1.1⟩⟩⟩, ⟨m, hmS, n, hnFS, rfl⟩, hny⟩),
  pullback_mem := λ U S HS V f,
  calc  V
      ≤ V ⊓ Sup (sigma.fst '' S) : le_inf (le_refl V) (le_trans f.1.1 HS)
  ... = Sup ((⊓) V '' (sigma.fst '' S)) : inf_Sup
  ... = Sup ((⊓) V ∘ sigma.fst '' S) : congr_arg Sup (set.image_comp _ _ S).symm
  ... ≤ Sup (sigma.fst '' {m | ∃ t ∈ S, (⟨_, pullback.fst f t.2⟩ : Σ W, W ⟶ V) = m}) :
    Sup_le' (λ b ⟨c, hcs, hb⟩, le_Sup' ⟨⟨V ⊓ c.1, ⟨⟨inf_le_left⟩⟩⟩, ⟨c, hcs, rfl⟩, hb⟩) }

end category_theory

[Kenny Lau]

import category_theory.limits.types

universes u v

namespace category_theory

instance has_pullback_Type : has_pullback (Type u) :=
λ F, by apply_instance

instance has_site_Type : has_site (Type u) :=
{ cov := λ α, { S | ∀ x : α, ∃ (f : Σ β, β ⟶ α), ∃ hf : f ∈ S, x ∈ set.range f.2},
  iso_mem := λ α β e x, ⟨⟨β, e.1⟩, set.mem_singleton _, e.2 x, congr_fun e.4 x⟩,
  comp_mem := λ α S HS F HF x, let ⟨f, hf, p, hfpx⟩ := HS x in
    let ⟨g, hg, q, hgqp⟩ := HF f hf p in
    ⟨⟨g.1, g.2 ≫ f.2⟩, ⟨f, hf, g, hg, rfl⟩, q, hfpx ▸ hgqp ▸ rfl⟩,
  pullback_mem := λ α S HS β f x, let ⟨g, hg, p, hgpx⟩ := HS (f x) in
    ⟨⟨pullback f g.2, pullback.fst f g.2⟩, ⟨g, hg, rfl⟩,
      ⟨λ v, pullback_diagram.rec_on v x p (f x),
      by intros v w h; cases h; dsimp only [pullback_diagram.to_category]; { refl <|> exact hgpx }⟩,
    rfl⟩ }

end category_theory

[Kenny Lau]

@Johan Commelin Am I duplicating effort?

[Johan Commelin]

@Kenny Lau Thanks for looking into this. The idea of the is_univalent class is a nice one! Also, as has been mentioned in the other thread, I agree that refining the lattice hierarchy is probably a good idea. (And I hope it doesn't lead to some exponential blow-up down the road.)
I don't think you are duplicating effort. Concerning pullback_diagram: there have been long discussions between @Scott Morrison @Reid Barton and myself and I think we are still not completely clear on what the best way to support special shapes is.
Other thoughts:

• there are different approaches to sites: Grothendieck topologies, coverages, and Grothendieck pretopologies. You have formalised pretopologies but not every site admits a pretopology (e.g. a basis for a topological space can be turned into a site, but doesn't have to be a pretopology).
• When I was working on these things half a year ago, I managed to formalise the definition of a sheaf on site. But I had a hard time actually verifying that certain "trivial" examples are sheaves: e.g. (continuous) functions from a topological space X to (a topological space) Y.
• Currently Kevin and you are thinking/working hard on gluing sheaves, which I think is a perfect way to stress-test the definitions. However, I would really want to add two things to that list: sheafification and the adjunction between pushforward and pullback. Without those, we won't have a reasonable API to sheaves.

In hindsight, I took on a project that was way to big. I'm very excited that there are now more people pouring power into this (-;

[Scott Morrison]

Regarding is_univalent --- usually this is called skeletal.

[Kenny Lau]

@Johan Commelin didn't I formalize sites in terms of coverages?

[Johan Commelin]

You use pullbacks

[Johan Commelin]

Coverages allow you to define sites on categories that don't have pullbacks

[Johan Commelin]

E.g. lattices without infs

[Johan Commelin]

E.g. bases of topologies

[Kevin Buzzard]

The schemes work that Ramon did about extending sheaves on bases to sheaves was made much easier by the fact that the intersection of two basic open sets was basic open in our situation.

[Kevin Buzzard]

$D(f)\cap D(g)=D(fg)$.

[Kevin Buzzard]

Without that, the construction of the sheaf of rings on $\mathrm{Spec}(A)$ would have been harder.

[Kenny Lau]

I just followed Stacks project

[Johan Commelin]

https://ncatlab.org/nlab/show/coverage

[Kenny Lau]

so I should use that definition instead?

[Kenny Lau]

also where did the first two axioms go?

[Johan Commelin]

@Kenny Lau You don't need the first two axioms.

[Kenny Lau]

then why did Stacks include them?

[Johan Commelin]

See also https://ncatlab.org/nlab/show/Grothendieck+topology#Saturation

[Johan Commelin]

It might make sense to browse through the first half of SGA 4 if you want to seriously attempt to build a library for sites.

[Kevin Buzzard]

SGA 4 you mean? Or not

[Johan Commelin]

Fixed :smiley:

[Kenny Lau]

how about no

[Kevin Buzzard]

SGA4 is not hard to read

[Kevin Buzzard]

It's much easier than EGA4

[Kenny Lau]

is there an English translation?

[Kevin Buzzard]

I don't know. "Categorie" = category, "morphisme" = morphism, "univers" = universe. Try just taking symmetric difference with {e}.

[Kenny Lau]

so espace etale = spac tal?

[Kevin Buzzard]

change e-acute to s

[Kevin Buzzard]

that sometimes work.

[Kevin Buzzard]

fenetre -> fenester

[Kenny Lau]

surely fenetre -> fnstr

[Kevin Buzzard]

Oh it's e-hat goes to s

[Johan Commelin]

Come on Kenny, your French is better than mine... and I can read that...

[Kevin Buzzard]

You're missing off the accents. They're not all e's.

[Kenny Lau]

how did Grothendieck call Grothendieck topos/topology/etc?

[Kevin Buzzard]

Probably just topos / topology on a category.

[Kenny Lau]

et d'ailleurs, quelles pages dois-je lire?

[Kevin Buzzard]

The definitions are probably only a few pages in.

[Kenny Lau]

il ne definit faisceaux que dans page 223

[Kenny Lau]

ok tous ce que j'ai besoin de est dans expose II

[Johan Commelin]

I'm not saying you should formalise SGA 4.1. But I'm saying that it might be good to be aware of what's in there.

[Kenny Lau]

Soit C une categorie. On appelle crible de la categorie C une sous-categorie pleine D de C possedant la propriete suivante: tout objet de C tel qu'il existe un morphisme de cet objet dans un objet de D est dans D. Soit X un objet de C; on appelle (par abus de langage) cribles de X les cribles de la categorie C/X.

[Kenny Lau]

seems complicated

[Johan Commelin]

Right... another option is to forget about sites for the moment.

[Johan Commelin]

And focus on sheaves on distrib_inf_lattices or whatever the variant you need.

[Kenny Lau]

can't I just use some variants of my current definition

[Johan Commelin]

Sure, you can

[Johan Commelin]

But if you want a basis for a topology to be a site, then you need coverages

[Kenny Lau]

structure sheaf (C : Type u) [category.{v} C] [has_pullback C] [has_site.{v} C] : Type (max u v (w+1)) :=
(to_presheaf : presheaf.{v w} C)
(ext : ∀ U : C, ∀ s t : to_presheaf.eval U, ∀ c ∈ has_site.cov U,
  (∀ d : Σ V, V ⟶ U, d ∈ c → to_presheaf.res d.2 s = to_presheaf.res d.2 t) →
  s = t)
(glue : ∀ U : C, ∀ c ∈ has_site.cov U, ∀ F : Π d : Σ V, V ⟶ U, d ∈ c → to_presheaf.eval d.1,
  (∀ d1 d2 : Σ V, V ⟶ U, ∀ H1 : d1 ∈ c, ∀ H2 : d2 ∈ c,
    to_presheaf.res (pullback.fst d1.2 d2.2) (F d1 H1) =
    to_presheaf.res (@@pullback.snd _ _inst_2 d1.2 d2.2) (F d2 H2)) →
  ∃ g : to_presheaf.eval U, ∀ d : Σ V, V ⟶ U, ∀ H : d ∈ c,
    to_presheaf.res d.2 g = F d H)

[Kenny Lau]

But if you want a basis for a topology to be a site, then you need coverages

oh that's for extending a sheaf from a sheaf on basis?

[Johan Commelin]

Yup, if you want to do that using the general framework

[Kenny Lau]

how do I do that if I have coverages?

[Johan Commelin]

We could of course do a hands-on extension

[Johan Commelin]

how do I do that if I have coverages?

You need to formalise morphism of sites, and then the $site_{basis}$ comes with a geometric morphism (aka morphism of sites/topoi) to $site_{topology}$.

[Johan Commelin]

You pushforward along this morphism.

[Kenny Lau]

and how do you show that if I restrict a sheaf to a sheaf on basis then extend it again, I get the "same" sheaf?

[Johan Commelin]

That's a theorem. I'm not saying it's easy.

[Johan Commelin]

(It's math easy, of course)

[Kenny Lau]

how do you do it in maths?

[Johan Commelin]

"Proof. Follows from the sheaf property. QED" (I guess this is what most people would do...)

[Johan Commelin]

I think there is a proof in the stacks project. The define a notion of "sheaf on a basis". But what they do is hands on. If you use coverages, then a "sheaf on a basis" is just a sheaf.

[Johan Commelin]

I don't know if we want to care about sheaves on bases...

[Kenny Lau]

so what I'm wondering is, if you use this wonderful language of coverage, how do you do it?

[Johan Commelin]

Well, you will still need to use the sheaf property for coverages

[Johan Commelin]

But anyway... do you have a good reason to pursue this?

[Johan Commelin]

Or should we first try to do the push-pull adjunction for sheaves on topological spaces?

[Kenny Lau]

I don't know

[Kenny Lau]

import category_theory.category

universes v u

namespace category_theory

class has_site (C : Type u) [category.{v+1} C] : Type (max u v) :=
(cov : Π U : C, set (set (Σ V : C, V ⟶ U)))
(lift : ∀ U : C, ∀ c ∈ cov U, ∀ V : C, ∀ g : V ⟶ U, ∃ h ∈ cov V,
  ∀ j ∈ h, ∃ i ∈ c, ∃ k : sigma.fst j ⟶ sigma.fst i, k ≫ i.2 = j.2 ≫ g)

end category_theory

[Kenny Lau]

@Johan Commelin how does this look?

[Mario Carneiro]

is that really the only axiom? I would have expected something like "{<U, id>} \in cov U" and possibly something about covers of covers

[Kenny Lau]

I'm just using https://ncatlab.org/nlab/show/coverage#Definition

[Kenny Lau]

I believe it's like how you can generate an equivalence relation given just any relation

[Kenny Lau]

and it's also to allow for a basis to be a site

[Kenny Lau]

import category_theory.sites.basic topology.bases topology.opens

universes v u

namespace category_theory

open topological_space lattice

@[reducible] def topological_basis (X : Type u) [topological_space X] : Type u :=
{ B : set (opens X) // opens.is_basis B }

instance basis.has_site {X : Type u} [topological_space X] (B : topological_basis X) : has_site B :=
{ cov := λ U, { c | ∀ x ∈ U.1, ∃ i ∈ c, x ∈ subtype.val (sigma.fst i) },
  lift := λ U c hc V g, ⟨{ h | ∃ i ∈ c, h.1.1 ≤ V ⊓ i.1.1 },
    λ x hxV, let ⟨i, hic, hxi⟩ := hc x (g.1.1 hxV),
      ⟨W, HWB, hxW, HWVi⟩ := opens.is_basis_iff_nbhd.1 B.2 (show x ∈ V.1 ⊓ i.1.1, from ⟨hxV, hxi⟩) in
      ⟨⟨⟨W, HWB⟩, ⟨⟨λ y hy, (HWVi hy).1⟩⟩⟩, ⟨i, hic, HWVi⟩, hxW⟩,
    λ j ⟨i, hic, hjVi⟩, ⟨i, hic, ⟨⟨λ y hy, (hjVi hy).2⟩⟩, rfl⟩⟩ }

end category_theory

[Kenny Lau]

looks like it's working

[Johan Commelin]

@Kenny Lau Cool!

[Johan Commelin]

So now you can probably also write down the sheaf axiom(s) in this language.

[Kevin Buzzard]

But anyway... do you have a good reason to pursue this?

Pushforwards and pullbacks are just adjoint functors. Kenny is flagging the situation where we go from a sheaf on a basis to a sheaf, and in that situation both the functors are equivalences. Is this some sort of Galois connection but one level up?

I guess Grothendieck knew that a top space, and a top-space-with-a-basis, were the same thing as far as sheaf theory goes, so he defined the topos associated to the site to be the category of sheaves on the site, and then we have two different sites with the same topos (and hence the same "geometry").

is that really the only axiom? I would have expected something like "{<U, id>} \in cov U" and possibly something about covers of covers

These are definitely axioms in some of these abstrations. What's a Grothendieck topology? Is this the difference between a Groth Top and a coverage?

[Johan Commelin]

Galois connections are adjunctions one level down, yes.

[Johan Commelin]

A coverage is the bare minimum that you need. You can use those to generate a Grothendieck topology.

[Kevin Buzzard]

Is it a Galois insertion I'm talking about then?

[Johan Commelin]

A Galois insertion is like an adjunction where the left(?) adjoint is fully faithful.

[Johan Commelin]

Ad coverage and axioms, see https://ncatlab.org/nlab/show/coverage#saturation_conditions

[Kevin Buzzard]

I have never used the nlab as a serious reference before (of course this is mostly because I do number theory rather than higher category stuff). I get the impression that there's a small community so probably not much refereeing going on. It would an interesting test for the nlab pages if they were being used as a resource for formalising. How accurate are they? I know that Kenny sees the nlab and can't tell it apart from SGA4, but for me SGA4 is refereed, much used, and trustworthy, whereas nlab is just some random website which might be full of fake news.

[Kevin Buzzard]

This was also a problem with Wikipedia in the beginning, when it had some maths pages and the quality was extremely variable.

[Reid Barton]

I would say nlab in general is somewhat more trustworthy than Wikipedia though of course still less trustworthy than peer-reviewed publications. Compared to Wikipedia, the nlab authors are a lot more likely to know what they're talking about in the first place.

[Kevin Buzzard]

Well that's good to know. With Wikipedia there used to be dozens of inaccuracies in some articles, some were very poor initially, but I could never be bothered to learn how to change them (I had three small kids at the time). Sufficiently many people did learn that Wikipedia is much better now, but I just didn't really know about nLab's record for accuracy, and if I don't know then my default opinion is "do not trust". What I've seen from it does look good though, when I'm reading about stuff I already understand.