feat(Algebra/StalkIso): prove BijectiveOnStalks for local isos and properties#25
Open
chrisflav wants to merge 7 commits intochrisflav:masterfrom
Open
feat(Algebra/StalkIso): prove BijectiveOnStalks for local isos and properties#25chrisflav wants to merge 7 commits intochrisflav:masterfrom
chrisflav wants to merge 7 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
Comment on lines
+102
to
+105
| lemma RingHom.injective_of_injectiveOnStalks_of_surjective_comap {f : R →+* S} | ||
| (hf : ∀ (p : Ideal S) [p.IsPrime], | ||
| Function.Injective (Localization.localRingHom (p.comap f) p f rfl)) | ||
| (hb : Function.Surjective (PrimeSpectrum.comap f)) : Function.Injective f := by |
Owner
Author
There was a problem hiding this comment.
It should be sufficient to take maximal ideals here by using MaximalSpectrum.toPiLocalization_injective.
Owner
Author
There was a problem hiding this comment.
Also move these general lemmas to the right place.
Comment on lines
+117
to
+121
| /-- A ring homomorphism `f : R →+* S` is flat if the induced maps on localizations at each | ||
| prime are flat. -/ | ||
| lemma RingHom.flat_of_localizations_flat {f : R →+* S} | ||
| (h : ∀ (p : Ideal S) [p.IsPrime], | ||
| (Localization.localRingHom (p.comap f) p f rfl).Flat) : |
Owner
Author
There was a problem hiding this comment.
This also only needs to check at maximal ideals.
Comment on lines
+136
to
+140
| /-- A ring homomorphism `f : R →+* S` is surjective if for every `s : S` and every maximal | ||
| ideal `m` of `R`, there exists `r ∉ m` such that `f r * s ∈ f.range`. -/ | ||
| lemma RingHom.surjective_of_range_criterion {f : R →+* S} | ||
| (h : ∀ (s : S) (m : Ideal R), m.IsMaximal → ∃ r : R, r ∉ m ∧ f r * s ∈ f.range) : | ||
| Function.Surjective f := by |
Owner
Author
There was a problem hiding this comment.
The converse of this is also true, prove this as well. Also, the name is wrong, it should be RingHom.surjective_of_forall_isMaximal_exists.
Comment on lines
+167
to
+170
| letI := (Localization.localRingHom (Ideal.comap f P) P f rfl).toAlgebra | ||
| show Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) | ||
| exact Module.Flat.of_linearEquiv | ||
| (LinearEquiv.ofBijective (Algebra.linearMap _ _) (hf P)).symm |
Owner
Author
There was a problem hiding this comment.
Use RingHom.Flat.of_bijective here.
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.
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.