feat(Algebra/IndZariski): fill `bijectiveOnStalks_algebraMap` and `of_colimitPresentation` sorries by chrisflav · Pull Request #92 · chrisflav/proetale

chrisflav · 2026-05-22T21:18:51Z

Summary

Closes the two remaining sorrys in Proetale/Algebra/IndZariski.lean for ind-Zariski-related stalk bijectivity statements.

Adds the helper Algebra.IndZariski.bijectiveOnStalks_of_colimitPresentation:
if S = colim_i A_i as R-algebras and each R → A_i is bijective on stalks,
then so is R → S.
Uses it to close Algebra.IndZariski.bijectiveOnStalks_algebraMap
(Stacks 096T): every ind-Zariski algebra map identifies local rings.
Closes Algebra.IndZariski.of_colimitPresentation: a filtered colimit of
ind-Zariski algebras is ind-Zariski, via iff_ind_isLocalIso and
ObjectProperty.ind_ind applied to CommAlgCat.isLocalIso_le_isFinitelyPresentable.
Adds \leanok to the proof block of the corresponding blueprint lemma
thm:ind-Zariski-identifies-local-rings.

The code is extracted from the archon branch.

Test plan

lake build succeeds on the full project.

…_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 · 2026-05-22T21:30:04Z

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 · 2026-05-23T09:56:04Z

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>

…` 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.

…eOnStalks` Address review feedback on PR chrisflav#92 by dropping the redundant `_algebraMap` suffix and updating the blueprint `\lean` label.

…esentation Extract two private helper lemmas matching the reviewer's structural strategy: - exists_localRingHom_eq: every element of Localization.AtPrime p lifts from Localization.AtPrime pᵢ for some i (existence half of colimit characterization) - exists_localRingHom_eq_of_localRingHom_eq: if two elements of Loc.q have equal images in Loc.p, they have equal images in Loc.pⱼ for some j (equality half) The main of_colimitPresentation proof now factors through these helpers plus RingHom.BijectiveOnStalks.localRingHom_of_eq. Not yet compiling — surjectivity case has a residual goal coercing between algebraMap R S and (P.ι.app i).hom.comp (algebraMap R Aᵢ). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Address PR review feedback: refactor `of_colimitPresentation` so the proof factors through the conceptual steps `localization of filtered colimit at a prime = filtered colimit of localizations` and the resulting bijectivity of the induced `Localization.localRingHom`. The refactor extracts two private helper lemmas: `exists_localRingHom_eq` (existence of lifts) and `exists_localRingHom_eq_of_localRingHom_eq` (filtered colimit of equalities), supported by `colimitPrime` / `colimitPrime_comap_algebraMap` / `colimitPrime_comap_diag`. The main `of_colimitPresentation` proof then combines these with bijectivity of each stalk to get bijectivity of the colimit's stalk. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

chrisflav · 2026-05-31T22:25:34Z

Show that if p is a prime of R and R is the filtered colimit of rings R_i, then the localization of R at the prime p is isomorphic to the filtered colimit of the localizations of R_i at the preimages of p in R_i.

…isColimitLocalizationCocone Address PR chrisflav#92 reviewer comment requesting refactor: 'Show that ... the localization of R at the prime p is isomorphic to the filtered colimit of the localizations of R_i at the preimages of p in R_i.' Adds: - localizationDiag P p : ι ⥤ CommRingCat, the diagram of localizations at preimages, with Localization.localRingHom transitions. - localizationCocone P p : Cocone with apex Localization.AtPrime p. - isColimitLocalizationCocone : IsColimit (localizationCocone P p), proved by reflection through the forgetful functor to Type and Types.FilteredColimit.isColimitOf'. Refactors of_colimitPresentation to use the new iso. WIP: compilation still has errors to address; pushing to preserve state. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…ding for iso lemma Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…itLocalizationCocone Add categorical infrastructure addressing review feedback on PR chrisflav#92: * `Algebra.BijectiveOnStalks.localizationDiag P p`: the diagram `i ↦ Localization.AtPrime (colimitPrime P p i)` with transition maps the canonical `Localization.localRingHom`s. * `Algebra.BijectiveOnStalks.localizationCocone P p`: the cocone with apex `Localization.AtPrime p` induced by the colimit injections. * `Algebra.BijectiveOnStalks.isColimitLocalizationCocone P p`: shows that this cocone is a colimit. Together these encode the statement that the localization of a filtered colimit of `R`-algebras at a prime `p` is the filtered colimit of the localizations at the preimages of `p`. The IsColimit proof reduces to the type-level criterion via the forgetful functor (which preserves filtered colimits and reflects isomorphisms), combining the existing `exists_localRingHom_eq` (surjectivity) with a new private helper `exists_eq_of_localRingHomDiag_eq` generalising the existing injectivity helper from the base ring `R` to arbitrary diagram constituents. Also: fix `colimitPrime_comap_diag` which broke after the recent Mathlib bumps. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

