## Stream: maths

### Topic: valuations

#### Kevin Buzzard (May 25 2018 at 22:47):

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 (May 25 2018 at 22:48):

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

#### Kevin Buzzard (May 25 2018 at 22:49):

(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 (May 25 2018 at 23:20):

I have approximately this lying around somewhere

#### Reid Barton (May 25 2018 at 23:27):

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

#### Reid Barton (May 25 2018 at 23:28):

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

#### Kevin Buzzard (May 25 2018 at 23:37):

line 91 should now be

#### Kevin Buzzard (May 25 2018 at 23:37):

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

#### Kevin Buzzard (May 25 2018 at 23:37):

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

#### Kevin Buzzard (May 25 2018 at 23:40):

Thanks so much! This is exactly what I wanted!

#### Kevin Buzzard (May 25 2018 at 23:40):

What a great little community we are getting here!

#### Kevin Buzzard (May 25 2018 at 23:41):

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

#### Kevin Buzzard (May 25 2018 at 23:42):

Is there a better way of doing things?

#### Reid Barton (May 25 2018 at 23:53):

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

#### Kevin Buzzard (May 26 2018 at 00:02):

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

#### Kevin Buzzard (May 26 2018 at 00:03):

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 (May 26 2018 at 00:04):

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 (May 26 2018 at 00:09):

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 (May 26 2018 at 00:09):

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

#### Kevin Buzzard (May 26 2018 at 00:10):

Is ord_pow broken?

#### Kevin Buzzard (May 26 2018 at 00:10):

Or did I break it myself?

#### Reid Barton (May 26 2018 at 00:11):

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

#### Kevin Buzzard (May 26 2018 at 00:11):

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

#### Kevin Buzzard (May 26 2018 at 00:11):

I just can't even guess what it would be

#### Kevin Buzzard (May 26 2018 at 00:11):

"any one of a couple of random examples"

#### Kevin Buzzard (May 26 2018 at 00:14):

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

:-)

#### Kevin Buzzard (May 26 2018 at 00:14):

I think some coercion magic happened?

#### Kevin Buzzard (May 26 2018 at 00:58):

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 (May 26 2018 at 00:59):

it's called the ordinal omega+1 :D

:D

#### Kevin Buzzard (May 26 2018 at 01:01):

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

#### Kevin Buzzard (May 26 2018 at 01:03):

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

#### Kevin Buzzard (May 26 2018 at 01:04):

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 (May 26 2018 at 01:05):

@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 (May 26 2018 at 01:07):

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 (May 26 2018 at 01:07):

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

#### Kevin Buzzard (May 26 2018 at 01:07):

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

#### Kevin Buzzard (May 26 2018 at 01:08):

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

#### Andrew Ashworth (May 26 2018 at 01:12):

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

#### Kevin Buzzard (May 26 2018 at 01:13):

They start 2nd July

#### Kevin Buzzard (May 26 2018 at 01:13):

It's going to be a crazy summer!

2 months!

#### Kevin Buzzard (May 26 2018 at 01:39):

I am so rubbish at coe

#### Kevin Buzzard (May 26 2018 at 01:39):

