valuations

Stream: maths

[Kevin Buzzard]

Both the Fibonacci Squares project and the Adic Space project need valuations on rings -- one in rather more generality than the other. But let's start at the beginning. Does Lean have p-adic valuations on Z? In other words, is the function $v_p(\cdot)$ on the non-zero integers (or even rationals) sending $p^nN$ (with $N$ coprime to the prime $p$) to $n$? The key theorems are $v_p(ab)=v_p(a)+v_p(b)$ and $v_p(a+b)\geq\min\{v_p(a),v_p(b)\}$ (where $v_p(0)$ is usually taken to be $+\infty$).

[Kevin Buzzard]

Perfectoid space valuations would take values in a certain kind of totally ordered monoid

[Kevin Buzzard]

(and are of a slightly different nature -- they are really norms not valuations, so the total function $M \mapsto p^{-v_p(M)}$ with target the non-negative reals would be an example).

[Reid Barton]

I have approximately this lying around somewhere

[Reid Barton]

https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

[Reid Barton]

I guess ord_add is missing, but it should be easy to prove from the other stuff

[Kevin Buzzard]

line 91 should now be

[Kevin Buzzard]

... = p * (p^r * k) : by unfold pow nat.pow; ac_refl,

[Kevin Buzzard]

[adding pow, probably because of some relatively recent change with ^]

[Kevin Buzzard]

Thanks so much! This is exactly what I wanted!

[Kevin Buzzard]

What a great little community we are getting here!

[Kevin Buzzard]

I'm just going to dump it in a subdirectory in my project called Reid_Barton. Is that OK?

[Kevin Buzzard]

Is there a better way of doing things?

[Reid Barton]

Sure, no problem.
The better way is probably to try to PR things into mathlib, but that's more effort.

[Kevin Buzzard]

example : has_le (ℕ+) := by apply_instance -- fails

[Kevin Buzzard]

Noticed this along the way. You've not proved the valuation of a + b but you've proved everything but. I've never worked with \N+ before.

[Kevin Buzzard]

Is there a good reason for not having le on \N+? I am making a little collection of random short mathlib proposals. I understand how mathlib works much better after my schemes exercise.

[Reid Barton]

I doubt there is any good reason. pnat isn't used that much, it seems. I remember finding it a little more annoying to use than I would have liked

[Reid Barton]

Particularly as there are coercions in both directions between nat and pnat

[Kevin Buzzard]

Is ord_pow broken?

[Kevin Buzzard]

Or did I break it myself?

[Reid Barton]

It's quite possibly broken because it is about 2.5 months old

[Kevin Buzzard]

do computer scientists really need a _coercion_ from nat to pnat?

[Kevin Buzzard]

I just can't even guess what it would be

[Kevin Buzzard]

"any one of a couple of random examples"

[Kevin Buzzard]

lemma ord_pow {k : ℕ} {a : ℕ+} : ord p (a^k) = k * ord p a := ord_ppow

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I think some coercion magic happened?

[Kevin Buzzard]

Is there a type Nat union {infinity}? I mean, it's option Nat but I want the obvious le, add and min functions (and don't want to write them if they're already there). The reason I ask is to extend p-adic valuation to zero, and I think I do have to add infinity, because the standard CS answer of just defining it to be 37 or whatever and ploughing on regardless doesn't seem to work here, because then things like min are wrong.

[Kenny Lau]

it's called the ordinal omega+1 :D

[Kevin Buzzard]

:D

[Kevin Buzzard]

Things which I want to be there, are more and more often beginning to be there :D

[Kevin Buzzard]

Anyone fancy univariate polynomials over a field (division algorithm, degree function with the usual problems at 0, gcd, unique factorization?)

[Kevin Buzzard]

I'm seeing that pop up more and more. Lean has multivariate polynomials but I think these deserve to be a special class rather than constantly carrying around the type "unit" for your list of variables.

[Kevin Buzzard]

@Nicholas Scheel do you want to try this? I'm going to show your work on Z[alpha] to the British Maths Olympiad squad tomorrow! See what they make of it.

[Kevin Buzzard]

Some stuff is there by a student of Johannes in his mason-stother directory but I don't think it's all there. And didn't someone do some Euclidean Algorithm stuff recently? Some student of Scott maybe? That might help I guess.

[Kevin Buzzard]

We need univariate polynomials for the Fibonacci project, as you know.

[Kevin Buzzard]

Or maybe Kenny or Chris will do it now their exams are over.

[Kevin Buzzard]

A fair amount of this stuff should be tidied up and put in mathlib, so it's all in one place.

[Andrew Ashworth]

hah, won't you soon have your own army of undergraduates working for you over the summer?

[Kevin Buzzard]

Over 20 undergrads now

[Kevin Buzzard]

They start 2nd July

[Kevin Buzzard]

It's going to be a crazy summer!

[Kevin Buzzard]

2 months!

[Kevin Buzzard]

I am so rubbish at coe

[Kevin Buzzard]

@[simp] lemma pgcd_coe_something (a b : ℕ) : pgcd a b = gcd a b := begin
unfold pgcd,
--rw pnat.coe_nat_coe a, -- I am so rubbish at coe
sorry
end

[Kevin Buzzard]

This is Reid's pgcd from his gist from earlier

