[Merged by Bors] - refactor: weaken HasPullbacks to HasPullback in Over.Pullback by Jlh18 · Pull Request #29795 · leanprover-community/mathlib4

Jlh18 · 2025-09-19T04:00:19Z

Add an abbreviation HasPullbackAlong f to mean that all maps into the codomain of f have pullbacks along f. As discussed in zulip #mathlib4 > Hom.HasPullback

The HasPullbacks instance on a category C for defining the pullback functor along a map f : X -> Y between their over categories can be weakened to just a HasPullbackAlong condition on f.

Dually, for HasPushout and undercategories.

github-actions · 2025-09-19T04:01:23Z

PR summary 1f467e3c77

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Comma.Over.Pullback	496	498	+2 (+0.40%)

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Comma.Over.Pullback`	2

Declarations diff

+ HasPullbacksAlong
+ HasPushoutsAlong

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

chrisflav

Thanks for this PR! I think this is a good change, but we should check how this affects performance.

chrisflav · 2025-09-19T15:31:32Z

Mathlib/CategoryTheory/Comma/Over/Pullback.lean

 by pulling back a morphism along `f`. -/
 @[simps! +simpRhs obj_left obj_hom map_left]
-def pullback {X Y : C} (f : X ⟶ Y) : Over Y ⥤ Over X where
+def pullback : Over Y ⥤ Over X where


In my opinion this is a regression in readability. I would repeat the f argument (and the HasPullback assumption) in the signature.
Similarly below.

(In lemmas, relying on the section variables is fine.)

chrisflav · 2025-09-19T15:37:09Z

Mathlib/CategoryTheory/Comma/Over/Pullback.lean


 section HasBinaryProducts
-variable [HasBinaryProducts C]
+variable [HasBinaryProducts C] (X)


This variable implicitness change is unrelated to the rest of this PR if I understand correctly. I would suggest to do this in a separate PR, because this change probably needs some further discussion. For example, if we change explicitness here, we should probably also change Over.post.

This was just because X was explicit before, then became implicit due to my variable declaration at the top of the file. It is removed now

chrisflav · 2025-09-19T15:38:04Z

!bench

Jlh18 · 2025-09-19T15:48:47Z

-awaiting-author

Mathlib/CategoryTheory/Comma/Over/Pullback.lean

chrisflav · 2025-09-19T15:56:27Z

Mathlib/CategoryTheory/Comma/Over/Pullback.lean

+section
+
+variable [HasPullbacks C]
+


Instead of making a section, I would just move the [HasPullbacks C] in the signature of the statement.

leanprover-bot · 2025-09-19T16:11:54Z

Here are the benchmark results for commit 2c45ee1.
There were no significant changes against commit 4f7d34e.

github-actions · 2025-09-19T16:12:34Z

File	Instructions	%
`build`	+7.192⬝10⁹	(+0.00%)
`Mathlib.CategoryTheory.Comma.Over.Pullback`	+6.148⬝10⁹	(+18.76%)
CI run Lakeprof report

Jlh18 · 2025-09-19T16:58:03Z

-awaiting-author

Jlh18 · 2025-09-22T14:46:27Z

I am now wondering if we should make a class

protected class Hom.HasPullback {X Y : C} (f : X ⟶ Y) : Prop where
  hasPullback {W} (g : W ⟶ Y) : HasPullback g f

to make these statements a little tidier?

kckennylau · 2025-09-23T11:03:59Z

Is there a context for this PR (and I suppose this new class)?

Jlh18 · 2025-09-29T13:00:46Z

The category of manifolds also admits not all pullbacks but all pullbacks along submersions, so this seems like a useful definition for that too. One small nitpick though: shouldn't it be Hom.HasPullbacksAlong instead of Hom.HasPullbackAlong? It is all pullbacks along that morphism that you're talking about after all, not just one

I am happy to go with that convention. Changed it now

peabrainiac

Added a comment on one more thing I previously missed. Other than that this looks good to me though, thanks!

peabrainiac · 2025-09-29T13:35:31Z

Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

+/-- `HasPullbacksAlong f` represents a choice of pullback
+for each morphism into the codomain of `f : X ⟶ Z`. -/


Suggested change

/-- `HasPullbacksAlong f` represents a choice of pullback

for each morphism into the codomain of `f : X ⟶ Z`. -/

/-- `HasPullbacksAlong f` states that all pullbacks of morphisms into `Y` along `f : X ⟶ Y` exist. -/

This is just a proposition, it doesn't actually carry any choices of pullbacks as data. Same thing for pushouts.

I was following the style of doc-strings for HasPullback and HasPullbacks. Should I change them too?

Oh right, those are outdated. They should definitely be updated at some point, but so should the docstrings for HasEqualizer, HasEqualizers, HasWideEqualizer, HasWideEqualizers, HasCoequalizer etc... maybe that is enough to warrant a separate PR. Let's just change the docstrings introduced in this PR for now.

Got it - fixed now. Thanks a lot for the review!

…30145) Update the docstrings of `HasPullbacks`, `HasEqualizers` etc. to reflect that those declarations are propositions and no longer carry any choices of limits as data. This came up in #29795. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib4-merge-conflict-bot · 2025-10-03T19:14:04Z

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

…eanprover-community#30145) Update the docstrings of `HasPullbacks`, `HasEqualizers` etc. to reflect that those declarations are propositions and no longer carry any choices of limits as data. This came up in leanprover-community#29795. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou · 2025-10-10T06:53:12Z

Thanks!

bors merge

Add an abbreviation `HasPullbackAlong f` to mean that all maps into the codomain of `f` have pullbacks along `f`. As discussed in zulip [#mathlib4 > Hom.HasPullback](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Hom.2EHasPullback/with/541055666) The `HasPullbacks` instance on a category `C` for defining the pullback functor along a map `f : X -> Y` between their over categories can be weakened to just a `HasPullbackAlong` condition on `f`. Dually, for `HasPushout` and undercategories. Co-authored-by: jlh18 <josephhua73@yahoo.com>

mathlib-bors · 2025-10-10T07:15:53Z

Pull request successfully merged into master.

Build succeeded:

…ts (#29812) The `HasPullbacks` instance on a category `C` for defining the `baseChange` / pullback functor along a map `f : X -> Y` between their over categories can be weakened to just a `HasPullback` condition on `f`. - [ ] depends on: #29795 Co-authored-by: jlh18 <josephhua73@yahoo.com>

…eanprover-community#30145) Update the docstrings of `HasPullbacks`, `HasEqualizers` etc. to reflect that those declarations are propositions and no longer carry any choices of limits as data. This came up in leanprover-community#29795. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…over-community#29795) Add an abbreviation `HasPullbackAlong f` to mean that all maps into the codomain of `f` have pullbacks along `f`. As discussed in zulip [#mathlib4 > Hom.HasPullback](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Hom.2EHasPullback/with/541055666) The `HasPullbacks` instance on a category `C` for defining the pullback functor along a map `f : X -> Y` between their over categories can be weakened to just a `HasPullbackAlong` condition on `f`. Dually, for `HasPushout` and undercategories. Co-authored-by: jlh18 <josephhua73@yahoo.com>

…Adjuction (#29810) This PR replaces the global assumption of `HasPullback T` with the weaker assumption that pullbacks exist along the morphism only. For the sake of readability I also moved the variable `(f : X -> Y)` into the statement of each theorem. As instructed in #29795 (comment) - [ ] depends on: #29795 - [ ] depends on: #29812 Co-authored-by: jlh18 <josephhua73@yahoo.com>

…Adjuction (leanprover-community#29810) This PR replaces the global assumption of `HasPullback T` with the weaker assumption that pullbacks exist along the morphism only. For the sake of readability I also moved the variable `(f : X -> Y)` into the statement of each theorem. As instructed in leanprover-community#29795 (comment) - [ ] depends on: leanprover-community#29795 - [ ] depends on: leanprover-community#29812 Co-authored-by: jlh18 <josephhua73@yahoo.com>

…eanprover-community#30145) Update the docstrings of `HasPullbacks`, `HasEqualizers` etc. to reflect that those declarations are propositions and no longer carry any choices of limits as data. This came up in leanprover-community#29795. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…over-community#29795) Add an abbreviation `HasPullbackAlong f` to mean that all maps into the codomain of `f` have pullbacks along `f`. As discussed in zulip [#mathlib4 > Hom.HasPullback](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Hom.2EHasPullback/with/541055666) The `HasPullbacks` instance on a category `C` for defining the pullback functor along a map `f : X -> Y` between their over categories can be weakened to just a `HasPullbackAlong` condition on `f`. Dually, for `HasPushout` and undercategories. Co-authored-by: jlh18 <josephhua73@yahoo.com>

…ts (leanprover-community#29812) The `HasPullbacks` instance on a category `C` for defining the `baseChange` / pullback functor along a map `f : X -> Y` between their over categories can be weakened to just a `HasPullback` condition on `f`. - [ ] depends on: leanprover-community#29795 Co-authored-by: jlh18 <josephhua73@yahoo.com>

…Adjuction (leanprover-community#29810) This PR replaces the global assumption of `HasPullback T` with the weaker assumption that pullbacks exist along the morphism only. For the sake of readability I also moved the variable `(f : X -> Y)` into the statement of each theorem. As instructed in leanprover-community#29795 (comment) - [ ] depends on: leanprover-community#29795 - [ ] depends on: leanprover-community#29812 Co-authored-by: jlh18 <josephhua73@yahoo.com>

refactor: weaken HasPullbacks to HasPullback in Over.Pullback

1122e16

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory labels Sep 19, 2025

Jlh18 added 2 commits September 19, 2025 00:41

fix: replace deleted docstring

252c90f

fix: unused import

2c45ee1

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

chrisflav reviewed Sep 19, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2025

fix: variable declarations

d3bb8c6

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2025

chrisflav reviewed Sep 19, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2025

style: remove section

54f0654

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2025

Jlh18 marked this pull request as draft September 19, 2025 20:27

Jlh18 marked this pull request as ready for review September 20, 2025 02:13

Jlh18 marked this pull request as draft September 22, 2025 14:44

Jlh18 marked this pull request as ready for review September 22, 2025 15:28

peabrainiac reviewed Sep 29, 2025

View reviewed changes

doc: clarify HasPullbacksAlong is propositional

8b64b61

leanprover-community-bot-assistant assigned kim-em Sep 30, 2025

peabrainiac mentioned this pull request Oct 3, 2025

[Merged by Bors] - doc(CategoryTheory/Limits): update docstrings of HasPullbacks etc #30145

Closed

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

merge master

61f2c34

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

Jlh18 added 2 commits October 7, 2025 13:27

Merge branch 'master' into OverPullback

50bc3f6

fix: breakage due to no HasPullbacksAlong instance

f10bb24

joelriou mentioned this pull request Oct 9, 2025

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

Open

ghost added the ready-to-merge This PR has been sent to bors. label Oct 10, 2025

mathlib-bors bot changed the title ~~refactor: weaken HasPullbacks to HasPullback in Over.Pullback~~ [Merged by Bors] - refactor: weaken HasPullbacks to HasPullback in Over.Pullback Oct 10, 2025

mathlib-bors bot closed this Oct 10, 2025

		/-- `HasPullbacksAlong f` represents a choice of pullback
		for each morphism into the codomain of `f : X ⟶ Z`. -/

	/-- `HasPullbacksAlong f` represents a choice of pullback
	for each morphism into the codomain of `f : X ⟶ Z`. -/
	/-- `HasPullbacksAlong f` states that all pullbacks of morphisms into `Y` along `f : X ⟶ Y` exist. -/

Conversation

Jlh18 commented Sep 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 1f467e3c77

Import changes for modified files

Declarations diff

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisflav commented Sep 19, 2025

Uh oh!

Jlh18 commented Sep 19, 2025

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leanprover-bot commented Sep 19, 2025

Uh oh!

github-actions bot commented Sep 19, 2025

Uh oh!

Jlh18 commented Sep 19, 2025

Uh oh!

Jlh18 commented Sep 22, 2025

Uh oh!

kckennylau commented Sep 23, 2025

Uh oh!

Jlh18 commented Sep 29, 2025

Uh oh!

peabrainiac left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peabrainiac Sep 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

joelriou commented Oct 10, 2025

Uh oh!

mathlib-bors bot commented Oct 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Jlh18 commented Sep 19, 2025 •

edited

Loading

github-actions bot commented Sep 19, 2025 •

edited

Loading

peabrainiac Sep 29, 2025 •

edited

Loading