@[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 (May 26 2018 at 01:39):

This is Reid's pgcd from his gist from earlier

#### Kevin Buzzard (May 26 2018 at 02:01):

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

#### Mario Carneiro (May 26 2018 at 02:06):

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 (May 26 2018 at 02:14):

wow what a coincidence lol

#### Mario Carneiro (May 26 2018 at 02:28):

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 (May 26 2018 at 02:30):

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 (May 26 2018 at 02:34):

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 (May 26 2018 at 02:35):

@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 (May 26 2018 at 02:39):

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 (May 26 2018 at 02:40):

This could be used to factor ennreal into with_top nnreal

#### Kenny Lau (May 26 2018 at 02:41):

rip ennreal 2017-2018

#### Kenny Lau (May 26 2018 at 02:42):

born Aug 30, 2017

#### Mario Carneiro (May 26 2018 at 02:42):

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 (May 26 2018 at 02:43):

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 (May 27 2018 at 13:00):

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 (May 27 2018 at 13:00):

You might find that if proofs of positivity are carried around

#### Kevin Buzzard (May 27 2018 at 13:01):

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

#### Kevin Buzzard (May 27 2018 at 13:01):

then the coercions work fine.

#### Kevin Buzzard (May 27 2018 at 13:01):

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

#### Kevin Buzzard (May 27 2018 at 13:02):

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 (May 27 2018 at 13:03):

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

#### Mario Carneiro (May 27 2018 at 13:10):

this isn't how coercions work

#### Mario Carneiro (May 27 2018 at 13:10):

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

#### Mario Carneiro (May 27 2018 at 13:10):

in particular, coercions cannot be partial

#### Mario Carneiro (May 27 2018 at 13:10):

except the coercion Prop -> bool which is magical

#### Kevin Buzzard (May 27 2018 at 13:32):

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

rfl

#### Kevin Buzzard (May 27 2018 at 13:32):

I was trying not to use rfl

#### Kevin Buzzard (May 27 2018 at 13:32):

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

#### Kevin Buzzard (May 27 2018 at 13:33):

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

#### Kevin Buzzard (May 27 2018 at 13:33):

Actually I don't understand.

#### Kevin Buzzard (May 27 2018 at 13:33):

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

Wait

#### Kevin Buzzard (May 27 2018 at 13:33):

I was asking for the name of the theorem

not the proof

#### Mario Carneiro (May 27 2018 at 13:34):

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

#### Kevin Buzzard (May 27 2018 at 13:34):

I'll formulate something precise.

#### Mario Carneiro (May 27 2018 at 13:34):

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

#### Mario Carneiro (May 27 2018 at 13:35):

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

#### Kevin Buzzard (May 27 2018 at 13:35):

[pause whilst we discover if Kevin is talking nonsense]

#### Kevin Buzzard (May 27 2018 at 13:41):

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


The question.

#### Kevin Buzzard (May 27 2018 at 13:42):

because I want to use you in a rewrite

#### Kevin Buzzard (May 27 2018 at 13:42):

so I need to know your name

#### Mario Carneiro (May 27 2018 at 13:42):

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

#### Kevin Buzzard (May 27 2018 at 13:43):

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

#### Mario Carneiro (May 27 2018 at 13:43):

same as how beta reduction isn't a named theorem

dsimp is what?

#### Kevin Buzzard (May 27 2018 at 13:43):

I used it a couple of times recently

#### Kevin Buzzard (May 27 2018 at 13:43):

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

#### Mario Carneiro (May 27 2018 at 13:44):

it's simp for definitional rewrites

#### Kevin Buzzard (May 27 2018 at 13:44):

which way does it go?

#### Kevin Buzzard (May 27 2018 at 13:44):

What does it actually do?

#### Kevin Buzzard (May 27 2018 at 13:44):

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

#### Kevin Buzzard (May 27 2018 at 13:44):

but does it ever add it?

#### Mario Carneiro (May 27 2018 at 13:44):

it does exactly the same sort of thing as simp

oh great :-)

#### Kevin Buzzard (May 27 2018 at 13:45):

Another black box :-)

I see

#### Mario Carneiro (May 27 2018 at 13:45):

it cancels projections applied to structure mk

#### Kevin Buzzard (May 27 2018 at 13:45):

What else does it do?

#### Mario Carneiro (May 27 2018 at 13:45):

this is the structure iota rule

#### Kevin Buzzard (May 27 2018 at 13:45):

What's a complete list of what it does?

#### Kevin Buzzard (May 27 2018 at 13:45):

Would I be able to understand the source code?

#### Kevin Buzzard (May 27 2018 at 13:45):

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

#### Mario Carneiro (May 27 2018 at 13:46):

dsimp has a config too

#### Kevin Buzzard (May 27 2018 at 13:46):

53 extra options?

#### Mario Carneiro (May 27 2018 at 13:46):

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

#### Mario Carneiro (May 27 2018 at 13:47):

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

#### Mario Carneiro (May 27 2018 at 13:47):

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

#### Kevin Buzzard (May 27 2018 at 13:47):

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 (May 27 2018 at 13:48):

Haven't we had this conversation before?

#### Mario Carneiro (May 27 2018 at 13:48):

I'm pretty sure you wrote that article

#### Kevin Buzzard (May 27 2018 at 13:48):

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

#### Kevin Buzzard (May 27 2018 at 13:48):

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

#### Andrew Ashworth (May 27 2018 at 13:50):

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

#### Nicholas Scheel (May 27 2018 at 13:52):

simplification using definition equalities, I believe

#### Kevin Buzzard (May 27 2018 at 13:54):

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 (May 27 2018 at 13:55):

change with is literally definitional rw

#### Kevin Buzzard (May 27 2018 at 13:55):

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 (May 27 2018 at 13:56):

but dsimp is nice for just cleaning up some common patterns

#### Kevin Buzzard (May 27 2018 at 13:56):

Equality is asymmetric for you people, isn't it

