mathlib

mathlib copied to clipboard

I don't have any specific application in mind, and just wanted to test how hard it is to connect the two.

For a general submonoid, adjoining the inverses of elements in a subset whose saturation equals that submonoid should yield localization at the submonoid. However we don't yet have the API to adjoin possibly infinitely many roots at once.

---

Hmm I got a strange deterministic timeout in field_theory/is_alg_closed/basic (which I didn't modify) at

structure subfield_with_hom :=
(carrier : subalgebra K L)
(emb : carrier →ₐ[K] M)

~~I can't reproduce the timeout locally.~~ (Edit: now I can.) This happened after I added the subsingleton instance for alg_homs from a localization to any algebra; this definition mentions an alg_hom but the whole file doesn't mention any localization or subsingleton...

hmm, I'm really not sure what's going on here. I don't know why structures automatically look for subsingleton instances, but from what I can see it's just slow because it keeps digging into that instance and trying to make the instances (which are quite hard... has to find rings, fields, carriers, is_localization...) and so it just takes a while. I feel like it's worth posting on Zulip to see if it's a known problem or not, though.

Thanks for the reviews! I'll get back to this PR in 1-2 days. Feel free to commit directly in the meantime.

Thanks for the reviews! I'll get back to this PR in 1-2 days. Feel free to commit directly in the meantime.

@alreadydone I've added awaiting author and removed awaiting review, since you said you will be back on this in a few days. When you feel it's ready don't hesitate to put the label back.

@riccardobrasca Thanks for that :) I was distracted and will need a few more days before I get back to this.

I'm finally back working on this PR; sorry for the long delay! In addition to the request to add ideal.quotient.alg_hom_ext, I also plan to prove localization.away is finitely presented (algebra.finite_presentation), and for that I need to show adjoin_root is finitely presented over the base ring. I wonder if @erdOne will need them and/or already have these somewhere.

@nick-kuhn said to me last month that he is working on showing localization.away is finitely presented. I'm not sure about his progress.

If I remember correctly, I do have a proof that k[X]/(rX-1) satsfies is_localization_away(r), (although a not very elegant one), and based on that, a proof that localization_away(r) is finitely presented. I can check whether my proof of finitely presentation of the localization away map connects nicely to what is done here. Except if it would be preferrable of doing it through adjoin_root?

@nick-kuhn So you didn't use adjoin_root API? Notice that adjoin_root f = (polynomial R ⧸ ideal.span {f}) definitionally, and it would be nice to show finite presentation more generally for adjoin_root. Did you even go through polynomial, or go straight to mv_polynomial?

I guess I'll just do it, and you can check if anything could be improved over my version.

I just checked and what you did here is much shorter and more elegant, so please go ahead!

Alright, the proof of

lemma is_localization.away.finite_presentation {R} [comm_ring R] (r : R) {S} [comm_ring S] [algebra R S]
  [is_localization.away r S] : algebra.finite_presentation R S :=

is now complete and the PR is again ready for review. Thanks @nick-kuhn for taking a look. I'm sorry for putting aside this PR for a long period; if it's in mathlib earlier you probably won't spend your time on this.

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests