is_function

Stream: new members

[Julian Berman]

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]

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]

Secret is safe with me.

[Julian Berman]

Thanks :)

[Yury G. Kudryashov]

mt (congr_arg f) works too

[Julian Berman]

Ah that's nice too thanks!

[Adam Topaz]

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

[Julian Berman]

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]

I'm not sure what you mean...

[Adam Topaz]

What's "The Book"?

[Julian Berman]

ha sorry, it's an Erdos thing

[Julian Berman]

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

[Adam Topaz]

Oh "THE Book"!

[Adam Topaz]

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

[Heather Macbeth]

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

[Adam Topaz]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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]

$\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]

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]

P^n is the projective n-space

[Julian Berman]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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