[Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) by sinhp · Pull Request #30373 · leanprover-community/mathlib4

sinhp · 2025-10-09T14:22:39Z

In LCCCs development, the sections functor is used to define the right adjoint to the pullback functor Over.ChosenPullback.pullback.

This PR defines Over.sections and proves that it is a right adjoint to the toOver (I : C) : C ⥤ Over I (this is the computable analogue of star).

This is the computable enhancement of #22319: instead of Limits.pullback this PR builds on top of Over.ChosenPullback and thus we eliminate any instance of noncomputable constructs.

depends on: [Merged by Bors] - feat (CategoryTheory): Chosen pullbacks #31033
depends on: [Merged by Bors] - feat(CategoryTheory): Computable cartesian monoidal structure on slices induced by chosen pullbacks #31433

github-actions · 2025-10-09T14:23:52Z

PR summary 959c85291a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.LocallyCartesianClosed.Sections` (new file)	499

Declarations diff

+ coreHomEquivToOverSections
+ curryRightUnitorHom
+ sections
+ sectionsCurry
+ sectionsCurry_sectionUncurry
+ sectionsUncurry
+ sectionsUncurry_sectionsCurry
+ toOverSectionsAdj
+ toUnit_comp_curryRightUnitorHom

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).

…ndex, pull-push) (Sigma=push, Reindex=pull, pull-push = cartesian product)

mathlib4-merge-conflict-bot · 2025-10-10T08:25:56Z

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

…c-prelim

… lccc-section

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

robin-carlier

Thanks!

maintainer merge

github-actions · 2026-01-02T13:30:43Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

jcommelin

Thanks 🎉

bors d+

Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

mathlib-bors · 2026-01-05T07:36:47Z

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

Co-authored-by: Johan Commelin <johan@commelin.net>

sinhp · 2026-01-05T10:33:40Z

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

bors r+

…ver.ChosenPullback.pullback`) (#30373) In LCCCs development, the `sections` functor is used to define the right adjoint to the pullback functor `Over.ChosenPullback.pullback`. This PR defines `Over.sections` and proves that it is a right adjoint to the `toOver (I : C) : C ⥤ Over I` (this is the computable analogue of `star`). This is the computable enhancement of #22319: instead of `Limits.pullback` this PR builds on top of `Over.ChosenPullback` and thus we eliminate any instance of noncomputable constructs. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

mathlib-bors · 2026-01-05T11:36:19Z

Canceled.

sinhp · 2026-01-05T14:36:28Z

bors r+

…ver.ChosenPullback.pullback`) (#30373) In LCCCs development, the `sections` functor is used to define the right adjoint to the pullback functor `Over.ChosenPullback.pullback`. This PR defines `Over.sections` and proves that it is a right adjoint to the `toOver (I : C) : C ⥤ Over I` (this is the computable analogue of `star`). This is the computable enhancement of #22319: instead of `Limits.pullback` this PR builds on top of `Over.ChosenPullback` and thus we eliminate any instance of noncomputable constructs. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

mathlib-bors · 2026-01-05T17:02:13Z

Pull request successfully merged into master.

Build succeeded:

…ver.ChosenPullback.pullback`) (leanprover-community#30373) In LCCCs development, the `sections` functor is used to define the right adjoint to the pullback functor `Over.ChosenPullback.pullback`. This PR defines `Over.sections` and proves that it is a right adjoint to the `toOver (I : C) : C ⥤ Over I` (this is the computable analogue of `star`). This is the computable enhancement of leanprover-community#22319: instead of `Limits.pullback` this PR builds on top of `Over.ChosenPullback` and thus we eliminate any instance of noncomputable constructs. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

github-actions bot added t-category-theory Category theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 9, 2025

sinhp changed the title ~~feat: Lccc section~~ feat: LCCC section Oct 9, 2025

sinhp mentioned this pull request Oct 9, 2025

feat(CategoryTheory): Basics of Locally Cartesian Closed Categories #30375

Open

3 tasks

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 Oct 9, 2025

sinhp added 2 commits October 9, 2025 18:15

the preliminaries for locally cartesian closed categories (Sigma, Rei…

e360a4a

…ndex, pull-push) (Sigma=push, Reindex=pull, pull-push = cartesian product)

The section functor as a right adjoint to the star functor

26a4061

sinhp force-pushed the lccc-section branch from faf8a71 to 26a4061 Compare October 9, 2025 16:28

fix

8a42aaf

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 10, 2025

sinhp added 6 commits October 10, 2025 16:53

Merge remote-tracking branch 'refs/remotes/sina/lccc-prelim' into lcc…

801ce89

…c-prelim

prelims for lcccs

fa5b706

fix for HasPullbacksAlong

1f9de85

parentheses and simp

75d9799

Update Mathlib.lean

6d82809

The section functor as a right adjoint to the star functor

0d83d6b

sinhp force-pushed the lccc-section branch from 8a42aaf to 0d83d6b Compare October 11, 2025 12:07

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 11, 2025

sinhp and others added 9 commits October 11, 2025 14:08

not needed assumption

012e053

rm simp

97a5a79

correcting attribution

f2618e6

Update Prelim.lean

ad1b0eb

The section functor as a right adjoint to the star functor

1031e3e

Merge branch 'lccc-section' of https://github.com/sinhp/mathlib4 into…

12bcdfe

… lccc-section

ChosenPullback

789d4d3

Update Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullback.lean

86055e3

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Update Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullback.lean

5fda83e

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

sinhp and others added 6 commits December 29, 2025 16:48

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

f3857aa

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

name change

5b6d0dd

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

53c7085

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

fix names

2604c34

better variable scoping and style

a242e4b

better docstring

c8d5ac5

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 29, 2025

robin-carlier reviewed Jan 2, 2026

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 2, 2026

jcommelin reviewed Jan 5, 2026

View reviewed changes

Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean Outdated Show resolved Hide resolved

Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean Outdated Show resolved Hide resolved

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 5, 2026

sinhp and others added 2 commits January 5, 2026 11:32

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

ad30dd6

Co-authored-by: Johan Commelin <johan@commelin.net>

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

caaaee5

Co-authored-by: Johan Commelin <johan@commelin.net>

fix

564791e

Merge branch 'master' into lccc-section

875d957

mathlib-bors bot changed the title ~~feat(CategoryTheory): LCCC sections (constructing right adjoint to Over.ChosenPullback.pullback)~~ [Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to Over.ChosenPullback.pullback) Jan 5, 2026

mathlib-bors bot closed this Jan 5, 2026

github-actions bot mentioned this pull request Jan 16, 2026

feat: MiM PR report #15355

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`)#30373

[Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`)#30373
sinhp wants to merge 176 commits intoleanprover-community:masterfrom
sinhp:lccc-section

sinhp commented Oct 9, 2025 •

edited by dagurtomas

Loading

Uh oh!

github-actions bot commented Oct 9, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Oct 10, 2025

Uh oh!

robin-carlier left a comment

Uh oh!

github-actions bot commented Jan 2, 2026

Uh oh!

jcommelin left a comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

sinhp commented Jan 5, 2026

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

sinhp commented Jan 5, 2026

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Conversation

sinhp commented Oct 9, 2025 • edited by dagurtomas Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 959c85291a

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Oct 10, 2025

Uh oh!

robin-carlier left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 2, 2026

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

sinhp commented Jan 5, 2026

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

sinhp commented Jan 5, 2026

Uh oh!

mathlib-bors bot commented Jan 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

sinhp commented Oct 9, 2025 •

edited by dagurtomas

Loading

github-actions bot commented Oct 9, 2025 •

edited

Loading