Oops, that's an interesting counterexample but I wrote the statement wrong, sorry — what I want is f and ℐ such that ℐ is radical, f pointwise belongs to ℐ, and there does not exist a constant c ∈ ℤ such that c⋅f ∈ ℐ. Otherwise f = 2 and ℐ = ⟨X(X+1)⟩ already works.
Yes, I know about the Nullstellensatz, but I haven't been able to apply it. Neither do I have a counterexample in ℤ where f belongs to ℐ pointwise but is not actually in ℐ and ℐ is radical, but I haven't seriously searched yet.
I can prove that (for ℤ) if ℐ is principal and f pointwise belongs to ℐ then in fact f belongs to ℐ. I'm ashamed to admit that for a long time I believed this to be true for all ℐ, until a colleague made ChatGPT find a stupid counterexample: XY pointwise belongs to ⟨X², Y²⟩.
Thanks. Specifically, I would like to know whether we can algorithmically decide, given f, g₀, …, gₙ₋₁ ∈ ℤ[X₀, …, Xₖ₋₁], whether f “pointwise”/whatever belongs to ⟨g₀, …, gₙ₋₁⟩. But more generally I'm interested in any characterizations of when this happens, maybe with some assumptions on the ideal.
For example, if R is a field then the statement that f locally belongs to I just means that f vanishes on the affine variety defined by I. The case I am interested in is R = ℤ.
Let R be a commutative ring. Say that a multivariate polynomial f ∈ R[X₀, …, Xₖ₋₁] locally belongs to an ideal I of R[X₀, …, Xₖ₋₁] when for every point x ∈ Rᵏ the value f(x) belongs to the ideal {g(x), g ∈ I} of R. Does this already have a name and what can be said about it?
I asked a question on MathOverflow.
mathoverflow.net/q/508812/1946 #MathOverflow
There's the MetaRocq project to write a verified version of it (in Rocq itself), but it still doesn't have a proof for termination, because that's precisely the part where Rocq does shady things whose consistency and semantics are unclear, and unsurprisingly three of Claude's bugs are there.
It's OCaml code, not formally verified, “validated” by the traditional method of code review :)
There's a list of them here, I haven't looked at them myself: tristan.st/blog/in_sear...
Oh my god, LLMs are autonomously finding inconsistencies in Rocq…
rocq-prover.zulipchat.com#narrow/chann...
Humour très, très niche 🙂
Je crois bien que c'est correct. Remplace "need" par "may" ou "must" et ça te surprendra sans doute moins.
(To be extra clear, I also think that even if one doesn't consider HoTT suitable as a foundation, it remains a mathematically interesting and technically useful object worth studying.)
in HoTT, I'm definitely thinking about something being “true”, but I don't really want that something to be a very complicated statement about simplicial sets or some variety of cubical sets—so what is it? This is why HoTT has made me feel philosophical discomfort that anti-classical math hasn't.
If I want to translate it to set-level foundations, I have half a dozen models available, but unlike the beginning of the subject, when Voevodsky's simplicial set model was considered canonical, I feel that in the present state of research none of them stands out as such. So when I prove a theorem …
There are even things which I now tend to think about in HoTT because I find it more intuitive. Yet if I try to make more precise what I really have in mind, I'm kind of stuck (and to be clear, this is not in favor of univalent foundations!).
Still, I think the ontology of Russian constructivism is clear: if I want to translate a theorem to ZFC, I just interpret it in the effective topos.
But what is the ontology of HoTT? I am perfectly able to work in HoTT, by appealing (when needed) to pre-mathematical intuitions about spaces.
However you do totally have a point about constructive math — for this comparison I would mainly count anti-classical schools, e.g., Russian constructivism. Not sure why I didn't think of this, silly me (I edited).
I mean, if I prove some theorem in PM and you're working in ZFC, it's pretty straightforward for you to translate it to your setting. The two foundations have a least upper bound of sorts. PM and other set-level type theories don't force a “types-as-sets” ontology but they're compatible with it.
Why philosophers of mathematics should care about univalent foundations (homotopy type theory):
mathstodon.xyz/@jeanas/1161...
(@joeldavidhamkins.bsky.social)
… primitive element which is a linear (not just algebraic) combination of the roots, and moreover "most" linear combinations are primitive elements, so you search it under this form? But it's elegant and a bit magical that you manage to do this computation without the algebraic closure.
I think I'm starting to understand this better, though I'll need a little more time to digest it. As I understand it, your idea is that by the strengthening of the primitive element theorem that the standard proof shows, the subfield of the algebraic closure generated by the roots will have a …
Wait, you meant to use an explicit description of the conjugates of y in a rupture field k[y]/⟨P⟩? What is this description?
Sorry, I didn't get the very last part, what is the linear algebra you do?
To be sure I understand, the reason for the “Zariski-closed” bit is that g is not separable iff the resultant of g and g' vanishes?
Oh yes, I'm interested.
Thank you! At least the beginning was very helpful (and even without details it's helpful to know when a problem is hard, which is what the books always neglect to tell you…). I couldn't much follow the rest, you lost me at “infinitesimals” 😅
