feat(Algebra/IndZariski): fill bijectiveOnStalks_algebraMap and of_colimitPresentation sorries#92
Open
chrisflav wants to merge 5 commits into
Conversation
…_colimitPresentation` Adds the helper `Algebra.IndZariski.bijectiveOnStalks_of_colimitPresentation` showing that bijectivity on stalks transports along a filtered colimit presentation, then uses it to close the two open sorries in the file: * `Algebra.IndZariski.bijectiveOnStalks_algebraMap` (Stacks 096T): every ind-Zariski algebra map is bijective on stalks. * `Algebra.IndZariski.of_colimitPresentation`: a filtered colimit of ind-Zariski algebras is ind-Zariski. Also adds `\leanok` to the proof block of the corresponding blueprint lemma `thm:ind-Zariski-identifies-local-rings`.
chrisflav
commented
May 22, 2026
Owner
Author
|
orchestra polish |
Apply review-code style guide: drop redundant variable redeclarations that shadow the section variables, replace the `change` tactic with a term-mode `DFunLike.congr_fun (congrArg ...)`, move `have` binders to the left of the colon, and add the missing docstring on `of_colimitPresentation`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
commented
May 23, 2026
Owner
Author
|
orchestra address review |
…ete-category API Address PR chrisflav#92 review feedback: - Refactor `bijectiveOnStalks_of_colimitPresentation` and `bijectiveOnStalks_algebraMap` to use the `Algebra.BijectiveOnStalks` class rather than the `(algebraMap …).BijectiveOnStalks` ring-hom property. - Replace usages of `Types.jointly_surjective_of_isColimit` and `Types.FilteredColimit.isColimit_eq_iff'` by the corresponding `Concrete.isColimit_exists_rep` and `IsColimit.eq_iff'` from `Mathlib.CategoryTheory.Limits.ConcreteCategory.{Basic,Filtered}`. - Update call sites in `WContractible` and `WLocalization/Basic` to convert between the algebra and ring-hom forms via `RingHom.bijectiveOnStalks_algebraMap`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
added
awaiting-auto-review
…` namespace `bijectiveOnStalks_of_colimitPresentation` is a general fact about filtered colimits and `Algebra.BijectiveOnStalks`; it has no `IndZariski` hypothesis. Move it from `Algebra.IndZariski` to `Algebra.BijectiveOnStalks` and rename to `of_colimitPresentation` so the qualified name reflects its content, and update the single in-file call site.
chrisflav
removed
the
awaiting-auto-review
chrisflav
commented
May 26, 2026
Comment on lines
+301
to
+308
| /-- If `S` is a filtered colimit of `R`-algebras `Aᵢ` and each `R → Aᵢ` is bijective on | ||
| stalks, then so is `R → S`. -/ | ||
| lemma of_colimitPresentation {ι : Type u} [SmallCategory ι] [IsFiltered ι] | ||
| (P : ColimitPresentation ι (CommAlgCat.of R S)) | ||
| (h : ∀ i, Algebra.BijectiveOnStalks R (P.diag.obj i)) : | ||
| Algebra.BijectiveOnStalks R S := by | ||
| refine ⟨fun p hp ↦ ?_⟩ | ||
| have hcomm (i : ι) (r : R) : |
Owner
Author
There was a problem hiding this comment.
Show first that the localization of a filtered colimit of rings at a prime ideal is the filtered colimit of the localizations. Then show that the Localization.localRingHom map here is induced by the stalk maps on the components. Deduce from this that the map is bijective.
chrisflav
added
the
awaiting-orchestra
…eOnStalks` Address review feedback on PR chrisflav#92 by dropping the redundant `_algebraMap` suffix and updating the blueprint `\lean` label.
chrisflav
added
awaiting-orchestra
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.
Summary
Closes the two remaining
sorrys inProetale/Algebra/IndZariski.leanfor ind-Zariski-related stalk bijectivity statements.Algebra.IndZariski.bijectiveOnStalks_of_colimitPresentation:if
S = colim_i A_iasR-algebras and eachR → A_iis bijective on stalks,then so is
R → S.Algebra.IndZariski.bijectiveOnStalks_algebraMap(Stacks 096T): every ind-Zariski algebra map identifies local rings.
Algebra.IndZariski.of_colimitPresentation: a filtered colimit ofind-Zariski algebras is ind-Zariski, via
iff_ind_isLocalIsoandObjectProperty.ind_indapplied toCommAlgCat.isLocalIso_le_isFinitelyPresentable.\leanokto the proof block of the corresponding blueprint lemmathm:ind-Zariski-identifies-local-rings.The code is extracted from the
archonbranch.Test plan
lake buildsucceeds on the full project.