#### Kevin Buzzard (May 27 2018 at 13:57):

This is only just dawning on me

#### Mario Carneiro (May 27 2018 at 13:57):

yes, with term rewrites direction really matters

#### Kevin Buzzard (May 27 2018 at 13:57):

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

#### Kevin Buzzard (May 27 2018 at 13:57):

you would put the more complicated side first

#### Kevin Buzzard (May 27 2018 at 13:57):

Is this just some general principle?

#### Mario Carneiro (May 27 2018 at 13:57):

yeah, simp simplifies

#### Mario Carneiro (May 27 2018 at 13:58):

it's not called complexify

#### Kevin Buzzard (May 27 2018 at 13:58):

I had not realised that = was asymmetric

#### Kevin Buzzard (May 27 2018 at 13:58):

in any way whatsoever

#### Kevin Buzzard (May 27 2018 at 13:58):

I have a different definition of = to you

#### Mario Carneiro (May 27 2018 at 13:58):

= itself is symmetric

#### Kevin Buzzard (May 27 2018 at 13:58):

symmetric in some theorem sense

#### Kevin Buzzard (May 27 2018 at 13:59):

but you have to decide which goes first

#### Kevin Buzzard (May 27 2018 at 13:59):

and we don't care

#### Mario Carneiro (May 27 2018 at 13:59):

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

#### Mario Carneiro (May 27 2018 at 13:59):

and this is directed

#### Kevin Buzzard (May 27 2018 at 13:59):

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

Aah!

#### Kevin Buzzard (May 27 2018 at 14:00):

I've just realised what my question actually is.

#### Kevin Buzzard (May 27 2018 at 14:00):

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 (May 27 2018 at 14:01):

Unfortunately, the answer is "depends on the structure"

#### Mario Carneiro (May 27 2018 at 14:01):

some axioms of a structure should be simp lemmas

subtype

#### Mario Carneiro (May 27 2018 at 14:01):

like zero_add

#### Kevin Buzzard (May 27 2018 at 14:01):

A type and a proof

#### Mario Carneiro (May 27 2018 at 14:02):

I don't think subtype has any simp lemmas

#### Mario Carneiro (May 27 2018 at 14:02):

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

#### Mario Carneiro (May 27 2018 at 14:02):

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

#### Kevin Buzzard (May 27 2018 at 14:03):

What about presheaf of types on a topological space?

#### Mario Carneiro (May 27 2018 at 14:03):

but actually I think simp might do that automatically anyway

#### Mario Carneiro (May 27 2018 at 14:04):

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

#### Kevin Buzzard (May 27 2018 at 14:05):

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

#### Kevin Buzzard (May 27 2018 at 14:05):

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

#### Kevin Buzzard (May 27 2018 at 14:05):

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 (May 27 2018 at 14:05):

that's just what I would have recommended

#### Mario Carneiro (May 27 2018 at 14:06):

except possibly for the dependent args

#### Kevin Buzzard (May 27 2018 at 14:06):

You would recommend the change in the structure?

#### Mario Carneiro (May 27 2018 at 14:06):

that doesn't matter so much

Oh!

#### Kevin Buzzard (May 27 2018 at 14:06):

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

#### Kevin Buzzard (May 27 2018 at 14:07):

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 (May 27 2018 at 14:07):

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

#### Mario Carneiro (May 27 2018 at 14:07):

so it depends on how you usually prove such goals

#### Kevin Buzzard (May 27 2018 at 14:07):

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

#### Mario Carneiro (May 27 2018 at 14:08):

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

#### Kevin Buzzard (May 27 2018 at 14:08):

Note the equality "f = g circ h"

#### Kevin Buzzard (May 27 2018 at 14:08):

the more complicated side on the right

#### Kevin Buzzard (May 27 2018 at 14:08):

is that also unwise?

#### Mario Carneiro (May 27 2018 at 14:08):

actually here I recommend that ordering

#### Kevin Buzzard (May 27 2018 at 14:08):

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 (May 27 2018 at 14:08):

because the argument to f is getting simpler

boggle

#### Kevin Buzzard (May 27 2018 at 14:09):

I don't understand

#### Mario Carneiro (May 27 2018 at 14:09):

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

#### Mario Carneiro (May 27 2018 at 14:10):

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

#### Kevin Buzzard (May 27 2018 at 14:10):

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

#### Kevin Buzzard (May 27 2018 at 14:10):

that's what it is really

#### Kevin Buzzard (May 27 2018 at 14:10):

You still want it that way round?

#### Mario Carneiro (May 27 2018 at 14:11):

