let in structure

Stream: general

[Kevin Buzzard]

structure foo :=
let bar := ℕ in
(3 : bar)

[Kevin Buzzard]

doesn't work

[Kevin Buzzard]

moans about the let

[Kevin Buzzard]

Am I doomed to write power_bounded_elements R throughout this entire definition?

[Johan Commelin]

well, we can make some notation for it, right?

[Johan Commelin]

Isn't double-superscript-circ common for this?

[Kevin Buzzard]

aah here notation will solve my problem

[Kevin Buzzard]

wait

[Kevin Buzzard]

oh I have to leave the stupid gap

[Kevin Buzzard]

$R\ {}^\circ$

[Kevin Buzzard]

need the gap because of some fussy tokenizer

[Johan Commelin]

It feels a bit like we are back to the typography of SGA etc, doesn't it?

[Andrew Ashworth]

def bar : Type := ℕ

structure foo :=
(x : bar)

I am unsure how to choose between notation and defs when you don't need infix/postfix parsing

[Simon Hudon]

I assume you're making it into a postfix operator. Why not make the whole thing (R∘) a notation?

[Johan Commelin]

You mean including the R?

[Simon Hudon]

Exactly

[Johan Commelin]

But that's variable

[Kevin Buzzard]

notation : R `ᵒ` := power_bounded_subring R

[Kevin Buzzard]

How does notation work? I never know. I need some notation notes

[Simon Hudon]

If you declare it with variable, and make your notation local, that should be ok

[Kevin Buzzard]

I know I can search through TPIL

[Johan Commelin]

Yay for Zulip's parsing of "`".

[Simon Hudon]

Use more ticks until it works

[Kevin Buzzard]

right

[Kevin Buzzard]

I use two outer ticks

[Johan Commelin]

@Simon Hudon Aah, it's not variable like that. It is really variable in the notation.

[Johan Commelin]

Like x and y in x + y.

[Kevin Buzzard]

I can't get the notation to work though

[Simon Hudon]

I must have misunderstood. I thought you wanted a local shorthand for the current file.

[Johan Commelin]

Hmm, but now you didn't leave a gap in the ticks.

[Johan Commelin]

I think it wants spaces around the \circ

[Simon Hudon]

Otherwise, you can use postfix `ᵒ` := power_bounded_subring

[Kevin Buzzard]

oh that looks like a nicer way to do it

[Kevin Buzzard]

it wants a number

[Kevin Buzzard]

postfix `ᵒ` : 37 := power_bounded_subring

[Kevin Buzzard]

that should do it

[Kevin Buzzard]

I must say, operator precedence is something else I am not sure I have a good feeling about

[Kevin Buzzard]

I guess I want this one to be very sticky

[Kevin Buzzard]

so should it be like 6 or 999999?

[Simon Hudon]

To be fair, I'm not fond of putting precedence on a linear scale. I feel like specifying a partial order would be easier

[Kevin Buzzard]

OK how about this:

[Kevin Buzzard]

structure perfectoid_ring (R : Type) (p : ℕ) [is_prime p] extends Tate_ring R :=
(is_complete : complete R)
(is_uniform  : uniform R)
(ramified    : ∃ ω : R ᵒ,
                 (is_pseudo_uniformizer ω) ∧ (ω ^ p ∣ p))
 (Frob       : ∀ a : R ᵒ,
                 ∃ b c : R ᵒ, a = b ^ p + p * c)

[Simon Hudon]

Think about the operators that are likely to appear in the same formula (including =) and what should take precedence

[Kevin Buzzard]

I want the circ to take precedence in the sense that I want R circ being evaluated ASAP

[Kevin Buzzard]

i.e. A x B o is definitely A x (B o)

[Simon Hudon]

precedence and evaluation order are not the same

[Kevin Buzzard]

@Johan Commelin I reckon that looks fairly readable

[Kevin Buzzard]

Simon I don't know anything about this stuff

[Johan Commelin]

Yes, this looks very good. I hope you can maintain this throughout the top-down approach.

[Kevin Buzzard]

and I know I can learn it but I'm not that interested in it

[Simon Hudon]

I'll leave you guys to it

[Kevin Buzzard]

do you have a good suggestion for a number?

[Kevin Buzzard]

or else I'll leave it as 37 :-/

[Mario Carneiro]

same as unary minus?

[Mario Carneiro]

which is 65

[Simon Hudon]

That looks like asking for trouble. Go one over or one below

[Johan Commelin]

Is there anything below 50 at the moment?

[Mario Carneiro]

tons

[Mario Carneiro]

propositional stuff mostly

[Mario Carneiro]

50 is =, so that's about as low as you get for atomic propositions

[Kevin Buzzard]

ha ha (-Ro) -- is that what you're worried about Simon?

