[Merged by Bors] - feat (CategoryTheory): Chosen pullbacks by sinhp · Pull Request #31033 · leanprover-community/mathlib4

sinhp · 2025-10-28T21:04:53Z

We develop a computable implementation of pullbacks, by introducing a new type-class ChosenPullbacksAlong. The non-computable HasPullbacksAlong and HasPullbacks predicates yield instances of ChosenPullbacksAlong (using global choice), but interestingly in the category of types every morphism has chosen pullbacks. Also, we prove that in cartesian monoidal categories, morphisms to the terminal object and the product projections have chosen pullbacks. We prove that ChosenPullbacksAlong has good closure properties, e.g., id, isos have chosen pullbacks, and composition of morphisms with chosen pullbacks have chosen pullbacks.

github-actions · 2025-10-28T21:06:05Z

PR summary a29cbe30b7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong` (new file)	716

Declarations diff

+ ChosenPullbacks
+ ChosenPullbacksAlong
+ cartesianMonoidalCategoryFst
+ cartesianMonoidalCategorySnd
+ cartesianMonoidalCategoryToUnit
+ chosenPullbacksAlongFst
+ comp
+ condition
+ fst
+ fst'
+ fst'_left
+ hasPullbackAlong
+ hasPullbacks
+ hom_ext
+ id
+ isPullback
+ iso
+ isoInv
+ lift
+ lift_fst
+ lift_snd
+ ofHasPullbacksAlong
+ pullbackComp
+ pullbackId
+ pullbackIsoOverPullback
+ pullbackIsoOverPullback_hom_app_comp_fst
+ pullbackIsoOverPullback_hom_app_comp_snd
+ pullbackIsoOverPullback_inv_app_comp_fst
+ pullbackIsoOverPullback_inv_app_comp_snd
+ pullbackMap
+ pullbackMap_comp
+ pullbackMap_fst
+ pullbackMap_id
+ pullbackMap_snd
+ pullbackObj
+ snd
+ snd'
+ snd'_left

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

Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullback.lean

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

into lccc-chosen_pullback

Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean

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

Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean

joelriou · 2025-11-11T15:35:41Z

Thanks!

bors merge

We develop a computable implementation of pullbacks, by introducing a new type-class `ChosenPullbacksAlong`. The non-computable `HasPullbacksAlong` and `HasPullbacks` predicates yield instances of `ChosenPullbacksAlong` (using global choice), but interestingly in the category of types every morphism has chosen pullbacks. Also, we prove that in cartesian monoidal categories, morphisms to the terminal object and the product projections have chosen pullbacks. We prove that `ChosenPullbacksAlong` has good closure properties, e.g., id, isos have chosen pullbacks, and composition of morphisms with chosen pullbacks have chosen pullbacks. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-11-11T15:49:35Z

Pull request successfully merged into master.

Build succeeded:

We develop a computable implementation of pullbacks, by introducing a new type-class `ChosenPullbacksAlong`. The non-computable `HasPullbacksAlong` and `HasPullbacks` predicates yield instances of `ChosenPullbacksAlong` (using global choice), but interestingly in the category of types every morphism has chosen pullbacks. Also, we prove that in cartesian monoidal categories, morphisms to the terminal object and the product projections have chosen pullbacks. We prove that `ChosenPullbacksAlong` has good closure properties, e.g., id, isos have chosen pullbacks, and composition of morphisms with chosen pullbacks have chosen pullbacks. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

ChosenPullback

789d4d3

github-actions bot added the t-category-theory Category theory label Oct 28, 2025

sinhp mentioned this pull request Oct 28, 2025

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

Open

joelriou reviewed Oct 28, 2025

View reviewed changes