Skip to content

feat(CategoryTheory): descent of morphisms for a pseudofunctor#24411

Closed
joelriou wants to merge 12 commits intomasterfrom
jriou-descent-2
Closed

feat(CategoryTheory): descent of morphisms for a pseudofunctor#24411
joelriou wants to merge 12 commits intomasterfrom
jriou-descent-2

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Apr 27, 2025 •
edited by alreadydone
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 a 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 if these presheaves are all sheaves (typeclass F.HasDescentOfMorphisms J).

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

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Apr 27, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 27, 2025 •
edited
Loading

PR summary 32e6452d56

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Bicategory.Functor.Strict (new file) 391
Mathlib.CategoryTheory.Bicategory.Functor.Cat (new file) 392
Mathlib.CategoryTheory.Sites.Descent.Morphisms (new file) 809

Declarations diff

+ HasDescentOfMorphisms
+ isoMapOfCommSq
+ isoMapOfCommSq_eq
+ isoMapOfCommSq_horiz_id
+ isoMapOfCommSq_vert_id
+ mapComp'
+ mapComp'_comp_id
+ mapComp'_comp_id_hom_app
+ mapComp'_comp_id_inv_app
+ mapComp'_def
+ mapComp'_eq_mapComp
+ mapComp'_hom_app_comp_mapComp'_hom_app_map_obj
+ mapComp'_hom_app_comp_map_map_mapComp'_hom_app
+ mapComp'_hom_comp_mapComp'_hom_whiskerRight
+ mapComp'_hom_comp_whiskerLeft_mapComp'_hom
+ mapComp'_hom_naturality
+ mapComp'_id_comp
+ mapComp'_id_comp_hom_app
+ mapComp'_id_comp_inv_app
+ mapComp'_inv_app_comp_mapComp'_hom_app
+ mapComp'_inv_app_comp_mapComp'_hom_app'
+ mapComp'_inv_app_map_obj_comp_mapComp'_inv_app
+ mapComp'_inv_comp_mapComp'_hom
+ mapComp'_inv_naturality
+ mapComp'_inv_whiskerRight_comp_mapComp'_inv
+ mapComp'_naturality_1
+ mapComp'_naturality_2
+ mapComp'₀₁₃_hom_app
+ mapComp'₀₁₃_inv_app
+ mapId'
+ mapId'_def
+ mapId'_eq_mapId
+ mapId'_hom_naturality
+ mapId'_inv_naturality
+ map_map_mapComp'_inv_app_comp_mapComp'_inv_app
+ overMapCompPresheafHomIso
+ presheafHom
+ sheafHom
+ whiskerLeft_mapComp'_inv_comp_mapComp'_inv

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.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
762 1 erw

Current commit 4cc9258745
Reference commit 32e6452d56

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 mentioned this pull request Apr 27, 2025
Closed
2 tasks
@joelriou joelriou mentioned this pull request Apr 28, 2025
Open
8 tasks
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 30, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Apr 30, 2025 •
edited
Loading

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 5, 2025

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 3, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 3, 2025

This PR has been migrated to a fork-based workflow: #30177

@joelriou joelriou mentioned this pull request Oct 3, 2025
Closed
2 tasks
@joelriou joelriou closed this Oct 3, 2025
@YaelDillies YaelDillies deleted the jriou-descent-2 branch November 6, 2025 09:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) migrated-to-fork t-category-theory Category theory WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @mathlib4-merge-conflict-bot