[Kevin Buzzard]

https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

[Mario Carneiro]

Is there a type Nat union {infinity}?

As of this morning, there is a with_top A structure that adds an infinity element to any order. So with_top nat is just what you want.

[Kenny Lau]

wow what a coincidence lol

[Mario Carneiro]

do computer scientists really need a _coercion_ from nat to pnat?

Hm, my original concern was that if you wanted to write 5 as a pnat you would need to write <5, dec_trivial> which is obviously cumbersome. But actually since pnat has has_one and has_add that's actually enough for bit0 and bit1 to work, meaning that (5 : pnat) works fine (being defined as bit1 (bit0 1) where the 1 and addition are interpreted in pnat). So maybe this isn't needed. I'll see what breaks if I remove it, I agree it's not great to have a non-identity looking coercion

[Mario Carneiro]

I was thinking of using pnat for the domain of Z/nZ btw, which will give it a better algebraic theory than fin n

[Kevin Buzzard]

Is there a type Nat union {infinity}?

As of this morning, there is a with_top A structure that adds an infinity element to any order. So with_top nat is just what you want.

Mario -- did you see Remark 1.5 of www2.math.uni-paderborn.de/fileadmin/Mathematik/People/wedhorn/Lehre/AdicSpaces.pdf (page 4)? There is a fundamental construction in adic spaces -- adding a "bottom" element zero to a a totally ordered group (e.g the group of positive reals) and creating a totally ordered monoid. Is this sort of thing easy to do now?

[Nicholas Scheel]

@Kevin Buzzard I could spend an hour or two on it ... should I use multivariate polynomials, should I use finsupp, or just do a direct list encoding?

[Mario Carneiro]

Actually your comment got me thinking about this. There is a related construction, let's say with_zero A, which adds a unit to any additive semigroup; and if the zero and bottom coincide then you get a composite structure which works well on some kinds of ordered groups, I would imagine. Similarly you can make sense of addition with infinity, and that structure coheres with the order of with_top, so that you can add an infinity element to an ordered additive semigroup.

[Mario Carneiro]

This could be used to factor ennreal into with_top nnreal

[Kenny Lau]

rip ennreal 2017-2018

[Kenny Lau]

born Aug 30, 2017

[Mario Carneiro]

It probably wouldn't go away as a definition, it has enough properties on its own that make it worthy of study, but it would simplify and generalize some theorems

[Mario Carneiro]

But to answer your question, currently with_bot and with_top only deal with the order structure, they don't have any monoid stuff

[Kevin Buzzard]

do computer scientists really need a _coercion_ from nat to pnat?

Hm, my original concern was that if you wanted to write 5 as a pnat you would need to write <5, dec_trivial> which is obviously cumbersome. But actually since pnat has has_one and has_add that's actually enough for bit0 and bit1 to work, meaning that (5 : pnat) works fine (being defined as bit1 (bit0 1) where the 1 and addition are interpreted in pnat). So maybe this isn't needed. I'll see what breaks if I remove it, I agree it's not great to have a non-identity looking coercion

Is it possible to keep the coercion but demand that the type class resolution system produces a proof of positivity before it is applied? I think that this would very much mirror the way a mathematician thought about the issue.

[Kevin Buzzard]

You might find that if proofs of positivity are carried around

[Kevin Buzzard]

with instances like "a > 0 and b > 0 implies a + b > 0"

[Kevin Buzzard]

then the coercions work fine.

[Kevin Buzzard]

With the current system you just occasionally see these \u \u x things

[Kevin Buzzard]

and it's only at the point where you go to cancel them and they won't cancel that you realise you've made a mathematical slip

[Kevin Buzzard]

Can we make the coercion part of type class resolution better?

[Mario Carneiro]

this isn't how coercions work

[Mario Carneiro]

they are functions A -> B, nothing else is allowed in there

[Mario Carneiro]

in particular, coercions cannot be partial

[Mario Carneiro]

except the coercion Prop -> bool which is magical

[Kevin Buzzard]

CS 101 question alert :-/

[Kevin Buzzard]

What's the theorem \<a,h\>.val = a called for subtypes?

[Mario Carneiro]

rfl

[Kevin Buzzard]

I was trying not to use rfl

[Kevin Buzzard]

I was looking at the proof that \u \u a =a

[Kevin Buzzard]

I just figured that I had a bunch of stuff about coercions that I needed to understand better before I said too much more about this

[Kevin Buzzard]

and then I ended up going down a rabbit hole watching the type class resolution system unfold :-/

[Kevin Buzzard]

Actually I don't understand.

[Kevin Buzzard]

How do I rewrite \u \u a as a?

[Kevin Buzzard]

Wait

[Kevin Buzzard]

I was asking for the name of the theorem

[Kevin Buzzard]

not the proof

[Mario Carneiro]

you haven't given me enough info to answer the question

[Kevin Buzzard]

I'll formulate something precise.

[Mario Carneiro]

lots of theorems look like \u \u a = a

[Mario Carneiro]

I need to know what is the type of a, and the type of \u a

[Kevin Buzzard]

[pause whilst we discover if Kevin is talking nonsense]

[Kevin Buzzard]