that's not a good simp lemma

#### Kevin Buzzard (May 27 2018 at 14:11):

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

#### Kevin Buzzard (May 27 2018 at 14:11):

Either way round?

#### Mario Carneiro (May 27 2018 at 14:12):

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

#### Mario Carneiro (May 27 2018 at 14:12):

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

#### Kevin Buzzard (May 27 2018 at 14:12):

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 (May 27 2018 at 14:13):

Aah so you do want to switch the order?

#### Kevin Buzzard (May 27 2018 at 14:13):

And then make a simp lemma?

#### Kevin Buzzard (May 27 2018 at 14:14):

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 (May 27 2018 at 14:15):

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

#### Mario Carneiro (May 27 2018 at 14:15):

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

Why?

#### Kevin Buzzard (May 27 2018 at 14:16):

proof args are fundamental statements about the situation

#### Kevin Buzzard (May 27 2018 at 14:17):

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

#### Kevin Buzzard (May 27 2018 at 14:18):

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

#### Kevin Buzzard (May 27 2018 at 14:19):

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

#### Mario Carneiro (May 27 2018 at 14:19):

assoc is a special case

boggle

#### Kevin Buzzard (May 27 2018 at 14:19):

I'll add it to the docs

#### Mario Carneiro (May 27 2018 at 14:19):

simp has special handling for comm/assoc operations

#### Kevin Buzzard (May 27 2018 at 14:20):

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

#### Mario Carneiro (May 27 2018 at 14:20):

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

#### Kevin Buzzard (May 27 2018 at 14:20):

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

#### Mario Carneiro (May 27 2018 at 14:21):

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 (May 27 2018 at 14:21):

None of those have proof args

oh

#### Mario Carneiro (May 27 2018 at 14:21):

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

#### Mario Carneiro (May 27 2018 at 14:22):

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

#### Kevin Buzzard (May 27 2018 at 14:22):

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

#### Mario Carneiro (May 27 2018 at 14:22):

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

#### Kevin Buzzard (May 27 2018 at 14:23):

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

yes

#### Mario Carneiro (May 27 2018 at 14:24):

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

#### Kevin Buzzard (May 27 2018 at 14:24):

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 (May 27 2018 at 14:25):

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

#### Kevin Buzzard (May 27 2018 at 14:25):

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

#### Kevin Buzzard (May 27 2018 at 14:25):

so I was forced to learn the system

#### Kevin Buzzard (May 27 2018 at 14:25):

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

Ok so coercions.

#### Kevin Buzzard (May 27 2018 at 14:32):

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

#### Kevin Buzzard (May 27 2018 at 14:32):

That's not good, right?

#### Kevin Buzzard (May 27 2018 at 14:32):

Should that be a simp lemma?

#### Kevin Buzzard (May 27 2018 at 14:33):

ℕ+ is one of my favourite sets in ZFC

#### Kevin Buzzard (May 27 2018 at 14:34):

Why is it so hard to work with here?

#### Kevin Buzzard (May 27 2018 at 14:34):

Just because it's not a stupid semiring

#### Kevin Buzzard (May 27 2018 at 14:34):

maybe it's a demisemiring

#### Mario Carneiro (May 27 2018 at 14:35):

that is a simp lemma, I think

#### Kevin Buzzard (May 27 2018 at 14:35):

Aah here's a question.

#### Kevin Buzzard (May 27 2018 at 14:35):

Let's say we ripped out the definition of pnat

#### Mario Carneiro (May 27 2018 at 14:35):

coe_nat_coe

#### Kevin Buzzard (May 27 2018 at 14:36):

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

#### Kevin Buzzard (May 27 2018 at 14:36):

Would that make any difference to anything

not really

#### Kevin Buzzard (May 27 2018 at 14:36):

or you just write the new interface

and that's it

#### Kevin Buzzard (May 27 2018 at 14:36):

No issue with compile time or running time

#### Kevin Buzzard (May 27 2018 at 14:36):

or simp not working as well

#### Mario Carneiro (May 27 2018 at 14:36):

anything not using the interface would be affected, of course

Aah

#### Kevin Buzzard (May 27 2018 at 14:37):

anything accessing the innards of the structure

#### Mario Carneiro (May 27 2018 at 14:37):

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

#### Kevin Buzzard (May 27 2018 at 14:37):

then they should be punished?

#### Kevin Buzzard (May 27 2018 at 14:37):

How does that work?

#### Kevin Buzzard (May 27 2018 at 14:38):

"You only use official constructors"

#### Kevin Buzzard (May 27 2018 at 14:38):