[Mario Carneiro]

but types go lower than that

[Kevin Buzzard]

can that sort of thing be an issue?

[Mario Carneiro]

equal isn't really a problem

[Mario Carneiro]

in fact it's important for having things be at the same level, like a + b - c

[Mario Carneiro]

which is left associated regardless of whether + or - comes first

[Johan Commelin]

@Kevin Buzzard If you want to squeeze out a little bit more readability, then maybe Frob should be phrased as a statement modulo p.

[Mario Carneiro]

there aren't many postfix operators in standard lean; there is ⁻¹ which has a crazy high precedence max+10

[Simon Hudon]

@Kevin Buzzard I'm not sure what Lean does in that kind of situation and I can't think of reasons why either of (-R)o or -(Ro) would be always the best default

[Kevin Buzzard]

I wasn't sure how to do quotient rings in Lean

[Johan Commelin]

But I guess, you rather prefer avoiding quotients.

[Kevin Buzzard]

actually I recently learnt how to use quotient types

[Kevin Buzzard]

I was forced to

[Mario Carneiro]

All notations come with a binding power, whichever is higher wins

[Kevin Buzzard]

I needed direct limits and Kenny's work is still not in mathlib

[Mario Carneiro]

that includes mixing pre/postfix

[Johan Commelin]

@Simon Hudon In both cases the unary minus doens't make much sense. (At least not in contemporary maths. Maybe someone wants to overload it, but that thought gives me shudders...)

[Johan Commelin]

So I guess in practice there won't be a problem.

[Mario Carneiro]

Since R o here is a type it really doesn't matter as long as it's higher than 50 or so

[Johan Commelin]

@Kevin Buzzard I told you before that 57 is a better default value than 37! Grothendieck was careful when choosing his prime!

[Mario Carneiro]

lol it would be funny if all the notation precedences were primes just because

[Johan Commelin]

Ooh, now I have a crazy question. What is the type of 65 in the notation for unary minus? Does it even have a type?

[Mario Carneiro]

It was once num, which was for a long time the only use of num. Now it's nat

[Kevin Buzzard]

instance p : nat

[Kevin Buzzard]

Does this lead me into trouble?

[Kevin Buzzard]

I am sick of this p

[Kevin Buzzard]

I want access to it at all times and yet I never want to carry it around

[Kevin Buzzard]

It's a global variable

[Mario Carneiro]

see e.g. std.prec.max

[Mario Carneiro]

In actual notation commands though the number is not an expression of type nat, it's a literal number string

[Mario Carneiro]

although you can use max and other things in that spot too

[Kevin Buzzard]

wait

[Kevin Buzzard]

I have to make nat a class

[Kevin Buzzard]

oh jeez where's that bit in the manual

[Kevin Buzzard]

now I finally want to do it

[Johan Commelin]

Do you mean like attribute [class] nat?

[Mario Carneiro]

don't make nat a class

[Mario Carneiro]

make Prime a class

[Johan Commelin]

@Kevin Buzzard Can't you have

variables (p : nat) (hp : prime p)
include p hp

[Johan Commelin]

Does that make p and hp available everywhere you want them?

[Kevin Buzzard]

I'm using type class inference to carry around primality of p

[Mario Carneiro]

import data.nat.prime algebra.group_power

class Prime :=
(p : ℕ) (pp : nat.prime p)
open Prime

section
variable [Prime]

example (R) [ring R] (x : R) : x ^ 2 = x ^ p := sorry

end

[Kevin Buzzard]

I thought Prime was supposed to be the subtype

[Mario Carneiro]

it is

[Kevin Buzzard]

I suppose

[Kevin Buzzard]

this way you get to change the name from val to p

[Mario Carneiro]

Actually I said "bundled structure", so this is in some sense more faithful to the convention

[Kevin Buzzard]

Is this sort of stuff mathlib-acceptable?

[Mario Carneiro]

only if you use it a lot

[Mario Carneiro]

I would prefer that you postprocess all your final theorems or whatever to make the prime explicit, but you can do this within the development if it helps

[Andrew Ashworth]

is p actually default nat in that code snippet?

[Mario Carneiro]

it's like default nat but not the same value

[Mario Carneiro]

This is one of the important aspects of creating a new class - you get to create your own typeclass graph

[Mario Carneiro]

in this case, since there are no instances of Prime, it will only ever pick up [Prime] in the context

[Mario Carneiro]

maybe fixed_prime is a better name for this typeclass

[Andrew Ashworth]

at first glance, this seems kinda hackish to me, but I need to think about it some

[Kevin Buzzard]

It very much conveys what's going on

[Andrew Ashworth]

the whole variable [Prime] has me for a loop

[Kevin Buzzard]

I won't be using it a lot for the definition of perfectoid spaces

[Johan Commelin]

