[Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections#18160
[Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections#18160
Conversation
…ry of presheaves of modules
PR summary ca1a155f7fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 1555 | 1 | erw |
Current commit ca1a155f7f
Reference commit 23ecdee3fc
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
|
This PR/issue depends on: |
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
|
||
| In this file, given a presheaf of rings `R` on a category `C`, | ||
| we construct a set `FreeYoneda R` of presheaves of modules that | ||
| is separating and detecting: this set consists of presheaves of |
There was a problem hiding this comment.
I'm not an expert in this area but I would like to see progress in algebraic geometry so I'm attempting to review anyway! This terminology was hard for me to understand. Is a "separating set" the same as a "family of generators" in the sense of https://en.wikipedia.org/wiki/Generator_(category_theory) ?
Edit: Aah, just reading the code and looking at the docstrings is answering my questions. Maybe you could highlight
PresheafOfModules.freeYoneda.isSeparating : IsSeparating (freeYoneda R)
PresheafOfModules.freeYoneda.isDetecting : IsDetecting (freeYoneda R) as "main results" in the module docstring?
There was a problem hiding this comment.
Thanks for the reviews! I have rewritten the module docstring.
| /-- The set of `PresheafOfModules.{v} R` consisting of objects of the | ||
| form `(free R).obj (yoneda.obj X)` for some `X`. -/ | ||
| def freeYoneda : Set (PresheafOfModules.{v} R) := Set.range (yoneda ⋙ free R).obj | ||
|
|
There was a problem hiding this comment.
Aah, you could have used yoneda ⋙ free R earlier, for example line 43 could have been (((yoneda ⋙ free R).obj X) ⟶ M) ≃ M.obj (Opposite.op X) . Is it worth choosing a standard form for this?
There was a problem hiding this comment.
When applied on a X, the better (dsimp) form is (free R).obj (yoneda.obj X).
| lemma fromFreeYonedaCoproduct_app_mk (e : M.Elements) : | ||
| M.fromFreeYonedaCoproduct.app _ (M.freeYonedaCoproductMk e) = e.2 := by | ||
| dsimp [freeYonedaCoproductMk] | ||
| erw [M.ι_fromFreeYonedaCoproduct_apply e] |
There was a problem hiding this comment.
Do you know why rw [M.ι_fromFreeYonedaCoproduct_apply e e.fst (ModuleCat.freeMk (𝟙 (Opposite.unop e.fst)))] doesn't work?
There was a problem hiding this comment.
This is basically the same reason why ι_fromFreeYonedaCoproduct_apply cannot be a simp lemma, as, according to the linter, it is not in simpNF. If we apply dsimp to the statement, for the "human" eye, nothing changes, but there are hidden changes behind a DFunLike.coe: the definition of some types can be unfolded by dsimp. See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/attribute.20simp_NF_my_lemma.3F/near/443101462
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
|
Thanks! bors merge |
…generated by their sections (#18160) We provide a presentation of any presheaf of modules involving coproducts of free presheaves of modules generated by Yoneda presheaves of types. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
…generated by their sections (#18160) We provide a presentation of any presheaf of modules involving coproducts of free presheaves of modules generated by Yoneda presheaves of types. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
We provide a presentation of any presheaf of modules involving coproducts of free presheaves of modules generated by Yoneda presheaves of types.