feat(Algebra/WLocalization): fill sorries for Stratification.Index and ProdStrata.map#115
Open
chrisflav wants to merge 4 commits into
Open
Conversation
…and `ProdStrata.map` Fill four `sorry` placeholders in `Proetale/Algebra/WLocalization/Basic.lean`: * `Stratification.Index.restrict.disjoint` and `union_eq`: the restriction of a disjoint union decomposition `F = F' ⨿ F''` to a subset `E ⊆ F`. * `Stratification.Index.iUnion_stratum`: the strata `Z(E', E'')` cover `Spec A` (Stacks blueprint `lemma:subset-stratification`). * `ProdStrata.mapsTo_map_specComap`: the transition map between stratification products sends `V(I_F)` to `V(I_E)` (blueprint `lemma:finite-stratification-map-closed`). Two auxiliary lemmas are added: * `Generalization.map_mem_ideal_of_strata`: if `I ≤ I'` and `f ∣ f'`, the transition map `Generalization f I → Generalization f' I'` sends the kernel ideal into the kernel ideal. * `ProdStrata.map_apply`: the index-wise formula for the transition map between stratification products. Adds `\leanok` to the corresponding blueprint proofs in `blueprint/src/chapters/local-structure.tex`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
chrisflav
added
archon
`Proetale/Mathlib/CategoryTheory/Sites/PrecoverageGenerating.lean` was added in chrisflav#112 but the project index file `Proetale.lean` was not regenerated. Run `lake exe mk_all --git` to add the missing import so that validation passes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Restate `map_mem_ideal_of_strata` as ideal containment `map_ideal_le`. - Factor the localized-quotient zero-iff into `toLocQuotient_algebraMap_eq_zero_iff`. - Replace open-coded Finset partition in `iUnion_stratum` with `Finset.disjoint_filter_filter_not` / `Finset.filter_union_filter_not_eq`. - Add `Stratification.Index.function_restrict_dvd_function` and `ideal_restrict_le` so the divisibility / span obligations have names. - Extract `ProdStrata.locClosedSubset_subset_restrict` and reuse it in `map` and `map_apply`; tag `map_apply` as `@[simp]`. - Add `ProdStrata.map_ideal_le` and rewrite `mapsTo_map_specComap` to use it, removing the `change` step. - Consolidate `classical` annotations in `Stratification.Index.restrict`.
Address the `linter.style.show` warnings turned errors by the validation script's `--wfail` flag.
chrisflav
removed
the
awaiting-auto-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.
Fill four
sorryplaceholders in theStratification.Index/ProdStratasection ofProetale/Algebra/WLocalization/Basic.lean:WLocalization.Stratification.Index.restrict.disjointandunion_eq: the restriction of a disjoint union decompositionF = F' ⨿ F''to a subsetE ⊆ F.WLocalization.Stratification.Index.iUnion_stratum: the strataZ(E', E'')coverSpec A(blueprintlemma:subset-stratification).WLocalization.ProdStrata.mapsTo_map_specComap: the transition map between stratification products sendsV(I_F)toV(I_E)(blueprintlemma:finite-stratification-map-closed).Two helper lemmas are introduced:
WLocalization.Generalization.map_mem_ideal_of_strata: ifI ≤ I'andf ∣ f', the canonical mapGeneralization f I → Generalization f' I'sends the kernelideal f Iinto the kernelideal f' I'.WLocalization.ProdStrata.map_apply: the index-wise formula for the transition map between stratification products.Adds
\leanokto the corresponding blueprint proofs inblueprint/src/chapters/local-structure.tex.Test plan
lake env lean Proetale/Algebra/WLocalization/Basic.leanreports no new errors introduced by these changes; the remaining diagnostics are pre-existing onmaster(thebijectiveOnStalks_algebraMap/indZariskisorries downstream of this section).🤖 Generated with Claude Code