Same here. I still don't get how Lean figures out what p means in the line
example (R) [ring R] (x : R) : x ^ 2 = x ^ p := sorry

[Kevin Buzzard]

it's just you'll use it all the time the moment you start proving theorems about them

[Mario Carneiro]

Since Prime was opened, that's Prime.p

[Johan Commelin]

Aah, cool!

[Mario Carneiro]

which has an implicit typeclass argument [Prime], which is discovered in the context

[Johan Commelin]

So then once we start doing etale cohomology we want another class fixed_coprime_prime, and constructor ℓ

[Johan Commelin]

And a proof that it is not p

[Mario Carneiro]

class fixed_prime :=
(p : ℕ)
(pp : nat.prime p)
open fixed_prime

class fixed_coprime [fixed_prime] :=
(q : ℕ)
(co : nat.coprime p q)

[Johan Commelin]

Mario, I really like this! I hope that it is not to hackish for Lean. This reflects how p is used in a lot of number theory/alg.geom. You just fix p at the beginning of your paper, and it doesn't change for 50 pages.

[Johan Commelin]

Yes, but the ℓ has to be prime as well. As in "ℓ-adic cohomology" etc...

[Mario Carneiro]

I haven't attempted to use this technique before. I'd be interested to see how it goes

[Andrew Ashworth]

it feels like an end run around parameter

[Mario Carneiro]

you get the idea

[Johan Commelin]

Sure.

[Johan Commelin]

I will try to use it in the stuff on p-adic valuations.

[Mario Carneiro]

Note that actually applying this for real primes, like if you want 57-adic cohomology, is a bit of a pain

[Johan Commelin]

Hmm, I see.

[Mario Carneiro]

well, maybe not so bad, you can use local instances or haveI to introduce a fixed_prime without doing so globally

[Johan Commelin]

That's a bit of a problem, I guess. For example squares in Q_2 behave different from squares in Q_p for p ≠ 2.

[Mario Carneiro]

I mean, worst case scenario is you have to write @thm whenever you want to apply the theorem in a non p case

[Johan Commelin]

Yes, I see. That makes sense.

[Mario Carneiro]

also you can prove things with the assumption p = 2

[Johan Commelin]

Right.

[Johan Commelin]

Actually the @ notation reflects exactly how most mathematicians feel about working with one concrete prime. (Of course not the symbol "@", but the fact that all of a sudden you want to be specific about p.)

[Johan Commelin]

You only do this in 1% of the time. And it always feels a bit disorienting.

[Mario Carneiro]

whence the 57 thing

[Johan Commelin]

I really think that we have theorems about Q_p, Q_ℓ and Q_2, and that is about it (-;

[Mario Carneiro]

one other messy thing is if you want to use l as your p

[Johan Commelin]

So, have to unpack stuff with @ is expected behaviour.

[Johan Commelin]

Aah, yes, that might get messy...

[Johan Commelin]

Also, there is a very delicate theory about what happens when ℓ = p...

[Johan Commelin]

Headache ensues

[Johan Commelin]

(Note: this is not relevant for defining perfectoid spaces. But it will definitely pop up later.)

[Mario Carneiro]

Long story short, this technique is useful for fixing a value for a long time, with the downside being it makes unfixing it hard

[Mario Carneiro]

parameters are easier to unfix, but then they stay unfixed

[Johan Commelin]

Ok, so maybe we should do the same thing as with multiplicative groups and additive groups. And just develop the theory both for p and for ℓ...

[Mario Carneiro]

That's not unreasonable; the theorems are defeq so you just have to state them

[Johan Commelin]

Hmm, but sometimes you also want to compare what happens at ℓ_1 and ℓ_2... and both are different from p.

[Mario Carneiro]

maybe ℓ shouldn't be as fixed as p

[Johan Commelin]

Or statements like \forall ℓ : (ℓ ≠ p) blabla.

[Andrew Ashworth]

an argument for using a parameter might be that when you use haveI and friends, you don't get to benefit from type class caching... although I am unsure how much time Lean spends searching the type class graph - it's not something I have a good feel for

[Mario Carneiro]

in practice I've never seen an appreciable difference from using haveI

[Johan Commelin]

Ok, maybe ℓ should indeed have less fixiness than p.

[Andrew Ashworth]

I think it might be a bigger deal for people working in interactive tactic mode... who have very large proofs / definitions

[Andrew Ashworth]

again, it ::sounds:: scary to me, also because I don't mind at all being explicit, but that may be because I don't have enough Lean experience

[Andrew Ashworth]

would it affect memoization? suppose you had

def myDef :=
begin
  expensive_tac1,  -- uses typeclass inference somewhere
  expensive_tac2  -- does this mean we can't memoize the results of expensive_tac1 if we disable type class cache?
end