# Zulip Chat Archive

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

#### Julian Berman (Oct 14 2020 at 14:39):

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

#### Adam Topaz (Oct 14 2020 at 15:08):

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