"not inbuilt stuff"

#### Kevin Buzzard (May 27 2018 at 14:38):

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

#### Kevin Buzzard (May 27 2018 at 14:39):

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

right

eew

#### Mario Carneiro (May 27 2018 at 14:39):

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

#### Kevin Buzzard (May 27 2018 at 14:39):

So there is a question left

#### Mario Carneiro (May 27 2018 at 14:39):

you can't replicate that functionality with an interface

#### Mario Carneiro (May 27 2018 at 14:40):

unless the interface is to pass in a specially defined structure

like simp_config

#### Kevin Buzzard (May 27 2018 at 14:40):

you've lost me now

#### Kevin Buzzard (May 27 2018 at 14:41):

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 (May 27 2018 at 14:41):

maybe order irrelevant

#### Kevin Buzzard (May 27 2018 at 14:41):

but you never know

yes

#### Mario Carneiro (May 27 2018 at 14:41):

order is relevant for anonymous constructors

#### Mario Carneiro (May 27 2018 at 14:42):

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 (May 27 2018 at 14:42):

what is an order_presheaf?

#### Kevin Buzzard (May 27 2018 at 14:43):

Would you want presheaves in mathlib?

oh eew

#### Kevin Buzzard (May 27 2018 at 14:43):

what just happened there

#### Kevin Buzzard (May 27 2018 at 14:43):

with the open sets

#### Kenny Lau (May 27 2018 at 14:43):

oh, they form a preorder under inclusion!

#### Kevin Buzzard (May 27 2018 at 14:43):

he thinks he's being clever

#### Kevin Buzzard (May 27 2018 at 14:43):

but we need the etale site ;-)

#### Kevin Buzzard (May 27 2018 at 14:44):

so he's still not general enough ;-)

#### Mario Carneiro (May 27 2018 at 14:44):

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

#### Kevin Buzzard (May 27 2018 at 14:44):

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 (May 27 2018 at 14:44):

but this part of the definition only needs a preorder

#### Kenny Lau (May 27 2018 at 14:45):

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?

sheaf on a site

#### Reid Barton (May 27 2018 at 14:45):

[category \a]

#### Kenny Lau (May 27 2018 at 14:45):

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

#### Mario Carneiro (May 27 2018 at 14:45):

if you want a category then this is just functor

Right

#### Kevin Buzzard (May 27 2018 at 14:45):

but it has to satisfy the sheaf axiom

point me to that

#### Kevin Buzzard (May 27 2018 at 14:46):

and you need more than a category to formalise that

#### Kenny Lau (May 27 2018 at 14:46):

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

#### Reid Barton (May 27 2018 at 14:46):

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

#### Mario Carneiro (May 27 2018 at 14:46):

I am actually very fine with that

#### Kevin Buzzard (May 27 2018 at 14:46):

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

#### Mario Carneiro (May 27 2018 at 14:46):

that's the remaining problem with this definition

#### Mario Carneiro (May 27 2018 at 14:46):

as I said, I don't like proof args

#### Reid Barton (May 27 2018 at 14:47):

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

#### Mario Carneiro (May 27 2018 at 14:47):

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

#### Kevin Buzzard (May 27 2018 at 14:47):

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

#### Mario Carneiro (May 27 2018 at 14:47):

I guess Hom x y?

That's a site

#### Reid Barton (May 27 2018 at 14:48):

Right, just a morphism in some category.

#### Kevin Buzzard (May 27 2018 at 14:49):

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

#### Kevin Buzzard (May 27 2018 at 14:50):

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"

#### Kevin Buzzard (May 27 2018 at 14:51):

"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 (May 27 2018 at 14:51):

How do you formalise that? ;-)

#### Mario Carneiro (May 27 2018 at 14:52):

It looks like sites have to be small though

#### Mario Carneiro (May 27 2018 at 14:52):

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

#### Mario Carneiro (May 27 2018 at 14:52):

all I see is a bunch of covering stuff

Also relevant

#### Kevin Buzzard (May 27 2018 at 14:53):

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

#### Kevin Buzzard (May 27 2018 at 14:54):

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

sheaf!

#### Kevin Buzzard (May 27 2018 at 14:54):

Still no presheaf :-)

#### Johan Commelin (May 27 2018 at 14:54):

Scott is doing sites in the his category stuff

#### Kevin Buzzard (May 27 2018 at 14:54):

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

#### Mario Carneiro (May 27 2018 at 14:54):

and what is the site corresponding to a top space?

#### Kevin Buzzard (May 27 2018 at 14:54):

