Guest post by Bruce Bartlett
On Monday, David Corfield and Kobi Kremnitzer gave philosophy talks in a snazzy new building at Oxford:
Kobi Kremnitzer, What is geometry?, 2-4pm.
David Corfield, What might philosophy make of homotopy t...
Guest post by Bruce Bartlett
On Monday, David Corfield and Kobi Kremnitzer gave philosophy talks in a snazzy new building at Oxford:
Kobi Kremnitzer, What is geometry?, 2-4pm.
David Corfield, What might philosophy make of homotopy type theory?, 4.30-6.30pm.
The talks shared homotopy type theory as a common theme. The name “Per Martin-L?f” was mentioned a lot, which was good for me since I had always thought Martin and L?f were two separate people:
Notes are available above, but I will try to give some brief impressions.
Kobi Kremnitzer, What is geometry?
1. Introduction
He started by answering the question “Why am I giving this talk?”, and explained that he followed the pragmatic approach to philosophy of mathematics. I think then he said his approach was somehow similar to that of Wittgenstein and Carnap (but he could have been saying the exact opposite :-)), and that for him, there is no Metaphysics in the joint carving. I’m afraid this totally went over my head, but I did imagine some Oxford dons pleasantly carving a roast chicken, which started to make me hungry!
He stressed that for him mathematics is not in the business of theorem proving only, but mathematicians create new systems, new languages, and that in the correct language a problem becomes trivial… the approach of Grothendieck.
2. Categorical language
Since it was a philosophy talk, he motivated categories by starting with Kripke semantics, going via posets, and then he went from posets to categories by literally “raising the bar”!
3. Crashcourse in algebraic geometry
Algebraic geometry is the study of solutions to polynomial equations, like a parabola:
X={y−x 2=0}.
I haven’t specified what “y” and “x” actually are, and that’s the point. We can interpret them in any ring. Hence the Grothendieck view is to think of an affine variety X defined by a bunch of polynomial equations f 1,…,f n as being a presheaf on the category of rings,
X:Rings op→Set,
defined by
X(R)={(a 1,…,a n)∈R n:f i(a 1,…,a n)=0foralli∈I}.
This leads us to define the category of algebraic spaces as being nothing but the category of presheaves on Ring.
This category of algebraic spaces has lots of nice properties. Inside it live subcategories of objects having nice properties, such as schemes and sheaves. But Kobi stressed that it is very handy to understand them as living in this general universe of algebraic spaces.
3. What is algebra?
There was a crucial idea lurking above - that a ring is a gismo R which allows you to take any polynomial f∈ℤ[x 1,…,x n] and evaluate it on elements of R.
So - to go from algebraic to differential geometry, we could replace the concept of a “ring” with the concept of a “C ∞-ring” — this is a gismo R which allows you to take any smooth function f∈C ∞(ℝ n,ℝ) and evaluate it on elements of R!
For instance, the space of smooth functions on a manifold is a C ∞-ring… but so is ℂ[ϵ]/ϵ 2 ! So by this slight change of view, we have accomplished Leibniz’s dream - calculus and infinitesimals in the same universe.
4. Final comments
He spoke a bit about: derived geometry, set-theoretic foundations, noncommutative geometry, synthetic differential geometry, elementary theory of the category of sets - have a look at the last few pages of his notes.
He stressed that ordinary set-theoretic foundations pulverizes spaces into “atomic dust” where the elements have no “cohesion” with each other… we have to put this back in by hand using topology. As a foundation, homotopy type theory will have this cohesiveness natively built in, and that is attractive to a geometer.
David Corfield, What might philosophy make of homotopy type theory?
Da