variables (α : Type) (p : α → Prop)
theorem what_am_i_called (a : α) (h : p a) : (subtype.mk a h).val = a := rfl

[Kevin Buzzard]

The question.

[Kevin Buzzard]

because I want to use you in a rewrite

[Kevin Buzzard]

so I need to know your name

[Mario Carneiro]

the theorem doesn't have a name, it is done automatically by dsimp

[Kevin Buzzard]

And there's you guys saying our naming conventions are bad

[Mario Carneiro]

same as how beta reduction isn't a named theorem

[Kevin Buzzard]

dsimp is what?

[Kevin Buzzard]

I used it a couple of times recently

[Kevin Buzzard]

Kenny told me "just use dsimp" and I'm like "ooh my goal has gone from 1 page to 5 lines"

[Mario Carneiro]

it's simp for definitional rewrites

[Kevin Buzzard]

which way does it go?

[Kevin Buzzard]

What does it actually do?

[Kevin Buzzard]

If it sees my subtype.mk.val stuff it just says "ooh I'll remove that"

[Kevin Buzzard]

but does it ever add it?

[Mario Carneiro]

it does exactly the same sort of thing as simp

[Kevin Buzzard]

oh great :-)

[Kevin Buzzard]

Another black box :-)

[Kevin Buzzard]

I see

[Mario Carneiro]

it cancels projections applied to structure mk

[Kevin Buzzard]

What else does it do?

[Mario Carneiro]

this is the structure iota rule

[Kevin Buzzard]

What's a complete list of what it does?

[Kevin Buzzard]

Would I be able to understand the source code?

[Kevin Buzzard]

Kenny says that Lean does not do magic but this is still magic to me

[Mario Carneiro]

dsimp has a config too

[Kevin Buzzard]

53 extra options?

[Mario Carneiro]

that has a fairly complete list of the kinds of automatic reductions it does, beta, eta, zeta, iota etc

[Mario Carneiro]

and it also uses @[simp] lemmas that are also rfl lemmas

[Mario Carneiro]

as well as definition unfolding when you give it to the bracket list or use !

[Kevin Buzzard]

I would be really interested in watching a video or seeing an article about what dsimp and/or simp do. If I understood what they were doing I wouldn't still just be hopefully typing simp every now and then just to see if I can make the goal go away

[Mario Carneiro]

Haven't we had this conversation before?

[Mario Carneiro]

I'm pretty sure you wrote that article

[Kevin Buzzard]

I feel like there's still a whole bunch of things I don't fully understand with all this business

[Kevin Buzzard]

I'll read my own docs and see if this enlightens me

[Andrew Ashworth]

The textbook "term rewriting and all that" is pretty good on this subject, if your uni library has it

[Nicholas Scheel]

simplification using definition equalities, I believe

[Kevin Buzzard]

So my real question was "how do I do a definitional rewrite in tactic mode", and the answer is "don't use rw, use show"

[Mario Carneiro]

change with is literally definitional rw

[Kevin Buzzard]

The textbook "term rewriting and all that" is pretty good on this subject, if your uni library has it

Thanks Andrew. My university can get any book for me.

[Mario Carneiro]

but dsimp is nice for just cleaning up some common patterns

[Kevin Buzzard]

Equality is asymmetric for you people, isn't it

[Kevin Buzzard]

This is only just dawning on me

[Mario Carneiro]

yes, with term rewrites direction really matters

[Kevin Buzzard]

If you write a = b, and if one side was more complicated than the other

[Kevin Buzzard]

you would put the more complicated side first

[Kevin Buzzard]

Is this just some general principle?

[Mario Carneiro]

yeah, simp simplifies

[Mario Carneiro]

it's not called complexify

[Kevin Buzzard]

I had not realised that = was asymmetric

[Kevin Buzzard]

in any way whatsoever

[Kevin Buzzard]

I have a different definition of = to you

[Mario Carneiro]

= itself is symmetric

[Kevin Buzzard]

symmetric in some theorem sense

[Kevin Buzzard]

but you have to decide which goes first

[Kevin Buzzard]

and we don't care

[Mario Carneiro]

but simp and dsimp takes the list of simp lemmas and use them as a rewrite graph

[Mario Carneiro]

and this is directed

[Kevin Buzzard]

Right, I've just been learning this from my own notes

[Kevin Buzzard]

Aah!

[Kevin Buzzard]

I've just realised what my question actually is.

[Kevin Buzzard]

My question is this: "I never ever tag anything with @[simp]. I make loads of structures. Can you give me some basic advice over which trivial lemmas I should be (a) proving and (b) tagging with simp?"

[Mario Carneiro]

Unfortunately, the answer is "depends on the structure"

[Mario Carneiro]

some axioms of a structure should be simp lemmas

[Kevin Buzzard]

subtype

[Mario Carneiro]

like zero_add

[Kevin Buzzard]

A type and a proof

[Mario Carneiro]

I don't think subtype has any simp lemmas

[Mario Carneiro]

which is to say, there is nothing that sticks out as necessary

[Mario Carneiro]

oh, <a, h1> = <b, h2> <-> a = b should be a simp lemma

[Kevin Buzzard]

What about presheaf of types on a topological space?

[Kevin Buzzard]

I made that structure once

[Mario Carneiro]

but actually I think simp might do that automatically anyway

[Kevin Buzzard]

I'll find you a link

[Mario Carneiro]

simp will already do a few things by default on all structures, which more or less covers all the general recommendations

[Kevin Buzzard]

https://github.com/kbuzzard/lean-stacks-project/blob/6617de7dd5f11af46f0c7e0d2223ee065d71b9f3/src/tag006E.lean#L4

[Kevin Buzzard]

I am proud to say that I did actually write a simp lemma for that

[Kevin Buzzard]

My simp lemma says "crap, I made a poor design decision when designing that structure, but I can't be bothered to change it now"

[Mario Carneiro]

that's just what I would have recommended

[Mario Carneiro]

except possibly for the dependent args

[Kevin Buzzard]

You would recommend the change in the structure?

[Mario Carneiro]

that doesn't matter so much

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

You don't care which definition I use if they're all equivalent?

[Kevin Buzzard]

I was going to bite the bullet one day and edit the definition of that structure. You're saying that's a crazy idea?

[Mario Carneiro]

it affects the proof goals when defining structures with { stuff := ... }

[Mario Carneiro]

so it depends on how you usually prove such goals

[Kevin Buzzard]

I was going to change "f = g circ h" with "forall x, g (h x) = f x"

[Mario Carneiro]

if the first thing you do is always funext, then that's a hint

[Kevin Buzzard]

Note the equality "f = g circ h"

[Kevin Buzzard]

the more complicated side on the right

[Kevin Buzzard]

is that also unwise?

[Mario Carneiro]

actually here I recommend that ordering

[Kevin Buzzard]

The thing about funext was that there were a few times when the fact that it was comp was really useful, it made some proofs really nice and short

[Mario Carneiro]

because the argument to f is getting simpler

[Kevin Buzzard]

boggle

[Kevin Buzzard]

I don't understand

[Mario Carneiro]

think of it as f (comp a b) = f a o f b

[Mario Carneiro]

here simp will want to go left to right to make the argument to f as simple as possible

[Kevin Buzzard]

It's res U W x = res V W (res U V x)

[Kevin Buzzard]

that's what it is really

[Kevin Buzzard]

You still want it that way round?

[Mario Carneiro]

that's not a good simp lemma

[Kevin Buzzard]

"restriction of a function on U down to V and then down to W equals restriction directly down to W"

[Kevin Buzzard]

Either way round?

[Mario Carneiro]

Okay, I guess in this case since it's a proof arg it shouldn't be a metric of simplicity

[Mario Carneiro]

so in that case you want res V W (res U V x) = res U W x

[Kevin Buzzard]

This is the thing I don't understand. It takes two functions res U V and res W V and it returns one function. It's made it simpler. I don't understand what should be a simp lemma.

[Kevin Buzzard]

Aah so you do want to switch the order?

[Kevin Buzzard]

And then make a simp lemma?

[Kevin Buzzard]

Okay, I guess in this case since it's a proof arg it shouldn't be a metric of simplicity

I don't understand that either :-/

[Mario Carneiro]

You have this extra argument that has a big term in it

[Mario Carneiro]

I've mentioned that proof args are bad for rewrites before

[Kevin Buzzard]

Why?

[Kevin Buzzard]

proof args are fundamental statements about the situation

[Kevin Buzzard]

Are you saying that associativity of addition should not be a simp lemma?

[Kevin Buzzard]

associativity of addition is both a simp lemma and seems to have the more complicated side on the right.

[Kevin Buzzard]

None of it adds up to me. I am still nowhere near understanding what should be a simp lemma.

[Mario Carneiro]

assoc is a special case

[Kevin Buzzard]

boggle

[Kevin Buzzard]

I'll add it to the docs

[Mario Carneiro]

simp has special handling for comm/assoc operations

[Kevin Buzzard]

which uses a convention which goes against the "simpler argument on the right" convention?

[Mario Carneiro]

it would not normally be a good simp lemma, because it doesn't simplify the term

[Kevin Buzzard]

mul_one is a simp lemma and it's a proof arg, if I've understood the last term correctly

[Mario Carneiro]

But simp will notice if you give it a lemma that looks like associativity and apply special algorithms to do smart things with that

[Mario Carneiro]

None of those have proof args

[Kevin Buzzard]

oh

[Mario Carneiro]

I'm talking about proofs as arguments to functions you want to rewrite

[Mario Carneiro]

so in this case that would be like proof arguments to mul or one

[Kevin Buzzard]

I thought you were talking about proofs as arguments used to create a structure

[Mario Carneiro]

in your case I'm talking about res which has three proof args

[Kevin Buzzard]

Would your opinion change if made them all work magically using type class resolution?

[Mario Carneiro]

yes

[Mario Carneiro]

that's an interesting idea, I'd have to see how messy the arguments can get

[Kevin Buzzard]

The reason I didn't use type class resolution for those things was that when I wrote that code I had no idea how typeclass resolution system worked

[Kevin Buzzard]

so I just over-rode it and would always pass the proofs manually

[Kevin Buzzard]

and then later on in the project I was forced to work with rings and ring homs

[Kevin Buzzard]

so I was forced to learn the system

[Kevin Buzzard]

and we had that long thread with me moaning and learning about letI

[Kevin Buzzard]