OK so presheaf on a category, sheaf on a site

#### Kevin Buzzard (May 27 2018 at 14:55):

The site corresponding to a top space is this

#### Kevin Buzzard (May 27 2018 at 14:55):

The category has an object for each open set

#### Kevin Buzzard (May 27 2018 at 14:55):

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

#### Kevin Buzzard (May 27 2018 at 14:55):

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

#### Kevin Buzzard (May 27 2018 at 14:56):

The sheaf axiom says this.

#### Kevin Buzzard (May 27 2018 at 14:56):

"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 (May 27 2018 at 14:57):

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 (May 27 2018 at 14:57):

They say "continuity can be checked locally"

#### Mario Carneiro (May 27 2018 at 14:58):

isn't that just true?

#### Kevin Buzzard (May 27 2018 at 14:58):

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

#### Mario Carneiro (May 27 2018 at 14:58):

like as a statement of topology

#### Kevin Buzzard (May 27 2018 at 14:58):

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

#### Kevin Buzzard (May 27 2018 at 14:58):

So the presheaf of continuous functions on a topological space

#### Kevin Buzzard (May 27 2018 at 14:58):

is actually a sheaf!

#### Kevin Buzzard (May 27 2018 at 14:58):

But the presheaf of constant functions is not a sheaf

#### Kevin Buzzard (May 27 2018 at 14:59):

because if I have two disjoint open sets

#### Kevin Buzzard (May 27 2018 at 14:59):

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

#### Kevin Buzzard (May 27 2018 at 14:59):

it's locally constant

but not constant

#### Mario Carneiro (May 27 2018 at 14:59):

ah okay, so locally constant functions is a sheaf

right

#### Kevin Buzzard (May 27 2018 at 14:59):

it's the sheafification of the presheaf of constant functions

#### Kevin Buzzard (May 27 2018 at 14:59):

sheafification is an adjoint to the forgetful functor

#### Mario Carneiro (May 27 2018 at 15:00):

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

Exactly

#### Kevin Buzzard (May 27 2018 at 15:00):

it doesn't matter at all

#### Kevin Buzzard (May 27 2018 at 15:00):

and in general they won't be

#### Kevin Buzzard (May 27 2018 at 15:00):

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

yes

#### Kevin Buzzard (May 27 2018 at 15:01):

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

#### Mario Carneiro (May 27 2018 at 15:01):

maybe it would be better to do this with honest categories

#### Kevin Buzzard (May 27 2018 at 15:02):

I think Scott said that quite a long time ago

#### Kevin Buzzard (May 27 2018 at 15:02):

but I just wanted to get on

#### Kevin Buzzard (May 27 2018 at 15:02):

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

#### Kevin Buzzard (May 27 2018 at 15:02):

This is distinct to the CS topos

#### Mario Carneiro (May 27 2018 at 15:03):

like in the literal sense?

#### Kevin Buzzard (May 27 2018 at 15:03):

You have some more general notion I think

#### Kevin Buzzard (May 27 2018 at 15:03):

Topos is used to mean two different things, I believe

#### Kevin Buzzard (May 27 2018 at 15:03):

I like Grothendieck topoi

#### Kevin Buzzard (May 27 2018 at 15:03):

you like elmentary topoi

#### Mario Carneiro (May 27 2018 at 15:03):

I am not sure I would say that...

#### Kevin Buzzard (May 27 2018 at 15:03):

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

#### Mario Carneiro (May 27 2018 at 15:04):

topoi is usually where I get off the bus

#### Kevin Buzzard (May 27 2018 at 15:04):

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

#### Kevin Buzzard (May 27 2018 at 15:04):

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 (May 27 2018 at 15:04):

and I had no idea what any of those things meant

#### Kevin Buzzard (May 27 2018 at 15:05):

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

as an UG :o

#### Kevin Buzzard (May 27 2018 at 15:05):

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

#### Mario Carneiro (May 27 2018 at 15:05):

I learn and forget those things every year

#### Kevin Buzzard (May 27 2018 at 15:06):

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

#### Kevin Buzzard (May 27 2018 at 15:06):

and the answer turned out to be

#### Mario Carneiro (May 27 2018 at 15:06):

because that means large universes, right?

#### Kevin Buzzard (May 27 2018 at 15:07):

"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 (May 27 2018 at 15:07):

Wiles most definitely used etale cohomology in his proof

#### Kevin Buzzard (May 27 2018 at 15:07):

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

#### Kevin Buzzard (May 27 2018 at 15:08):

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

#### Kevin Buzzard (May 27 2018 at 15:09):

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 (May 27 2018 at 15:09):

