feat(Algebra/WLocalization/Ideal): fill sorries for w-localization wrt ideal#40
Open
chrisflav wants to merge 3 commits into
Open
feat(Algebra/WLocalization/Ideal): fill sorries for w-localization wrt ideal#40chrisflav wants to merge 3 commits into
chrisflav wants to merge 3 commits into
Conversation
…t ideal Fill most sorries in `Proetale/Algebra/WLocalization/Ideal.lean`, proving: - `isWLocalRing_generalization_one`: w-local structure is preserved by Generalization 1 I - `IsWLocalRing.zeroLocus_map_algebraMap_generalization_one_eq`: the zero locus of the mapped ideal equals the closed points - `Ideal.WLocalization.indZariski`: the ideal w-localization is ind-Zariski - `zeroLocus_map_algebraMap_eq_closedPoints`: main zero locus characterization - `algebraMap_specComap_preimage_closedPoints_eq`: [Stacks 097A (2)(d)] Two sorries remain: `quotientMap_algebraMap_bijective` [097A (2)(a)] and the residue-field-algebraicity step in `zeroLocus_map_algebraMap_eq_closedPoints`, both depending on sorry'd upstream infrastructure. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Owner
Author
|
orchestra address review: Fill the missing |
- Fill `quotientMap_algebraMap_bijective` (Stacks 097A (2)(a)) by
composing two bijections through `WLocA/J`:
- α : A/I → WLocA/J via new helper
`WLocalization.quotientMap_algebraMap_bijective_of_ideal` (sorry'd)
- β : WLocA/J → I.WLocalization/(J.map(...)) via `IsLocalization.atUnits`
on the image submonoid (which consists of units in WLocA/J).
- Identify codomains via `Ideal.quotEquivOfEq`.
- Fill the residue-field-algebraicity sorry in
`zeroLocus_map_algebraMap_eq_closedPoints` by chaining
`IndZariski → IndEtale → isSeparable_residueField → IsAlgebraic`.
- Add `Ideal.WLocalization.isLocalization` instance.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
commented
May 5, 2026
Owner
Author
|
orchestra address review |
The helper `WLocalization.quotientMap_algebraMap_bijective_of_ideal` was false in general (e.g. I = 0 gives A → WLocA bijective). Per the blueprint (lemma:closed-closed-points-tilde-w-local), the correct hypothesis is `V(I) ⊆ closedPoints A`. Propagate this hypothesis to: - `WLocalization.quotientMap_algebraMap_bijective_of_ideal` - `Ideal.WLocalization.quotientMap_algebraMap_bijective` - `Ideal.WLocalization.bijOn_zeroLocus_map` Add an algebraicity-of-residue-fields hypothesis to `faithfullyFlat_map_algebraMap` (matching `algebraMap_specComap_preimage_closedPoints_eq`) to derive `V(I·B) ⊆ closedPoints B` for the call to `bijOn_zeroLocus_map`. Update the consumer in `WContractible.lean` accordingly. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
commented
May 5, 2026
Comment on lines
+270
to
+275
| lemma quotientMap_algebraMap_bijective_of_ideal (I : Ideal A) | ||
| (hI : zeroLocus I ⊆ closedPoints (PrimeSpectrum A)) : | ||
| Function.Bijective | ||
| (Ideal.quotientMap (I.map (algebraMap A (WLocalization A))) | ||
| (algebraMap A (WLocalization A)) I.le_comap_map) := | ||
| sorry |
Owner
Author
|
orchestra address review |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fill most sorries in
Proetale/Algebra/WLocalization/Ideal.lean, closing #39.What was proved
isWLocalRing_generalization_one:Generalization 1 Iis w-local whenAis w-local, using the embeddingSpec(Generalization 1 I) → Spec Awith specialization-stable range.IsWLocalRing.zeroLocus_map_algebraMap_generalization_one_eq: the zero locus of the mapped ideal equals the closed points, using the embedding lemma and the generalization hull structure.Ideal.WLocalization.indZariski: the ideal w-localization is ind-Zariski (by transitivity throughWLocalization A).zeroLocus_map_algebraMap_eq_closedPoints: the main zero locus characterization forI.WLocalization.algebraMap_specComap_preimage_closedPoints_eq[Stacks 097A (2)(d)]: proved by reducing tozeroLocus_map_algebraMap_eq_closedPoints.Remaining sorries
quotientMap_algebraMap_bijective[Stacks 097A (2)(a)]: requires faithful flatness and surjectivity results fromBasic.leanwhich are currently sorry'd.zeroLocus_map_algebraMap_eq_closedPoints(thatWLocalization Ahas algebraic residue field extensions overA): depends on sorry'dAlgebra.IndZariski.bijectiveOnStalks_algebraMapinIndZariski.lean.