Ok so coercions.

[Kevin Buzzard]

theorem eew (Y : ℕ+) : ((Y : ℕ) : ℕ+) = Y := rfl -- fails

[Kevin Buzzard]

That's not good, right?

[Kevin Buzzard]

Should that be a simp lemma?

[Kevin Buzzard]

ℕ+ is one of my favourite sets in ZFC

[Kevin Buzzard]

Why is it so hard to work with here?

[Kevin Buzzard]

Just because it's not a stupid semiring

[Kevin Buzzard]

maybe it's a demisemiring

[Mario Carneiro]

that is a simp lemma, I think

[Kevin Buzzard]

Aah here's a question.

[Kevin Buzzard]

Let's say we ripped out the definition of pnat

[Mario Carneiro]

coe_nat_coe

[Kevin Buzzard]

and replaced it with a straight inductive structure with one and succ

[Kevin Buzzard]

Would that make any difference to anything

[Mario Carneiro]

not really

[Kevin Buzzard]

or you just write the new interface

[Kevin Buzzard]

and that's it

[Kevin Buzzard]

No issue with compile time or running time

[Kevin Buzzard]

or simp not working as well

[Mario Carneiro]

anything not using the interface would be affected, of course

[Kevin Buzzard]

Aah

[Kevin Buzzard]

anything accessing the innards of the structure

[Mario Carneiro]

i.e. if someone creates a pnat by writing <2, dec_trivial>

[Kevin Buzzard]

instead of (2 : pnat)

[Kevin Buzzard]

then they should be punished?

[Kevin Buzzard]

How does that work?

[Kevin Buzzard]

"You only use official constructors"

[Kevin Buzzard]

"not inbuilt stuff"

[Kevin Buzzard]

Oh wait -- surely anyone writing a proof in term mode with pnat will have constructors like that everywhere

[Kevin Buzzard]

because it's a super-cool way of being fancy in fancy term mode

[Kenny Lau]

right

[Kevin Buzzard]

eew

[Mario Carneiro]

well, the thing is that I don't want to avoid structure constructors, because they are very nice

[Kevin Buzzard]

So there is a question left

[Mario Carneiro]

you can't replicate that functionality with an interface

[Mario Carneiro]

unless the interface is to pass in a specially defined structure

[Mario Carneiro]

like simp_config

[Kevin Buzzard]

you've lost me now

[Kevin Buzzard]

but I do see that there is a huge argument for structure constructors and this presumably has some bearing on exactly which constructors you choose and maybe even in which order?

[Kevin Buzzard]

maybe order irrelevant

[Kevin Buzzard]

but you never know

[Mario Carneiro]

yes

[Mario Carneiro]

order is relevant for anonymous constructors

[Mario Carneiro]

Here are my currrent thoughts on presheaf fyi:

structure order_presheaf (α : Type u) [preorder α] :=
(F : α → Type u)
(res : ∀ x {y}, x ≤ y → F y → F x)
(Hid : ∀ x h a, res x h a = a)
(Hcomp : ∀ x y z h₁ h₂ (a : F z),
  res x h₁ (res y h₂ a) = res x (le_trans h₁ h₂) a)

[Kenny Lau]

what is an order_presheaf?

[Kevin Buzzard]

Would you want presheaves in mathlib?

[Kevin Buzzard]

oh eew

[Kevin Buzzard]

what just happened there

[Kevin Buzzard]

with the open sets

[Kenny Lau]

oh, they form a preorder under inclusion!

[Kevin Buzzard]

he thinks he's being clever

[Kevin Buzzard]

but we need the etale site ;-)

[Kevin Buzzard]

so he's still not general enough ;-)

[Mario Carneiro]

if you add enough axioms to the preorder you can capture exactly the open sets of some topology

[Kevin Buzzard]

yeah, I was just remarking that at some point later on algebraic geometry needs the notion of sheaf on something more general than a topological space

[Mario Carneiro]

but this part of the definition only needs a preorder

[Kenny Lau]

yeah, I was just remarking that at some point later on algebraic geometry needs the notion of sheaf on something more general than a topological space

what do you need?

[Kevin Buzzard]

sheaf on a site

[Reid Barton]

[category \a]

[Kenny Lau]

i.e. there may be more than one morphisms?

[Mario Carneiro]

if you want a category then this is just functor

[Reid Barton]

Right

[Kevin Buzzard]

but it has to satisfy the sheaf axiom

[Mario Carneiro]

point me to that

[Kevin Buzzard]

and you need more than a category to formalise that

[Kenny Lau]

@Mario Carneiro so they may have two "proofs" of x \le y and they want the two things to be unequal

[Reid Barton]

well, so far we are only talking about presheaf I thought

[Mario Carneiro]

I am actually very fine with that

[Kevin Buzzard]

that's true but I am interested in more than presheaves here

[Mario Carneiro]

that's the remaining problem with this definition

[Mario Carneiro]

as I said, I don't like proof args

[Reid Barton]

well then great! They won't be proofs once you generalize to a category :simple_smile:

[Mario Carneiro]

but you can't easily remove them from this... what's the structure of that argument otherwise?

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/00VH

[Mario Carneiro]

I guess Hom x y?

[Kevin Buzzard]

That's a site