before that debate died down

#### Kevin Buzzard (May 27 2018 at 15:11):

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

#### Kevin Buzzard (May 27 2018 at 15:11):

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 (May 27 2018 at 15:11):

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

#### Kevin Buzzard (May 27 2018 at 15:12):

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

#### Kevin Buzzard (May 27 2018 at 15:12):

Or even "universe u" perhaps

#### Kevin Buzzard (May 27 2018 at 15:12):

if it uses Type as well

#### Mario Carneiro (May 27 2018 at 15:12):

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

Oh

#### Mario Carneiro (May 27 2018 at 15:12):

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

aie

#### Kevin Buzzard (May 27 2018 at 15:13):

so you get a proof which lived in another universe

#### Kevin Buzzard (May 27 2018 at 15:13):

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

#### Kevin Buzzard (May 27 2018 at 15:13):

so you use propext

cunning

#### Mario Carneiro (May 27 2018 at 15:13):

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

ha ha

#### Kevin Buzzard (May 27 2018 at 15:13):

Prop covers its tracks

#### Mario Carneiro (May 27 2018 at 15:13):

that's what impredicativity does for you

#### Kevin Buzzard (May 27 2018 at 15:14):

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

#### Kenny Lau (May 27 2018 at 15:14):

is @Kevin Buzzard being impredicative?

#### Mario Carneiro (May 27 2018 at 15:14):

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

#### Kevin Buzzard (May 27 2018 at 15:15):

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

#### Mario Carneiro (May 27 2018 at 15:15):

right, there are large universes in the proof

DTT

?

#### Mario Carneiro (May 27 2018 at 15:15):

so that wouldn't translate

#### Mario Carneiro (May 27 2018 at 15:15):

However, this sort of sleight of hand is very rare

#### Kevin Buzzard (May 27 2018 at 15:15):

And the problem is that the proof might not be mine

#### Kevin Buzzard (May 27 2018 at 15:15):

The theorem could be formulated about Type in some library

#### Kenny Lau (May 27 2018 at 15:15):

so they work in a system stronger than ZFC?

#### Kenny Lau (May 27 2018 at 15:15):

like how PA can't prove Goodstein?

#### Kevin Buzzard (May 27 2018 at 15:15):

and I never look at the proof

Yes Kenny

#### Kevin Buzzard (May 27 2018 at 15:16):

they work in ZFC + infinitely many inaccessible cardinals here

#### Kevin Buzzard (May 27 2018 at 15:16):

It's infinitely less likely to be consistent than ZFC

#### Mario Carneiro (May 27 2018 at 15:16):

which is weaker than Tarski Grothendieck set theory btw

Grothendieck?!

#### Mario Carneiro (May 27 2018 at 15:16):

which is what most category theorists use

#### Mario Carneiro (May 27 2018 at 15:17):

That is equivalent to ZFC + proper class of inaccessible cardinals

#### Mario Carneiro (May 27 2018 at 15:17):

here we only need omega many

fascinating

#### Kenny Lau (May 27 2018 at 15:17):

logic never fails to fascinate me

#### Mario Carneiro (May 27 2018 at 15:17):

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

#### Mario Carneiro (May 27 2018 at 15:18):

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

#### Kevin Buzzard (May 27 2018 at 15:18):

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

#### Kevin Buzzard (May 27 2018 at 15:18):

For example does FLT definitely only use one universe?

#### Mario Carneiro (May 27 2018 at 15:18):

well, actually you want zero universes

#### Kevin Buzzard (May 27 2018 at 15:18):

Oh yes I just want Type

#### Mario Carneiro (May 27 2018 at 15:18):

ZFC has zero universes

#### Kenny Lau (May 27 2018 at 15:19):

ZFC has zero universes

zero built-in universes

#### Kevin Buzzard (May 27 2018 at 15:19):

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

#### Mario Carneiro (May 27 2018 at 15:19):

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

Why?

#### Kevin Buzzard (May 27 2018 at 15:19):

Say I globally exchange all the type u for type

#### Kevin Buzzard (May 27 2018 at 15:19):

how far do I get before the errors appear?

#### Mario Carneiro (May 27 2018 at 15:20):

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 (May 27 2018 at 15:20):

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

#### Kevin Buzzard (May 27 2018 at 15:20):

ZFC people are used to making promises

#### Kevin Buzzard (May 27 2018 at 15:21):

and they're usually quite good at keeping them

#### Kevin Buzzard (May 27 2018 at 15:21):

This is the world I have lived in all my life

