feat(CategoryTheory): Basics of Locally Cartesian Closed Categories by sinhp · Pull Request #30375 · leanprover-community/mathlib4

sinhp · 2025-10-09T14:47:45Z

Supersedes #22321

This PR defines locally cartesian closed categories in terms of existence of the pushforward functors (right adjoint to the pullback functor) for all morphisms. We develop basic API and prove the following:

Existence of the pushforward functors is equivalent to cartesian closed slices.
Any locally cartesian closed category with a terminal object is cartesian closed.
The slices of a locally cartesian closed category are locally cartesian closed.

depends on: [Merged by Bors] - feat (CategoryTheory): Chosen pullbacks #31033
depends on: [Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to Over.ChosenPullback.pullback) #30373
depends on: [Merged by Bors] - feat(CategoryTheory): Exponentiable morphisms #31332

github-actions · 2025-10-09T15:22:59Z

PR summary 8b49178e5c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism` (new file)	492
`Mathlib.CategoryTheory.LocallyCartesianClosed.Sections` (new file)	498
`Mathlib.CategoryTheory.LocallyCartesianClosed.Basic` (new file)	500

Declarations diff

+ ChosenPushforwards
+ ExponentiableMorphism
+ IsExponentiable
+ LocallyCartesianClosed
+ OverMkHom
+ binaryFan
+ binaryFanIsBinaryProduct
+ binaryFan_fst
+ binaryFan_pt
+ binaryFan_snd
+ cartesianClosed
+ cartesianClosedOver
+ cartesianMonoidalCategory
+ chosenPullbacksOver
+ chosenPushforwards
+ coev
+ coev_ev
+ comp
+ coreHomEquivToOverSections
+ curryId
+ ev
+ ev_coev
+ exponentiableMorphism
+ exponentiableOverMk
+ fst'_naturality
+ homEquiv_apply_eq
+ homEquiv_symm_apply_eq
+ id
+ instance (f : I ⟶ J) : ExponentiableMorphism f
+ instance : ChosenPullbacksAlong (Over.mk f).hom := by
+ instance [CartesianMonoidalCategory C] [ChosenPullbacks C] (X : C) [Exponentiable X] :
+ isExponentiable
+ iteratedSliceEquivOverMapIso
+ iteratedSliceForwardNaturalityIso
+ mapPullbackIsoProd
+ mapPullbackIsoProd_hom
+ ofCartesianClosedOver
+ ofChosenPushforwards
+ ofExponentiable
+ overLocallyCartesianClosed
+ pullbackMapNatIsoTensorRight
+ pullbackMapNatIsoTensorRight_hom_app
+ pullback_map_left_fst
+ pullback_map_left_snd
+ pushforwardCompIso
+ pushforwardCurry
+ pushforwardIdIso
+ pushforwardUncurry
+ pushforward_curry_uncurry
+ pushforward_uncurry_curry
+ sections
+ sectionsCurry
+ sectionsMap
+ sectionsMap_comp
+ sectionsMap_id
+ sectionsObj
+ sectionsUncurry
+ sections_curry_uncurry
+ sections_uncurry_curry
+ toOverSectionsAdj
+ toUnit_comp_curryId

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:57Z

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

…c-prelim

… lccc-section

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

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

mathlib4-merge-conflict-bot · 2025-12-19T14:59:34Z

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

…lib4 into lccc-section

…basic

mathlib4-merge-conflict-bot · 2026-01-02T19:55:05Z

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

mathlib4-dependent-issues-bot · 2026-01-05T17:07:14Z

This PR/issue depends on:

~~[Merged by Bors] - feat (CategoryTheory): Chosen pullbacks #31033~~
~~[Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to Over.ChosenPullback.pullback) #30373~~
~~[Merged by Bors] - feat(CategoryTheory): Exponentiable morphisms #31332~~
By Dependent Issues (🤖). Happy coding!

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

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

sinhp force-pushed the lccc-basic branch 2 times, most recently from d898479 to a242226 Compare October 9, 2025 16:06

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-basic branch 2 times, most recently from fd440d8 to 5839f0a Compare October 9, 2025 16:35

fix

8a42aaf

sinhp force-pushed the lccc-basic branch from 5839f0a to 2f9c443 Compare October 9, 2025 16:40

sinhp mentioned this pull request Oct 10, 2025

feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories #30366

Open

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 12 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

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

sinhp force-pushed the lccc-basic branch from c74e51c to 410019d Compare October 11, 2025 20:06

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 11, 2025

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Oct 11, 2025

sinhp and others added 7 commits December 19, 2025 13:24

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

012c328

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

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

dd8caed

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

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

a968e73

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

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

efcfeaf

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

Update Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

d76f3d9

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

Update Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksA…

54323e6

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

Merge branch 'master' into lccc-over

56e94a3

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 Dec 19, 2025

sinhp added 10 commits December 19, 2025 16:06

Merge branch 'master' of https://github.com/leanprover-community/math…

9eba639

…lib4 into lccc-section

Merge branch 'master' into lccc-exp_mor

4984135

@[expose] public section

88c5190

Delete Over.lean

90bd2bb

Merge branch 'master' into lccc-exp_mor

7afed7f

fix

566969e

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

12807e1

…basic

Merge branch 'lccc-over' into lccc-basic

24333da

Merge branch 'lccc-exp_mor' into lccc-basic

9940dd1

Merge branch 'lccc-section' into lccc-basic

81176c4

github-actions 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 Dec 19, 2025

sinhp added 4 commits December 19, 2025 22:47

refactor

09f3c94

Update Basic.lean

0f75c1e

Update Basic.lean

c8f77ca

fix linter error

a1acee7

sinhp removed the WIP Work in progress label Dec 21, 2025

sinhp mentioned this pull request Dec 22, 2025

feat(CategoryTheory): Locally cartesian closed structure on presheaf categories #33191

Open

1 task

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 Jan 2, 2026

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 Jan 5, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

feat(CategoryTheory): Basics of Locally Cartesian Closed Categories#30375
sinhp wants to merge 210 commits intoleanprover-community:masterfrom
sinhp:lccc-basic

sinhp commented Oct 9, 2025 •

edited

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!

mathlib4-merge-conflict-bot commented Dec 19, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Jan 2, 2026

Uh oh!

mathlib4-dependent-issues-bot commented Jan 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

sinhp commented Oct 9, 2025 • edited 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 8b49178e5c

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

mathlib4-merge-conflict-bot commented Dec 19, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Jan 2, 2026

Uh oh!

mathlib4-dependent-issues-bot commented Jan 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

sinhp commented Oct 9, 2025 •

edited

Loading

github-actions bot commented Oct 9, 2025 •

edited

Loading