[Reid Barton]

Right, just a morphism in some category.

[Kevin Buzzard]

Did you see https://stacks.math.columbia.edu/tag/00VI

[Kevin Buzzard]

Mario, I think this says "if a computer scientist tries to do this, they will have universe issues. But in all the cases that a mathematican cares about, these issues can be avoided and we can do everything in Type"

[Mario Carneiro]

Presheaves are already rather large

[Kevin Buzzard]

"This definition uses two universes u and v, but when we apply it I claim that we can get away with one universe"

[Kevin Buzzard]

How do you formalise that? ;-)

[Mario Carneiro]

It looks like sites have to be small though

[Mario Carneiro]

but what's a (pre)sheaf on a site?

[Mario Carneiro]

all I see is a bunch of covering stuff

[Kevin Buzzard]

Also relevant

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/00ZF

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/00VL

[Kevin Buzzard]

sheaf!

[Kevin Buzzard]

Still no presheaf :-)

[Johan Commelin]

Scott is doing sites in the his category stuff

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/00V1

[Mario Carneiro]

and what is the site corresponding to a top space?

[Kevin Buzzard]

OK so presheaf on a category, sheaf on a site

[Kevin Buzzard]

The site corresponding to a top space is this

[Kevin Buzzard]

The category has an object for each open set

[Kevin Buzzard]

Homs from U to V are empty unless V sub U in which case there is one elment

[Kevin Buzzard]

Coverings: a set of morphisms U_i -> U covers U iff the union of the image of the U_i is U

[Kevin Buzzard]

The sheaf axiom says this.

[Kevin Buzzard]

"If U is an open set, and it is covered by opens U_i, then to give a continuous function on U is to give a continuous function f_i on each U_i such that f_i and f_j agree on U_i intersect U_j"

[Reid Barton]

You can equivalently describe the category like this. The objects are topological spaces equipped with a map to X which is an open immersion. A morphism is a continuous map which is compatible with the structural maps to X.

[Kevin Buzzard]

They say "continuity can be checked locally"

[Mario Carneiro]

isn't that just true?

[Kevin Buzzard]

Reid's changing of my category to an equivalent category was something which turned out to be really important

[Mario Carneiro]

like as a statement of topology

[Kevin Buzzard]

It's precisely the statement that continuity is a local condition

[Kevin Buzzard]

So the presheaf of continuous functions on a topological space

[Kevin Buzzard]

is actually a sheaf!

[Kevin Buzzard]

But the presheaf of constant functions is not a sheaf

[Kevin Buzzard]

because if I have two disjoint open sets

[Kevin Buzzard]

and define a function to be 1 on one of them but 2 on the other one

[Kevin Buzzard]

it's locally constant

[Kevin Buzzard]

but not constant

[Mario Carneiro]

ah okay, so locally constant functions is a sheaf

[Kevin Buzzard]

right

[Kevin Buzzard]

it's the sheafification of the presheaf of constant functions

[Kevin Buzzard]

sheafification is an adjoint to the forgetful functor

[Mario Carneiro]

so how much does it matter that these are poset categories?

[Kevin Buzzard]

Exactly

[Kevin Buzzard]

it doesn't matter at all

[Kevin Buzzard]

and in general they won't be

[Kevin Buzzard]

is a poset category one where the hom sets have size <= 1?

[Mario Carneiro]

yes

[Kevin Buzzard]

so the etale site attached to a scheme does not have this property I guess

[Mario Carneiro]

maybe it would be better to do this with honest categories

[Kevin Buzzard]

I think Scott said that quite a long time ago

[Kevin Buzzard]

but I just wanted to get on

[Kevin Buzzard]

Sheaves of sets on a site are a Mathematician's Topos Mario.

[Kevin Buzzard]

This is distinct to the CS topos

[Mario Carneiro]

like in the literal sense?

[Kevin Buzzard]

You have some more general notion I think

[Kevin Buzzard]

Topos is used to mean two different things, I believe

[Kevin Buzzard]

I like Grothendieck topoi

[Kevin Buzzard]

you like elmentary topoi

[Mario Carneiro]

I am not sure I would say that...

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/00X9

[Mario Carneiro]

topoi is usually where I get off the bus

[Kevin Buzzard]

It took me a while, in the pre-Wikipedia age, to understand that the two uses of the word were distinct

[Kevin Buzzard]

I knew this guy as an UG who would go round saying "a topos is a category which is finitely complete, finitely cocomplete, has exponentiation and a subobject classifier"

[Kevin Buzzard]

and I had no idea what any of those things meant

[Kevin Buzzard]

and then years later I found some topoi I was actually interested in

[Mario Carneiro]

that's about where I am

[Kenny Lau]

as an UG :o

[Kevin Buzzard]

and then it turned out they were a different kind of topos

[Mario Carneiro]

I learn and forget those things every year

[Kevin Buzzard]

There was once some debate about whether Wiles/Taylor-Wiles used Grothendieck topoi in their proof of FLT

[Kevin Buzzard]

and the answer turned out to be

[Mario Carneiro]

because that means large universes, right?

[Kevin Buzzard]

"well, mathematicians are always a bit vague about what exactly they are using, and there is no mention of set-theoretic difficulties, but Brian Conrad went away and checked every single cohomology group in the entire proof and verified that it was OK, everything happened within one universe"

[Kevin Buzzard]

Wiles most definitely used etale cohomology in his proof

[Kevin Buzzard]

and I am almost certain that he cited some papers which at some point use flat cohomology

[Kevin Buzzard]

and they probably cite some papers which at some point mention fpqc cohomology

[Kevin Buzzard]

so we really needed an expert who could come along and say "I know exactly which parts of the theory of etale cohomlogy and other cohomology theories he used and can verify that all the stuff he uses can be formalised in ZFC"

[Kevin Buzzard]

before that debate died down

[Kevin Buzzard]

Some people really care about universes. If Lean really cannot keep track of them then these people might be skeptical

[Kevin Buzzard]

My current personal viewpoint on this is simply to accept the large cardinals. If they make maths easier and more fun to do then I'm in

[Mario Carneiro]

For the most part, if it lives in Type it can be constructed in ZFC

[Kevin Buzzard]

Right, but any file which uses "universes u v" is open to question right?

[Kevin Buzzard]

Or even "universe u" perhaps

[Kevin Buzzard]

if it uses Type as well

[Mario Carneiro]

no, as long as at the end you build something in Type

[Kevin Buzzard]

Oh

[Mario Carneiro]

The part which makes this not quite true is impredicativity of Prop

[Kevin Buzzard]

aie

[Kevin Buzzard]

so you get a proof which lived in another universe

[Kevin Buzzard]

but you can't get a proof in your own universe

[Kevin Buzzard]

so you use propext

[Kevin Buzzard]

cunning

[Mario Carneiro]

you can construct proofs of propositions in Prop in Type, which assert existence of large cardinals

[Kevin Buzzard]

ha ha

[Kevin Buzzard]

oh I hadn't realised that

[Kevin Buzzard]

Prop covers its tracks

[Mario Carneiro]

that's what impredicativity does for you

[Kevin Buzzard]

But still to construct the proof you need the extra universes, right?

[Kenny Lau]

is @Kevin Buzzard being impredicative?

[Mario Carneiro]

you could talk about configurations in Type 63 and it wouldn't make the proof large

[Kevin Buzzard]

I am just interested in exactly what can go wrong with regards to translating a DTT proof into ZFC

[Mario Carneiro]

right, there are large universes in the proof

[Kevin Buzzard]

Because one day someone serious is going to ask me about this

[Kenny Lau]

DTT

[Kenny Lau]

?

[Mario Carneiro]

so that wouldn't translate

[Mario Carneiro]

However, this sort of sleight of hand is very rare

[Kevin Buzzard]

And the problem is that the proof might not be mine

[Kevin Buzzard]

The theorem could be formulated about Type in some library

[Kenny Lau]

so they work in a system stronger than ZFC?

[Kenny Lau]

like how PA can't prove Goodstein?

[Kevin Buzzard]

and I never look at the proof

[Kevin Buzzard]

Yes Kenny

[Kevin Buzzard]

they work in ZFC + infinitely many inaccessible cardinals here

[Kevin Buzzard]

It's infinitely less likely to be consistent than ZFC

[Mario Carneiro]

which is weaker than Tarski Grothendieck set theory btw

[Kenny Lau]

Grothendieck?!

[Mario Carneiro]

which is what most category theorists use

[Mario Carneiro]

That is equivalent to ZFC + proper class of inaccessible cardinals

[Mario Carneiro]

here we only need omega many

[Kenny Lau]

fascinating

[Kenny Lau]

logic never fails to fascinate me

[Mario Carneiro]

and for any particular proof you can say "this used 3 universes" or such

[Mario Carneiro]

it's impossible to use all the universes in a proof

[Kevin Buzzard]

But I am specifically interested in the proofs which only use one universe

[Kevin Buzzard]

For example does FLT definitely only use one universe?

[Mario Carneiro]

well, actually you want zero universes

[Kevin Buzzard]

Oh yes I just want Type

[Mario Carneiro]

ZFC has zero universes

[Kenny Lau]

ZFC has zero universes

zero built-in universes

[Kevin Buzzard]

So currently the reference for "Wiles/TW proof of FLT is in ZFC" is "Email from Conrad"

[Mario Carneiro]

It's a bit tricky to work with DTT with zero universes

[Kevin Buzzard]

Why?

[Kevin Buzzard]

Say I globally exchange all the type u for type

[Kevin Buzzard]

how far do I get before the errors appear?

[Kevin Buzzard]

Start with core lean

[Mario Carneiro]

you have to be careful: Gamma |- A : Type is okay, but Type is not a type, in the sense Gamma |- Type : Type 1 doesn't exist

[Kevin Buzzard]

Yeah, I promise I will never ask Type its type.

[Kevin Buzzard]

ZFC people are used to making promises

[Kevin Buzzard]

and they're usually quite good at keeping them

[Kevin Buzzard]

This is the world I have lived in all my life

[Kevin Buzzard]

and you are claiming to offer me more

[Mario Carneiro]

Also you can have things like A : Type -> Type in ZFC

[Kevin Buzzard]

but I don't see anything of interest out there

[Mario Carneiro]

but again you can't quantify over them

[Kevin Buzzard]

Yes

