feat(Algebra/StalkIso): prove BijectiveOnStalks for local isos and properties#25
Open
chrisflav wants to merge 12 commits intochrisflav:masterfrom
Open
feat(Algebra/StalkIso): prove BijectiveOnStalks for local isos and properties#25chrisflav wants to merge 12 commits intochrisflav:masterfrom
chrisflav wants to merge 12 commits intochrisflav:masterfrom
Conversation
…operties Prove that local isomorphisms are bijective on stalks, that BijectiveOnStalks is stable under composition, and that a ring homomorphism that is bijective on stalks and induces a bijection on prime spectra is itself bijective.
- Simplify hcomap_comp and hcomap_R using `← Ideal.comap_comap` instead of the verbose `show ... from` construction - Remove redundant `change` in the algebraMap condition proof in h_comp_bij; use `.symm` of IsScalarTower.algebraMap_apply directly - Inline hJ_add and hJ_smul helpers into the J_s structure definition - Simplify hJ_ne_top to a one-liner using typed ascription - Replace hkey2 calc block with `linear_combination` - Simplify hkey3 to two lines Total: 227 → 209 lines (-18 lines) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 18, 2026
Owner
Author
|
orchestra address review |
1 similar comment
Owner
Author
|
orchestra address review |
The lemma BijectiveOnStalks.prod was accidentally removed in the refactoring commit. Restore it with sorry as the proof is not yet filled. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 19, 2026
- Add @[algebraize] attribute and toAlgebra lemma to RingHom.IsLocalIso - Use algebraize [f] instead of manual haveI for Algebra.IsLocalIso instance - Replace haveI with letI for IsScalarTower instance in proof - Replace change tactic with simp only using Pi.algebraMap_apply - Restore prod lemma to original signature without hypotheses Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Owner
Author
|
orchestra polish |
1 similar comment
Owner
Author
|
orchestra polish |
- Replace `haveI` with `letI` in tactic proofs - Replace `fun ... =>` with `fun ... ↦` throughout - Break line exceeding 100 characters - Remove `change` tactic in favour of definitional equality Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Owner
Author
|
orchestra polish |
4 similar comments
Owner
Author
|
orchestra polish |
Owner
Author
|
orchestra polish |
Owner
Author
|
orchestra polish |
Owner
Author
|
orchestra polish |
- Split semicolon-chained tactics onto separate lines - Replace `show ... from` inside `rw` with a `have` statement - Use `simpa` instead of `simp; exact` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 20, 2026
Owner
Author
|
orchestra address review |
- Extract injectivity proof into `RingHom.injective_of_injectiveOnStalks_of_surjective_comap` with minimal assumptions (injective stalks + surjective comap) - Extract flatness proof into `RingHom.flat_of_localizations_flat` (if flat on stalks, then flat) - Extract surjectivity criterion into `RingHom.surjective_of_range_criterion` - Replace `funext` with `ext` tactic - Replace `letI := f.toAlgebra` with `algebraize [f]` Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 20, 2026
Owner
Author
|
orchestra address review |
1 similar comment
Owner
Author
|
orchestra address review |
- Use `MaximalSpectrum.toPiLocalization_injective` in injectivity proof and weaken hypothesis to only require maximal ideals - Use `IsMaximal` instead of `IsPrime` in `flat_of_localizations_flat` - Rename `surjective_of_range_criterion` to `surjective_of_forall_isMaximal_exists` and prove the converse - Use `RingHom.Flat.of_bijective` for flatness in `bijective_of_bijective` - Move general ring hom lemmas to `Proetale/Mathlib/RingTheory/Spectrum/Prime/RingHom.lean` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 24, 2026
Owner
Author
|
orchestra address review |
1 similar comment
Owner
Author
|
orchestra address review |
- Change `injective_of_injectiveOnStalks` to use `[p.IsMaximal]` and `Function.Surjective (PrimeSpectrum.comap f)` for easier application - Remove explicit `@` usage in favor of `haveI` - Use `algebraize` instead of manual `letI := ...toAlgebra` - Rename `forall_isMaximal_exists_of_surjective` to `exists_mul_mem_range_of_surjective` - Remove unnecessary `have`s: rewrite directly in goals and hypotheses - Use `refine` instead of intermediate `have`s when building final term Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
jjdishere
reviewed
Mar 25, 2026
Collaborator
jjdishere
left a comment
jjdishere
left a comment
There was a problem hiding this comment.
Code Review
Overall this is solid work — the three main results are well-structured with good separation of general lemmas into Proetale/Mathlib/. A few style nits below.
…p_specializes Extract the going-down / specialization-reflection argument from `bijective_of_bijective` into a general topological lemma: an injective generalizing map reflects specialization. This simplifies the inline proof from ~10 lines to 3 lines. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
jjdishere
force-pushed
the
pr/stalkiso-bijective-on-stalks
branch
from
7ea6869 to
f927ea1
Compare
chrisflav
commented
Mar 25, 2026
Owner
Author
|
orchestra address review |
2 similar comments
Owner
Author
|
orchestra address review |
Owner
Author
|
orchestra address review |
Introduce `BijectiveOnStalks.of_localization` lemma showing that bijectivity on stalks can be checked after localizing at any element not in the prime. This locality property simplifies the proof of `IsLocalIso.bijectiveOnStalks` by reducing it to the standard open immersion case. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 27, 2026
Owner
Author
|
orchestra address review |
- Simplified of_localization signature to avoid long let statements - Added of_span_unit_ideal lemma for locality property - Still has compilation errors that need fixing Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
chrisflav
commented
Mar 27, 2026
Comment on lines
+39
to
+43
| /-- If `f : R →+* S` is bijective on stalks, then checking bijectivity at a prime `p` of `S` | ||
| can be done after localizing at any element not in `p`. -/ | ||
| lemma of_localization {f : R →+* S} (g : S) (p : Ideal S) [hp : p.IsPrime] (hgp : g ∉ p) | ||
| (Sg : Type*) [CommRing Sg] [Algebra S Sg] [IsLocalization.Away g Sg] | ||
| (h : let hpM : Disjoint (Submonoid.powers g : Set S) (↑p : Set S) := |
Owner
Author
There was a problem hiding this comment.
This lemma is not useful, inline it in the proof of of_span_unit_ideal. Then use of_span_unit_ideal below in RingHom.IsLocalIso.bijectiveOnStalks.
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
2 participants
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.
Proves three results about
RingHom.BijectiveOnStalks:RingHom.IsLocalIso.bijectiveOnStalks: local isomorphisms are bijective on stalks.RingHom.BijectiveOnStalks.comp: stability under composition.RingHom.BijectiveOnStalks.bijective_of_bijective: a ring homomorphism bijective on stalks that also induces a bijection on prime spectra is itself bijective.