- Move BijectiveOnStalks colimit material to new file Proetale/Algebra/BijectiveOnStalks/ColimitPresentation.lean - Restore bijectiveOnStalks_algebraMap returning (algebraMap R S).BijectiveOnStalks and add an Algebra.BijectiveOnStalks instance for IndZariski algebras - Extract ColimitPresentation.ι_app_diag_map_apply helper, dedupe hnat - Trim proof-strategy commentary from docstrings - Replace `;`-chained tactics, remove `linear_combination` for `exact` - Drop the offending `rfl` after a closing `rw` - Update call sites in WContractible and WLocalization/Basic - Update blueprint reference to the restored name Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…ack round 2 - Make `colimitPrime`, `localizationDiag`, `localizationCocone`, `isColimitLocalizationCocone` and their comap lemmas public (they are genuinely general results about localization commuting with filtered colimits of `R`-algebras). - Move the namespace from `Algebra.BijectiveOnStalks.ColimitPresentation` to `Localization.AtPrime.ColimitPresentation`, which is the natural algebraic scope. - Move `ColimitPresentation.ι_app_diag_map_apply` to the CommAlgCat mirror file and add new helpers `diag_map_id_apply`, `diag_map_comp_apply`, and `ι_app_algebraMap_apply` so the colimit file no longer reaches for raw `(P.diag.map _).map_id`/`map_comp`. - Use these helpers + add `localizationDiag_map_apply` and `localizationCocone_ι_app_apply` `@[simp]` lemmas to eliminate several `change`s and the `simp ...; exact h` -> `simpa using h` pattern. - Rename `exists_eq_of_localRingHomDiag_eq` to `exists_localizationDiag_map_eq`. - Inline the `refine ... ?_ ; exact ...` in `IndZariski.bijectiveOnStalks_algebraMap` into a single `exact`.

jjdishere · 2026-06-09T04:13:31Z

orchestra address review

… direction, drop privates - Rename `colimitPrime` to `contractionIdeal` and propagate to dependent lemma names and the prime-ideal instance (now named `contractionIdeal.isPrime`). - Reverse the direction of `contractionIdeal_comap_algebraMap` and `contractionIdeal_comap_diag` and tag them `@[simp]`. - Drop the unused `localizationDiag_map_apply` simp lemma. - Drop `@[simp]` from `localizationCocone_ι_app_apply`. - Make `exists_localRingHom_eq` and `exists_localRingHom_eq_of_localRingHom_eq` public. - Replace the omitted blueprint proof of `thm:ind-Zariski-identifies-local-rings` with a natural-language proof.

Add the missing `Proetale.Mathlib.AlgebraicGeometry.AffineTransitionLimit` and `Proetale.Mathlib.AlgebraicGeometry.Sites.AffineEtale` entries via `lake exe mk_all --git`, which the validation script enforces.

jjdishere · 2026-06-09T05:30:20Z

Please check and fix documentation build.

jjdishere · 2026-06-09T05:42:15Z

orchestra address review

- Add @[simp] to ColimitPresentation.ι_app_diag_map_apply. - Drop @[simp] from ColimitPresentation.diag_map_id_apply since it is only used explicitly, not via simp. - Sharpen the docstring of ι_app_algebraMap_apply to describe the diagram-level statement rather than the vague phrase "colimit injection commutes". - Drop `private` from `exists_localizationDiag_map_eq`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

