sheaf annihilator and quasi-coherent ideal sheaves#4
Open
chrisflav wants to merge 9 commits into
Open
Conversation
chrisflav
commented
Jun 27, 2026
chrisflav
commented
Owner
Introduce the annihilator ideal sheaf of a sheaf of modules over a general site, formulated in the language of (pre)sheaves of modules. - `PresheafOfModules.SubmoduleSystem`: a restriction-stable family of submodules of a presheaf of modules, cutting out a subobject (`toPresheafOfModules`) with its inclusion monomorphism (`ι`). - `PresheafOfModules.annihilatorIdeal`/`annihilator`: the local annihilator (sections of `R` whose every restriction annihilates `M`), a subobject of the unit, with `mem_annihilatorIdeal` and the contravariance lemma `annihilatorIdeal_le_of_surjective`. - `SheafOfModules.annihilator`: the annihilator as a sheaf of modules, together with its monomorphism into `unit R`. The sheaf condition is proved by the covering-closure argument for the underlying subpresheaf of the sheaf `R`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
commented
Jun 27, 2026
chrisflav
added
the
awaiting-orchestra
Address review on PR chrisflav#4: - make `PresheafOfModules.Submodule` a `protected structure` - add the `CompleteLattice` structure (pointwise order, via `completeLatticeOfInf`) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
added
awaiting-auto-review
and removed
awaiting-orchestra
…af condition, docstrings) - Make presieveIsSheaf_comp_forget a single public lemma; remove the duplicated private copy in Quasicoherent.lean. - Extract PresheafOfModules.Submodule.toSubfunctor and isSheaf_toPresheafOfModules, factoring the subfunctor sheaf-condition boilerplate; migrate SheafOfModules.annihilator to use it. - Rename annihilatorSystem to annihilatorSubmodule. - Drop @[simp] from mem_annihilatorIdeal. - Update stale 'left for future work' docstrings now that orderIsoQuasicoherentIdealSheaf is delivered. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
commented
Jun 27, 2026
Comment on lines
+119
to
+123
| instance : CompleteLattice M.Submodule := | ||
| completeLatticeOfInf _ fun S ↦ by | ||
| refine ⟨fun N hN X ↦ ?_, fun N hN X ↦ ?_⟩ | ||
| · simpa only [sInf_toSubmodule] using iInf₂_le N hN | ||
| · simpa only [sInf_toSubmodule] using le_iInf₂ fun N' hN' ↦ hN hN' X |
Owner
Author
There was a problem hiding this comment.
Construct the CompleteLattice as it is done for SubmonoidFunctor's. Provide the lemmas confirming the def-eqs for inf and sup constructions.
chrisflav
added
the
awaiting-orchestra
…idFunctor style) Per review: replace completeLatticeOfInf with explicit sup/inf/sSup/sInf/top/bot fields + @[simps] def-eq lemmas. Also fixes pre-existing ext over-application in le_antisymm. sup/sSup map_mem proofs still WIP: element-type mismatch because M.map f lands in (restrictScalars).obj (M.obj Y). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
removed
the
awaiting-orchestra
…sheaf lemma
Subobject.lean: complete the WIP explicit CompleteLattice instance — supply
the missing map_mem fields for bot/top, and prove the sup/sSup additivity
steps through (M.presheaf.map f).hom (the underlying additive map) so they no
longer require a Module instance on the restrictScalars target. Add
respectTransparency false for the membership goals.
Annihilator.lean: pin isSheaf_toPresheafOfModules to PresheafOfModules.{max v₁ u₁}.
The PR-review extraction generalized it to universe v but the reverse criterion
isSheaf_iff_isSheaf_forget needs the value category at Type (max v₁ u₁); the sole
use site (SheafOfModules.annihilator) is exactly at that universe.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
added a commit
to chrisflav-agents/mathlib-staging
that referenced
this pull request
Jun 28, 2026
…al sheaves) Integrate the diff from chrisflav/mathlib4#4 into the staging library following the mirror hierarchy: each new `Mathlib/...` file is added as its `MathlibStaging/...` counterpart. Imports of the eight co-staged modules are rewritten to the mirror hierarchy, stable mathlib imports are kept as `Mathlib.*`, and every file imports `MathlibStaging.Init`. To let these module-system mirror files import the staging prelude, convert `MathlibStaging.Init` and `MathlibStaging.Linter.Staging` to `module` files (a `module` file cannot import a non-`module` file), mirroring how `Mathlib.Init` aggregates mathlib's own linters. The aggregator `MathlibStaging.lean` is regenerated with `mk_all`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.