Zulip Chat Archive

Stream: new members

Topic: is_function


view this post on Zulip 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

view this post on Zulip 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')

view this post on Zulip Julian Berman (Oct 14 2020 at 14:38):

Secret is safe with me.

view this post on Zulip Julian Berman (Oct 14 2020 at 14:39):

Thanks :)

view this post on Zulip Yury G. Kudryashov (Oct 14 2020 at 14:47):

mt (congr_arg f) works too

view this post on Zulip Julian Berman (Oct 14 2020 at 15:01):

Ah that's nice too thanks!

view this post on Zulip 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 ;)

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Oct 14 2020 at 15:07):

I'm not sure what you mean...

view this post on Zulip Adam Topaz (Oct 14 2020 at 15:07):

What's "The Book"?

view this post on Zulip Julian Berman (Oct 14 2020 at 15:08):

ha sorry, it's an Erdos thing

view this post on Zulip Julian Berman (Oct 14 2020 at 15:08):

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

view this post on Zulip Adam Topaz (Oct 14 2020 at 15:08):

Oh "THE Book"!

view this post on Zulip Adam Topaz (Oct 14 2020 at 15:10):

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

view this post on Zulip Heather Macbeth (Oct 14 2020 at 16:43):

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

view this post on Zulip Adam Topaz (Oct 14 2020 at 16:43):

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

view this post on Zulip Heather Macbeth (Oct 14 2020 at 16:44):

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

view this post on Zulip Kevin Buzzard (Oct 14 2020 at 17:17):

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

view this post on Zulip 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}?

view this post on Zulip Adam Topaz (Oct 14 2020 at 21:15):

F1\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 Fq\mathbf{F}_q as qq tends to 11.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 14 2020 at 21:17):

P^n is the projective n-space

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 14 2020 at 21:26):

The example of projective spaces is nice, because for a finite field Fq\mathbf{F}_q you have
#Pn1(Fq)=#((Fqn{0})/Fq×)=(qn1)/(q1) \# \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 Pn1\mathbb{P}^{n-1} as a disjoint union
Pn1=An1An2A0 \mathbb{P}^{n-1} = \mathbb{A}^{n-1} \sqcup \mathbb{A}^{n-2} \sqcup \cdots \sqcup \mathbb{A}^{0}
while #Ak(Fq)=qk\#\mathbb{A}^k(\mathbf{F}_q) = q^k.
So the fact that these agree give the formula
qn1q1=qn1+qn2++1. \frac{q^n-1}{q-1} = q^{n-1} + q^{n-2} + \cdots + 1.

view this post on Zulip Adam Topaz (Oct 14 2020 at 21:26):

And in the limit where q1q \to 1 you get nn.

view this post on Zulip Adam Topaz (Oct 14 2020 at 21:30):

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


Last updated: May 11 2021 at 23:11 UTC