Felix Cherubini, Thierry Coquand, Matthias Hutzler, David Wärn, "Projective Space in Synthetic Algebraic Geometry"
Abstract: Working in an abstract, homotopy type theory based axiomatization of the higher Zariski-topos called synthetic algebraic geometry, we show that the Picard group of projective n-space is the integers, the automorphism group of projective n-space is PGL(n+1) and morphisms between projective standard spaces are given by homogenous polynomials in the usual way.
Matías Menni, "Bi-directional models of `Radically Synthetic' Differential Geometry", Theory and Applications of Categories, Vol. 40, 2024, No. 15, pp 413-429.
Abstract: The radically synthetic foundation for smooth geometry formulated in [Law11] postulates a space T with the property that it has a unique point and, out of the monoid T^T of endomorphisms, it extracts a submonoid R which, in many cases, is the (commutative) multiplication of a rig structure. The rig R is said to be bi-directional if its subobject of invertible elements has two connected components. In this case, R may be equipped with a pre-order compatible with the rig structure. We adjust the construction of `well-adapted' models of Synthetic Differential Geometry in order to build the first pre-cohesive toposes with a bi-directional R. We also show that, in one of these pre-cohesive variants, the pre-order on R, derived radically synthetically from bi-directionality, coincides with that defined in the original model. http://www.tac.mta.ca/tac/volumes/40/15/40-15abs.html
@highergeometer - proving that the automorphism group of projective n-space is PGL(n+1) will sound a bit unimpressive to most algebraic geometers, since it's such a basic fact. I wonder if with almost equal ease the homotopy type theory approach can prove some much more impressive-sounding homotopical generalization of this fact.
@highergeometer wrote: "Yeah, but you have to see the definition of this synthetic projective space as a type to realise it's not immediate. And the automorphism group consists of endomorphisms of the synthetic projective space as a type, not via some explicit construction."
Showing you can still prove things in a formalism that makes them less obvious doesn't count as an advertisement for the formalism to me - it's mostly interesting to people already committed to the formalism. I was hoping that with some tweak one could consider the projective space of a "homotopy vector space", or something like that. (The main kind of "homotopy vector space" I know is a simplicial object in Vect, aka chain complex of vector spaces, but there should be more interesting ones that are spectra. I don't however know if the projective space still makes sense.)
I just had an epiphany. The purpose of an review rebuttal is not to convince the reviewers to change their mind - which is obviously not possible except in vanishingly rare cases - it's to convince the programme committee that the reviewers don't know what they're talking about
@ProfKinyon@julesh "The purpose of an review rebuttal is not to convince the reviewers to change their mind - which is obviously not possible except in vanishingly rare cases - it's to convince the programme committee that the reviewers don't know what they're talking about."
Yes, and this is also the right attitude when arguing with jerks on the internet. You are really talking to the smarter people quietly looking on.
Here's something I just learned: the lucky numbers of Euler.
Euler's "lucky" numbers are positive integers n such that for all integers k with 1 ≤ k < n, the polynomial k² − k + n produces a prime number.
Leonhard Euler published the polynomial k² − k + 41 which produces prime numbers for all integer values of k from 1 to 40.
Only 6 lucky numbers of Euler exist, namely 2, 3, 5, 11, 17 and 41 (sequence A014556 in the OEIS).
The Heegner numbers 7, 11, 19, 43, 67, 163, yield prime generating functions of Euler's form for 2, 3, 5, 11, 17, 41; these latter numbers are called lucky numbers of Euler by F. Le Lionnais.
h/t John Carlos Baez
(@johncarlosbaez) for pointing this out.
The fascinating Heegner numbers [1] are so named for the amateur mathematician who proved Gauss' conjecture that the numbers {-1, -2, -3, -7, -11, -19, -43, -67,-163} are the only values of -d for which imaginary quadratic fields Q[√-d] are uniquely factorable into factors of the form a + b√-d (for a, b ∈ ℤ) (i.e., the field "splits" [2]). Today it is known that there are only nine Heegner numbers: -1, -2, -3, -7, -11, -19, -43, -67, and -163 [3].
Interestingly, the number 163 turns up in all kinds of surprising places, including the irrational constant e^{π√163} ≈ 262537412640768743.99999999999925... (≈ 2.6253741264×10^{17}), which is known as the Ramanujan Constant [4].
which gives primes from 𝑛 = 1 to 𝑛 = 39 is actually related to the fact that 41 × 4 - 1 = 163 is a Heegner number. And this fact has (less impressive) relatives for the smaller Heegner numbers!
As a student, I once walked into a philosophy department's library and found a small gem discussing the origin and naturalness of different Boolean connectives. I remember several options for implication being discussed, a connective we nowadays learn about and whose properties are taken without question.
The paper below on 'why negation' reminds me of that experience some thirty years ago, though as research goes this paper is written with some quantitative arguments instead of only qualitative ones.
I want to read this book: A Darwinian Survival Guide. Sounds like a realistic view of what we need to do now. You can read an interview with one author, the biologist Daniel Brooks. A quote:
...
Daniel Brooks: What can we begin doing now that will increase the chances that those elements of technologically-dependent humanity will survive a general collapse, if that happens as a result of our unwillingness to begin to do anything effective with respect to climate change and human existence?
Peter Watts: So to be clear, you’re not talking about forestalling the collapse —
Daniel Brooks: No.
Peter Watts: — you’re talking about passing through that bottleneck and coming out the other side with some semblance of what we value intact.
Daniel Brooks: Yeah, that’s right. It is conceivable that if all of humanity suddenly decided to change its behavior, right now, we would emerge after 2050 with most everything intact, and we would be “OK.” We don’t think that’s realistic. It is a possibility, but we don’t think that’s a realistic possibility. We think that, in fact, most of humanity is committed to business as usual, and that’s what we’re really talking about: What can we begin doing now to try to shorten the period of time after the collapse, before we “recover”? In other words — and this is in analogy with Asimov’s Foundation trilogy — if we do nothing, there’s going to be a collapse and it’ll take 30,000 years for the galaxy to recover. But if we start doing things now, then it maybe only takes 1,000 years to recover. So using that analogy, what can some human beings start to do now that would shorten the period of time necessary to recover?
@michael_w_busch - does Daniel Brooks suggest setting up small towns without access to surgery? I don't see that. But I want to read his book, to get more detail.
The interview comes to close to discussing these issues:
...
So you live in circumstances where people cannot identify the sociopaths before they’ve taken control. And that’s the subtext in the idea that one of the ways that we should deal with the fact that more than 50 percent of human beings now live in large cities in climate-insecure places, is for those people to redistribute themselves away from climate-insecure areas, into population centers of lower density, and cooperating networks of low-density populations, rather than big, condensed cities.
Peter Watts: Let’s follow this move back to the rural environment a bit, because it’s fundamental. I mean, you brought it up, and it is fundamental to the modular post-apocalyptic society you’re talking about.
Daniel Brooks: Sure. Not post-apocalyptic: post-collapse.
....
But they get distracted, and Watts never gets back to asking what this move to a rural environment would look like.
Despite Wildberger being a bit off the usual conventional paths in mathematics, he's influenced me to the point where every time I write a line of code using an angle I ask myself if I could use an alternative "rational" representation.
@codyroux@BartoszMilewski@dpiponi - if you're trying to declare that some things "exist" and others don't, and you don't want to define what you mean by this term, it's up to smell. Even if you carefully define what it means, in a way that allows you to rigorously prove some things exist and others don't, the definition is likely just a reification of your sense of smell. But that's okay with me as long as you don't think your definition of "exist" is the only acceptable one. I don't think there's any "true" definition of existence of mathematical objects.
(Personally I don't care at all about which mathematical objects "exist": it's a non-issue to me, and an utter waste of time. But I try to remain polite.)
@pozorvlak@BartoszMilewski@dpiponi - that's hilarious! Reminds me of the guy who tried to dial 870247i and got the message "The number you have tried to dial is imaginary. Please rotate by 90 degrees and dial again".
Tolstoy: "Happy families are all alike; every unhappy family is unhappy in its own way."
Mathematics: "Real tori are all alike; every complex torus is complex in its own way."
To be precise, a 'n-dimensional real torus' is a real manifold of the form V/Λ where V is an n-dimensional real vector space and Λ ⊆ V is a lattice of rank n in this vector space. They are all isomorphic.
An 'n-dimensional complex torus' is a complex manifold of the form V/Λ where V is an n-dimensional complex vector space and Λ ⊆ V is a lattice of rank 2n in this vector space. These are not all isomorphic, because there are different ways the lattice can get along with multiplication by i. For example we might have iΛ = Λ or we might not.
And so, it's possible to write a whole book - and indeed a fascinating one - on complex tori. For example a 1-dimensional complex torus is an elliptic curve, and there are whole books just about those.
A while back @pschwahn raised an interesting puzzle here:
You can define a well-behaved cross product of vectors only in 3 and 7 dimensions. The 7d cross product is weird because it's not preserved by all rotations of 7d space. But very smart people have told us there's a way to get the group of 𝟯𝗱 rotations to act on 7d space while preserving the 7d cross product. In fact, you can do it while also getting this group to act 'irreducibly', meaning the only subspaces of 7d space preserved by this action are {0} and the whole space!
The puzzle is: 𝗰𝗮𝗻 𝘆𝗼𝘂 𝘄𝗿𝗶𝘁𝗲 𝗱𝗼𝘄𝗻 𝘁𝗵𝗲 𝗳𝗼𝗿𝗺𝘂𝗹𝗮𝘀 𝗳𝗼𝗿 𝗵𝗼𝘄 𝘁𝗵𝗶𝘀 𝘄𝗼𝗿𝗸𝘀?
I got stuck on this so I asked some of my friends, and now Layra Idarani has outlined a nice way to do it:
Interestingly he doesn't actually give the formulas; he just tells you how to get them. So I will need to do some work to check his answer! If you want to help out, that would be great.
Layra said "The devil of the details is in the eating". I thought the proof was in the pudding. Now I'm hungry for devil's food cake.
@Dyoung@pschwahn - it's there: it's the group of rotations that rotates x, y, and z in the usual way. To understand this you need to start further back, e.g. with my failed attempt
I laid out the strategy nicely but failed to guess a good choice of 7 cubic polynomials - I called them 𝑒₁,...𝑒₇ . They lacked the properties I wanted to check, but worse they weren't even orthonormal. Layra's polynomials P, Q, R, S, T, U, V have all the right properties - or so he claims.
By the way, it's super-easy to construct the 7d cross product on the imaginary octonions: just define
𝑎 × 𝑏 = (𝑎𝑏−𝑏𝑎)/2
All the work here is constructing an SO(3) group that acts irreducibly on the imaginary octonions while preserving this cross product!