feat(Algebra/WLocalization): fill sorries for Generalization API#104
Open
chrisflav wants to merge 3 commits into
Open
feat(Algebra/WLocalization): fill sorries for Generalization API#104chrisflav wants to merge 3 commits into
Generalization API#104chrisflav wants to merge 3 commits into
Conversation
Fill the five `sorry` placeholders in the `WLocalization.Generalization` section of `Proetale/Algebra/WLocalization/Basic.lean`: * `range_algebraMap_generalization`: identify the image of `Spec (Generalization f I) → Spec A` with the generalization hull of `D(f) ∩ V(I)`. * `bijOn_algebraMap_generalization_specComap_zeroLocus_ideal`: the closed subscheme `V(ideal f I)` maps bijectively onto `D(f) ∩ V(I)`. * `submonoid_le`: monotonicity of `submonoid f I` along inclusions of locally closed subsets. * `Generalization.map.commutes'`: the `A`-algebra structure of `map h` is provided by `IsLocalization.liftAlgHom`. * `exists_specializes_zeroLocus_ideal`: every point of `Spec (Generalization f I)` specializes to a point of `V(ideal f I)`. This corresponds to `lemma:locally-closed-specializations` in `blueprint/src/chapters/local-structure.tex`; the proof now carries a `\leanok`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
added
archon
Address review feedback on PR chrisflav#104: - Drop redundant `submonoid_disjoint_locClosedSubset_primes` helper; its content is now a 1-line corollary of the iff lemma. - Rename `mem_submonoid_iff_not_mem_locClosedSubset` to `mem_submonoid_iff` and prove both directions symmetrically via `PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit`. - Extract the prime lift used by both `bijOn_…` and `exists_specializes_zeroLocus_ideal` into the private lemma `exists_mem_zeroLocus_ideal_specComap_eq`. - Use `IsLocalization.isPrime_iff_isPrime_disjoint` in the `mapsTo` branch of `bijOn_…` to obtain disjointness directly. - Reorder declarations so the iff comes first and the proofs read top-down. - Drop stale planning comments, `with hq_def` binders, unused `set f_bar`/`set a_bar` indirection, and the double blank line. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
added
awaiting-auto-review
chrisflav
commented
May 24, 2026
chrisflav
added
the
awaiting-orchestra
- unprivate `mem_submonoid_iff` as it is a general purpose lemma - avoid `change` tactic in favor of explicit API lemmas Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
removed
the
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.
Fill the five
sorryplaceholders in theWLocalization.Generalizationsection ofProetale/Algebra/WLocalization/Basic.lean:range_algebraMap_generalization: identifies the image ofSpec (Generalization f I) → Spec Awith the generalization hull ofD(f) ∩ V(I).bijOn_algebraMap_generalization_specComap_zeroLocus_ideal: the closed subschemeV(ideal f I) ⊂ Spec (Generalization f I)maps bijectively ontoD(f) ∩ V(I).submonoid_le: monotonicity ofGeneralization.submonoid f Ialong inclusions of locally closed subsetsD(f') ∩ V(I') ⊆ D(f) ∩ V(I).Generalization.map.commutes': theA-algebra structure of the transition map between generalizations.exists_specializes_zeroLocus_ideal: every point ofSpec (Generalization f I)specializes to a point ofV(ideal f I).The proofs use two private helper lemmas:
submonoid_disjoint_locClosedSubset_primes(forward direction of the membership criterion) andmem_submonoid_iff_not_mem_locClosedSubset(characterisingsubmonoid f Ivia primes inD(f) ∩ V(I)).This corresponds to
lemma:locally-closed-specializationsinblueprint/src/chapters/local-structure.tex; the informal proof is now annotated with\leanok.Test plan
lake build Proetale.Algebra.WLocalization.Basicsucceeds with no warnings.bash .agent/validation.shpasses (full project build with--wfail).🤖 Generated with Claude Code