Stream: new members

Topic: is_function

Julian Berman (Oct 14 2020 at 14:32):

Does the simple definition of a function live somewhere I'm not finding and/or is there a tactic I should be using? I found congr_arg at least in the definition of function.injective

lemma is_function {α β : Type} {a a' : α} (f: α → β) : f a ≠ f a' → a ≠ a' := begin
contrapose,
push_neg,
exact congr_arg f,
end


Patrick Massot (Oct 14 2020 at 14:36):

Don't tell the other mathematicians I told you that, but you don't need all those double negation here. The proof term is λ h h', h (congr_arg f h')

Julian Berman (Oct 14 2020 at 14:38):

Secret is safe with me.

Thanks :)

Yury G. Kudryashov (Oct 14 2020 at 14:47):

mt (congr_arg f) works too

Julian Berman (Oct 14 2020 at 15:01):

Ah that's nice too thanks!

Adam Topaz (Oct 14 2020 at 15:04):

If you look at the definition of mt, I think you'll see that these are really the same solution ;)

Julian Berman (Oct 14 2020 at 15:05):

Yeah true though if we consider whether Lean has a notion of proofs from The Book the ones in it have to be the non-fully-unwound ones right :D?

Adam Topaz (Oct 14 2020 at 15:07):

I'm not sure what you mean...

Adam Topaz (Oct 14 2020 at 15:07):

What's "The Book"?

Julian Berman (Oct 14 2020 at 15:08):

ha sorry, it's an Erdos thing

Julian Berman (Oct 14 2020 at 15:08):

https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

Oh "THE Book"!

Adam Topaz (Oct 14 2020 at 15:10):

I prescribe to the idea (I think of Kronecker?) that God created $\mathbf{N}$ and everything else is from us mere mortals.

Heather Macbeth (Oct 14 2020 at 16:43):

Really? I believe in $\mathbb{P}^n$.

Adam Topaz (Oct 14 2020 at 16:43):

$\mathbb{P}^n_{\mathbf{F}_1}$?

Heather Macbeth (Oct 14 2020 at 16:44):

Well, the others, but maybe not that one :)

Kevin Buzzard (Oct 14 2020 at 17:17):

A disdainful Faltings introduced Soul\'e at a talk at Max Planck about $\mathbb{F}_1$, and at the end of it Faltings suggested that the next time he came back he could talk about $\mathbb{F}_2$

Julian Berman (Oct 14 2020 at 21:06):

Can someone explain the joke to us mere mortals or does that ruin it -- what's F_1​, the nonexistent field-with-one-element? And P^n? n-tuples of N - {0}?

Adam Topaz (Oct 14 2020 at 21:15):

$\mathbf{F}_1$ is the field with one element. There is no field with one element. Rather it's a collection of ideas based on observations that there is some consistent behavior for objects over $\mathbf{F}_q$ as $q$ tends to $1$.

Kenny Lau (Oct 14 2020 at 21:17):

https://en.wikipedia.org/wiki/Field_with_one_element
According to the analogy, the projective n-space over the field with 1 element is the set with n elements

Kenny Lau (Oct 14 2020 at 21:17):

P^n is the projective n-space

Julian Berman (Oct 14 2020 at 21:19):

That is an impressively long page. OK I am probably starting to understand the literal possibility of giving a talk on it

Adam Topaz (Oct 14 2020 at 21:26):

The example of projective spaces is nice, because for a finite field $\mathbf{F}_q$ you have
$\# \mathbb{P}^{n-1}(\mathbf{F}_q) = \# \left( (\mathbf{F}_q^n - \{0\}) / \mathbf{F}_q^\times \right) = (q^n-1)/(q-1)$
and on the other hand you can write $\mathbb{P}^{n-1}$ as a disjoint union
$\mathbb{P}^{n-1} = \mathbb{A}^{n-1} \sqcup \mathbb{A}^{n-2} \sqcup \cdots \sqcup \mathbb{A}^{0}$
while $\#\mathbb{A}^k(\mathbf{F}_q) = q^k$.
So the fact that these agree give the formula
$\frac{q^n-1}{q-1} = q^{n-1} + q^{n-2} + \cdots + 1.$

Adam Topaz (Oct 14 2020 at 21:26):

And in the limit where $q \to 1$ you get $n$.

Adam Topaz (Oct 14 2020 at 21:30):

There have been various proposals over the years for "geometry over $\mathbf{F}_1$", one by Soul\'e that Kevin mentioned above.

Last updated: May 11 2021 at 23:11 UTC