[Kevin Buzzard]

no

[Kevin Buzzard]

oh wait

[Kevin Buzzard]

I can quantify over them

[Mario Carneiro]

A : (Type -> Type) -> Type is starting to get weird

[Mario Carneiro]

A : Type -> Type is a proper class function

[Kevin Buzzard]

I just have to write some footnote explaining about how it can all be done properly if you ask a set theorist

[Kevin Buzzard]

because no object I consider in my paper has size greater than 2^2^2^2^aleph_0 so it's all OK

[Kevin Buzzard]

who needs inaccessible cardinals

[Kevin Buzzard]

I just something closed under a few iterations of the power set axiom and I'll be fine

[Mario Carneiro]

That's really hard to do formally

[Kevin Buzzard]

There will be people out there who care about this.

[Mario Carneiro]

at least if you didn't literally do that in the proof

[Kevin Buzzard]

Right, and who wants to do that?

[Kevin Buzzard]

We just wanna have fun

[Kevin Buzzard]

I don't see any reason why ZFC should stay as the prevalent model of mathematics

[Mario Carneiro]

What you want is a way to take a proof and shrink all the things in it to ZFC things

[Kevin Buzzard]

but without a doubt it is the prevalent model of mathematics

[Kevin Buzzard]

I don't

[Kevin Buzzard]

but some people might

[Kevin Buzzard]

and I have them in mind

[Mario Carneiro]

or 2^2^2^2^aleph_0 things

[Mario Carneiro]

and it's my job to figure out how to make sense of your request

[Kevin Buzzard]

There are theorems of the form "if you proved X using 3 universes then you could have done it in ZFC" I think

[Kevin Buzzard]

I think someone might have told me that even though wiles certainly used AC in his proof, FLT was now known to be a theorem of ZF

[Kevin Buzzard]

because one of these magic meta-theorem things

[Mario Carneiro]

yes, it's a pi01 statement so magic happens

[Mario Carneiro]

here's the sheaf axiom using the poset presheaf definition:

def gluing {α} [complete_lattice α] (F : order_presheaf α)
  (X : α) {ι : Type*} (Y : ι → α) (Hcov : X = ⨆ i, Y i)
  (r : F.F X) :
  {a : Π i, F.F (Y i) | ∀ (i j : ι),
    F.res (Y i ⊓ Y j) inf_le_left (a i) =
    F.res (Y i ⊓ Y j) inf_le_right (a j) } :=
⟨λ i, F.res (Y i) (by rw Hcov; apply le_supr) r,
 λ i j, by simp [F.comp]⟩

def is_order_sheaf {α : Type u} [complete_lattice α]
  (F : order_presheaf α) : Prop :=
∀ (X : α) {ι : Type u} (Y : ι → α) (Hcov : X = ⨆ i, Y i),
function.bijective (gluing F X Y Hcov)

[Kevin Buzzard]

Did you look at what I did?

[Mario Carneiro]

yes, it was based on your definition

[Kevin Buzzard]

ha ha hope I didn't make a mistake :-)

[Mario Carneiro]

I think probably bijective makes more axioms than you really need here

[Mario Carneiro]

like it's probably already injective

[Mario Carneiro]

I would just state the actual condition you want, and prove it implies this function is bijective

[Kevin Buzzard]

https://stacks.math.columbia.edu/tag/009I

[Kevin Buzzard]

Actually I guess I just copied everything from the stacks project (and spotted a mistake or two along the way :-) )

[Kevin Buzzard]

no, injective needs checking

[Kevin Buzzard]

A presheaf is just a functor

[Kevin Buzzard]

It takes an open set to a type

[Kevin Buzzard]

I could easily replace its value on X with some gigantic type that maps to the old value

[Kevin Buzzard]

If you think of them as sheaves of functions then injectivity may well be obvious

[Kevin Buzzard]

but this is a true pi type -- it takes an open set to a random type, not functions on U or anything

[Kevin Buzzard]

and res is part of the data, not restriction of functions

[Kevin Buzzard]

So are you interested in putting this presheaf and sheaf stuff in mathlib?

[Kevin Buzzard]

I'm not bothered either way

[Mario Carneiro]

but it is compositional

[Kevin Buzzard]

yes but that's an axiom

[Kevin Buzzard]

one of the two axioms of functor

[Mario Carneiro]

Of course, I'm assuming it's a presheaf already

[Kevin Buzzard]

gotcha

[Kevin Buzzard]

I don't know whether I should bother tidying everything up

[Mario Carneiro]

I mean the condition of being a sheaf can be stated more directly given it's a presheaf

[Kevin Buzzard]

right

[Kevin Buzzard]

but you still don't get injectivity for free

[Kevin Buzzard]

because I can replace F X

[Kevin Buzzard]

with with a random type Y that mapped to the old F X

[Kevin Buzzard]

X the whole space

[Kevin Buzzard]

and then it's still a presheaf

[Kevin Buzzard]

but there's no reason Y -> old F X is injective

[Kevin Buzzard]

so I broke the sheaf property precisely by breaking injectivity

[Sean Leather]

@Kevin Buzzard Re: @[simp] and left-to-right rewriting, perhaps, by browsing through the @[simp] theorems in this file, you can get an idea of why they are structured the way they are.