May 30, 2020
Online Magnitude Talk by Mark Meckes
Posted by Simon Willerton
For any magnitude fans out there, Mark Meckes is giving a Zoom talk at the Online Asymptotic Geometric Analysis Seminar next Saturday, June 6, 11:30AM (New York time) 4:30PM (Sheffield time).
- Magnitude and intrinsic volumes of convex bodies.
Abstract: Magnitude is an isometric invariant of metric spaces with origins in category theory. Although it is very difficult to exactly compute the magnitude of interesting subsets of Euclidean space, it can be shown that magnitude, or more precisely its behavior with respect to scaling, recovers many classical geometric invariants, such as volume, surface area, and Minkowski dimension. I will survey what is known about this, including results of Barcelo-Carbery, Gimperlein-Goffeng, Leinster, Willerton, and myself, and sketch the proof of an upper bound for the magnitude of a convex body in Euclidean space in terms of intrinsic volumes.
May 16, 2020
The Brauer 3-Group
Posted by John Baez
For reasons ultimately connected to physics I’ve been spending time learning about the Brauer 3-group. For any commutative ring there is a bicategory with
- algebras over as objects,
- bimodules as morphisms,
- bimodule homomorphisms as 2-morphisms.
This is a monoidal bicategory, since we can take the tensor product of algebras, and everything else gets along nicely with that.
Given any monoidal bicategory we can take its core: that is, the sub-monoidal bicategory where we only keep invertible objects (invertible up to equivalence), invertible morphisms (invertible up to 2-isomorphism), and invertible 2-morphisms. The core is a monoidal bicategory where everything is invertible in a suitably weakened sense so it’s called a 3-group.
I’ll call the particular 3-group we get from a commutative ring its Brauer 3-group, and I’ll denote it as . It’s discussed on the Lab: there it’s called the Picard 3-group of but denoted as .
Like any 3-group, we can think of as a homotopy type with 3 nontrivial homotopy groups, and . These groups are wonderful things in themselves:
is the Brauer group of .
is the Picard group of .
is the group of units of .
But in general, a homotopy type contains more information than its homotopy groups. So on MathOverflow I asked if anyone knew the Postnikov invariants of the Brauer 3-group — the extra glue that binds the homotopy groups together. In theory these could give extra information about our commutative ring .
But Jacob Lurie said the Postnikov invariants are trivial in this case.
May 10, 2020
In Further Praise of Dependent Types
Posted by David Corfield
After an exciting foray into the rarefied atmosphere of current geometry, I want to return to something more prosaic – dependent types – the topic treated in Chapter 2 of my book. We have already had a paean on this subject a few years ago in Mike’s post – In Praise of Dependent Types, hence the title of this one.
I’ve just watched Kevin Buzzard’s talk – Is HoTT the way to do mathematics?. Kevin is a number theorist at Imperial College London who’s looking to train his undergraduates to produce computer-checked proofs of mainstream theory (e.g., theorems in algebraic geometry concerning rings and schemes) in the Lean theorem-prover.
Why Lean? Well, at (12:14) in the talk Kevin claims of mathematicians that
They use dependent types, even though they don’t know they are using dependent types.
Let’s hope they receive this news with the delight of Molière’s Mr. Jourdain:
« Par ma foi ! il y a plus de quarante ans que je dis de la prose sans que j’en susse rien, et je vous suis le plus obligé du monde de m’avoir appris cela. »
“My faith! For more than forty years I have been speaking prose while knowing nothing of it, and I am the most obliged person in the world to you for telling me so.”