jjdishere · 2026-06-09T05:54:45Z

merge master.

jjdishere · 2026-06-09T05:54:54Z

orchestra address review

…jective-on-stalks

Subscripting `\mathfrak{q}` via `_\mathfrak{q}` confuses unicode-math (`_` grabs `\mathfrak` before its argument is read), aborting the blueprint PDF build. Wrap subscripts in explicit braces and simplify the prose to a concise natural-language proof that avoids the ad-hoc `\varphi` notation. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

chrisflav added the archon Upstreamed from `archon` branch label May 22, 2026

chrisflav commented May 22, 2026

View reviewed changes

Comment thread Proetale/Algebra/IndZariski.lean Outdated

chrisflav commented May 23, 2026

View reviewed changes

Comment thread Proetale/Algebra/IndZariski.lean Outdated

chrisflav added awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. and removed awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. labels May 23, 2026

chrisflav removed the awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. label May 23, 2026

chrisflav commented May 26, 2026

View reviewed changes

Comment thread Proetale/Algebra/IndZariski.lean

Comment thread Proetale/Algebra/IndZariski.lean Outdated

chrisflav added the awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. label May 26, 2026

chore(IndZariski): rename bijectiveOnStalks_algebraMap to `bijectiv…

df06d9e

…eOnStalks` Address review feedback on PR chrisflav#92 by dropping the redundant `_algebraMap` suffix and updating the blueprint `\lean` label.

chrisflav added awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. and removed awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. labels May 26, 2026

chrisflav and others added 2 commits May 31, 2026 11:08

chrisflav removed the awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. label May 31, 2026

Merge branch 'master' into pr/ind-zariski-bijective-on-stalks

4ef0c4f

chrisflav added the awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. label May 31, 2026

chrisflav and others added 5 commits May 31, 2026 22:57

WIP refactor(Algebra/IndZariski): partial fixes for new iso lemmas

a18ce1a

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

WIP refactor(Algebra/IndZariski): add localizationDiag/Cocone scaffol…

f5ab170

…ding for iso lemma Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

style(Algebra/IndZariski): replace show with change per linter

f74d7ae

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

chrisflav added awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. and removed awaiting-orchestra A reviewer has made suggestions that are waiting to be implemented by orchestra. labels May 31, 2026

chrisflav and others added 3 commits June 1, 2026 11:02

WIP: address PR feedback - move colimit block to new file (in progress)

bba30bf

WIP refactor: move BijectiveOnStalks colimit block to new file

34ec9a0

chrisflav added awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. and removed awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. labels Jun 1, 2026

chrisflav removed the awaiting-auto-review This PR is scheduled to receive an automatic review through orchestra. label Jun 2, 2026

Merge branch 'master' into pr/ind-zariski-bijective-on-stalks

7fb8e77

jjdishere reviewed Jun 9, 2026

View reviewed changes

chrisflav added 2 commits June 9, 2026 04:24

chore: regenerate Proetale.lean umbrella imports

77749d0

Add the missing `Proetale.Mathlib.AlgebraicGeometry.AffineTransitionLimit` and `Proetale.Mathlib.AlgebraicGeometry.Sites.AffineEtale` entries via `lake exe mk_all --git`, which the validation script enforces.

jjdishere reviewed Jun 9, 2026

View reviewed changes

chrisflav and others added 2 commits June 9, 2026 05:57

Merge remote-tracking branch 'upstream/master' into pr/ind-zariski-bi…

0666e8c

…jective-on-stalks

Conversation

chrisflav commented May 22, 2026

Summary

Test plan

Uh oh!

Uh oh!

chrisflav commented May 22, 2026

Uh oh!

Uh oh!

chrisflav commented May 23, 2026

Uh oh!

Uh oh!

Uh oh!

chrisflav commented May 31, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jjdishere commented Jun 9, 2026

Uh oh!

jjdishere commented Jun 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jjdishere commented Jun 9, 2026

Uh oh!

jjdishere commented Jun 9, 2026

Uh oh!

jjdishere commented Jun 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants