mastodon 4.7.2I’m a mathematician working as a Rust programmer, based in Regensburg, Germany. I enjoy fun and easy math questions, mostly within algebraic geometry. I like constructive mathematics, mainly for aesthetical reasons, and try to think and write constructively when possible.
I’m also interested in literature, history, sociology, economics and philosophy and I enjoy reading books from these fields.
I try to be friendly towards my fellow creatures, which of course has political implications.
Maybe I should be quite happy that I left academia before LLMs were a thing. Now mathematics for me will always be this beautiful creative activity and exchange of ideas over generations and centuries. And in my free time I can still engage with these ideas without any pressure.
If creativity and beauty are taken away from programming, which is now my bread job, it won't effect me emotionally that much because at heart I'm a mathematician.
My motivation to think about math right now is higher than it was at any point of my PhD. It's just so relieving not to feel any pressure.
I was trying to explain to my (non-mathematical) girlfriend why it might be interesting to see what could be proved using constructive logic/why constructive proofs are stronger than classical ones. I came up with an analogy to a court situation where you can't be sentenced even if it can be proved that last night you either commited crime A or crime B but it is not clear which one. You can only be sentenced if there is a proof that you committed crime A or there is a proof that you committed crime B. (Does anyone know if such a scenario ever occurred in reality?)
Anyway, the talk didn't exactly go as I had anticipated, because the law of excluded middle didn't seem intuitive to her at all. »Wait, claiming that everything always has to be either this way or the other, isn't this a very right wing thing to say? It's like saying that there can only be two genders, that doesn't make sense to me at all!« So in the end I was trying to make plausible why some people would be convinced that either there is at least one unicorn or there are no unicorns at all, but I don't think she was convinced.
So I guess I have a constructive girlfriend.
The last couple of days I've been wrapping my head around Gröbner bases over arbitrary (strongly discrete for the constructivists) ground rings and damn, that theory is elegant. Somehow being forced to take care of ideals in the ground ring rather than just zero/non-zero elements forces a more elegant treatment 😅 I'm writing it up in my own words right now…
New goal: Learn elimination theory
I'd like to buy a (gaming) laptop for my girlfriend because her current laptop cannot run the games she likes to play smoothly (mostly Sims 4 and inzoi). I know almost nothing about gaming and/or hardware, so perhaps anyone has recommendations?
@pojntfx@mastodon.social Ping because I feel like you have opinions on hardware for Linux
Question: Constructively, the real line is not covered by (-oo,0] and [0, oo) because for a given real number one can't decide if it's <=0 or >=0. Does the locale of real numbers fix this somehow? Are there two closed sublocales (-oo,0] and [0,oo) whose join is R?
Followup question: Does this allow to define a real function (as a map of locales) which is =0 on (-oo,0] and exp(-1/x) on [0,oo) constructively? (This is the function usually used to prove existence of bump functions https://en.wikipedia.org/wiki/Non-analytic_smooth_function)
Probably not, because I guess everything would descend to the topological space.
A monomial ordering is a total order on ℕ^r making ℕ^r into an ordered monoid, i.e. 0 <= m for all m and m <= m' implies m + n <= m' + n for all m, m', n.
Classically, every monomial ordering is a well-ordering (algebra people like to deduce this from Hilbert's basis theorem).
Is it true constructively that every monomial ordering is well-founded, i.e. allows well-founded induction?
Feel free to boost if you have constructive people in your bubble 😅
I've been typing a lot for the last couple of weeks and my arms are hurting more and more :(
I really wish the Fediverse was more diverse… Do you have any ideas what could be done about this on an individual and on a structural level?
Puzzle: Let A^1 : CAlg(R) -> Set be the forgetful functor from commutative algebras over the real numbers to Set. Show that there is no natural transformation A^1 -> A^1 such that A^1(R) -> A^1(R) is the exponential function. Can you do it without using that A^1 is representable?
Consider the complete lattice of substructures of an algebraic structure, or just submodules of a module, or even just ideals in a commutative ring. Every element of this lattice is a join of »principal« substructures (generated by one element). Is there anything else that is special about the set of principal substructures (or its individual elements) from an order-theoretic point of view?
Can someone explain to me which developments of the recent months justify the MSCI world index being rated 5% higher than at the beginning of the year?
Is there a notion of surjectivity for morphisms of locales (I'm wondering this mostly with algebraic geometry in mind)?