Skip to content

[Merged by Bors] - feat(CategoryTheory): prestacks#30177

Closed
joelriou wants to merge 50 commits intoleanprover-community:masterfrom
joelriou:jriou-descent-2
Closed

[Merged by Bors] - feat(CategoryTheory): prestacks#30177
joelriou wants to merge 50 commits intoleanprover-community:masterfrom
joelriou:jriou-descent-2

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 3, 2025 •
edited
Loading

Let C be a category and F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat. Given S : C, and objects M and N in F.obj (.mk (op S)), we define a presheaf of types F.presheafHom M N on the category Over S: its sections on an object T : Over S corresponding to a morphism p : X ⟶ S are the type of morphisms p^* M ⟶ p^* N. We shall say that F satisfies the descent of morphisms for a Grothendieck topology J (i.e. F is a prestack) if these presheaves are all sheaves.

Co-authored-by: Christian Merten christian@merten.dev

This PR continues the work from #24411.

Original PR: #24411

joelriou and others added 26 commits April 26, 2025 10:18
@joelriou
feat(CategoryTheory): pseudofunctors from strict bicategories
4913881
@joelriou
better names
430466b
@joelriou
cleaning up
6d3eca6
@joelriou
whitespace
74dc8c5
@joelriou
cleaning up
6529163
@joelriou
better lemmas
45d4532
@joelriou
feat(CategoryTheory): pseudofunctors to Cat
050a27a
@joelriou
more lemmas
4ca7538
@joelriou
fix
fdfad5b
@joelriou
feat(CategoryTheory): descent of morphisms for a pseudofunctor
af25fe7
@joelriou
typo
600c3f7
@joelriou
Merge remote-tracking branch 'origin' into pseudofunctor-mapcomp-prim…
a11351e 
…e-cat
@joelriou
Merge remote-tracking branch 'upstream/master' into pseudofunctor-map…
da748f4 
…comp-prime-cat
@joelriou
used/fixed to_app
006d77d
@joelriou
fixed tests
29f1496
@joelriou
fixed imports
c97b420
@joelriou @callesonne
Update Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean
46c29d4 
Co-authored-by: Calle Sönne <calle.sonne@gmail.com>
@joelriou
Merge remote-tracking branch 'origin/master' into pseudofunctor-mapco…
44a44bd 
…mp-prime-cat
@joelriou
better names
652be11
@joelriou
removed set_option
0d6d91b
@joelriou
fix
315a899
@joelriou
fix
380e65e
@joelriou
fix
e056e9a
@joelriou
Merge remote-tracking branch 'origin/master' into pseudofunctor-mapco…
a030ca5 
…mp-prime-cat
@joelriou
Merge remote-tracking branch 'origin/master' into pseudofunctor-mapco…
fdfaa29 
…mp-prime-cat
@joelriou
Merge remote-tracking branch 'origin' into jriou-descent-2
4cc9258
@joelriou joelriou mentioned this pull request Oct 3, 2025
Closed
2 tasks
@github-actions github-actions bot added the t-category-theory Category theory label Oct 3, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 3, 2025 •
edited
Loading

PR summary aa78411076

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Sites.Descent.IsPrestack (new file) 853

Declarations diff

+ IsPrestack
+ mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom
+ map_eq_pullHom
+ overMapCompPresheafHomIso
+ presheafHom
+ pullHom
+ pullHom_id
+ pullHom_pullHom
+ sheafHom

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@joelriou joelriou added the WIP Work in progress label Oct 3, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 12, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 12, 2025

This PR/issue depends on:

@joelriou joelriou removed the WIP Work in progress label Oct 12, 2025
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 20, 2025
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 25, 2025
kim-em
kim-em reviewed Oct 28, 2025
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 28, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 28, 2025

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 28, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 29, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 29, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@joelriou
feat(CategoryTheory): prestacks (#30177)
a8951e2 
Let `C` be a category and `F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat`. Given `S : C`, and objects `M` and `N` in `F.obj (.mk (op S))`, we define a presheaf of types `F.presheafHom M N` on the category `Over S`: its sections on an object `T : Over S` corresponding to a morphism `p : X ⟶ S` are the type of morphisms `p^* M ⟶ p^* N`. We shall say that `F` satisfies the descent of morphisms for a Grothendieck topology `J` (i.e. `F` is a prestack) if these presheaves are all sheaves.

Co-authored-by: Christian Merten [christian@merten.dev](mailto:christian@merten.dev)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): prestacks [Merged by Bors] - feat(CategoryTheory): prestacks Oct 29, 2025
@mathlib-bors mathlib-bors bot closed this Oct 29, 2025
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@joelriou @BeibeiX0
feat(CategoryTheory): prestacks (leanprover-community#30177)
1913c5f 
Let `C` be a category and `F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat`. Given `S : C`, and objects `M` and `N` in `F.obj (.mk (op S))`, we define a presheaf of types `F.presheafHom M N` on the category `Over S`: its sections on an object `T : Over S` corresponding to a morphism `p : X ⟶ S` are the type of morphisms `p^* M ⟶ p^* N`. We shall say that `F` satisfies the descent of morphisms for a Grothendieck topology `J` (i.e. `F` is a prestack) if these presheaves are all sheaves.

Co-authored-by: Christian Merten [christian@merten.dev](mailto:christian@merten.dev)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@robin-carlier robin-carlier robin-carlier left review comments

Assignees

@robin-carlier robin-carlier

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @mathlib4-dependent-issues-bot @kim-em @robin-carlier