#### Kevin Buzzard (May 27 2018 at 15:21):

and you are claiming to offer me more

#### Mario Carneiro (May 27 2018 at 15:21):

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

#### Kevin Buzzard (May 27 2018 at 15:21):

but I don't see anything of interest out there

#### Mario Carneiro (May 27 2018 at 15:21):

but again you can't quantify over them

Yes

no

oh wait

#### Kevin Buzzard (May 27 2018 at 15:22):

I can quantify over them

#### Mario Carneiro (May 27 2018 at 15:22):

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

#### Mario Carneiro (May 27 2018 at 15:22):

A : Type -> Type is a proper class function

#### Kevin Buzzard (May 27 2018 at 15:22):

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

#### Kevin Buzzard (May 27 2018 at 15:22):

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 (May 27 2018 at 15:23):

who needs inaccessible cardinals

#### Kevin Buzzard (May 27 2018 at 15:23):

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

#### Mario Carneiro (May 27 2018 at 15:23):

That's really hard to do formally

#### Mario Carneiro (May 27 2018 at 15:23):

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

#### Kevin Buzzard (May 27 2018 at 15:23):

Right, and who wants to do that?

#### Kevin Buzzard (May 27 2018 at 15:23):

We just wanna have fun

#### Kevin Buzzard (May 27 2018 at 15:24):

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

#### Mario Carneiro (May 27 2018 at 15:24):

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

#### Kevin Buzzard (May 27 2018 at 15:24):

but without a doubt it is the prevalent model of mathematics

I don't

#### Kevin Buzzard (May 27 2018 at 15:24):

but some people might

#### Kevin Buzzard (May 27 2018 at 15:24):

and I have them in mind

#### Mario Carneiro (May 27 2018 at 15:25):

or 2^2^2^2^aleph_0 things

#### Mario Carneiro (May 27 2018 at 15:25):

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

#### Kevin Buzzard (May 27 2018 at 15:25):

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 (May 27 2018 at 15:26):

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 (May 27 2018 at 15:26):

because one of these magic meta-theorem things

#### Mario Carneiro (May 27 2018 at 15:26):

yes, it's a pi01 statement so magic happens

#### Mario Carneiro (May 27 2018 at 15:44):

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 (May 27 2018 at 15:47):

Did you look at what I did?

#### Mario Carneiro (May 27 2018 at 15:47):

yes, it was based on your definition

#### Kevin Buzzard (May 27 2018 at 15:47):

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

#### Mario Carneiro (May 27 2018 at 15:48):

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

#### Mario Carneiro (May 27 2018 at 15:49):

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

#### Kevin Buzzard (May 27 2018 at 15:51):

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

#### Kevin Buzzard (May 27 2018 at 15:51):

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

#### Kevin Buzzard (May 27 2018 at 15:52):

no, injective needs checking

#### Kevin Buzzard (May 27 2018 at 15:52):

A presheaf is just a functor

#### Kevin Buzzard (May 27 2018 at 15:52):

It takes an open set to a type

#### Kevin Buzzard (May 27 2018 at 15:52):

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

#### Kevin Buzzard (May 27 2018 at 15:53):

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

#### Kevin Buzzard (May 27 2018 at 15:53):

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

#### Kevin Buzzard (May 27 2018 at 15:54):

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

#### Kevin Buzzard (May 27 2018 at 15:55):

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

#### Kevin Buzzard (May 27 2018 at 15:55):

I'm not bothered either way

#### Mario Carneiro (May 27 2018 at 15:55):

but it is compositional

#### Kevin Buzzard (May 27 2018 at 15:55):

yes but that's an axiom

#### Kevin Buzzard (May 27 2018 at 15:55):

one of the two axioms of functor

#### Mario Carneiro (May 27 2018 at 15:55):

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

gotcha

#### Kevin Buzzard (May 27 2018 at 15:56):

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

#### Mario Carneiro (May 27 2018 at 15:56):

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

right

#### Kevin Buzzard (May 27 2018 at 15:56):

because I can replace F X

#### Kevin Buzzard (May 27 2018 at 15:56):

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

#### Kevin Buzzard (May 27 2018 at 15:57):

X the whole space

#### Kevin Buzzard (May 27 2018 at 15:57):

and then it's still a presheaf

#### Kevin Buzzard (May 27 2018 at 15:57):

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

#### Kevin Buzzard (May 27 2018 at 15:57):

so I broke the sheaf property precisely by breaking injectivity

#### Sean Leather (May 28 2018 at 06:40):

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

Last updated: May 14 2021 at 18:28 UTC