feat(CategoryTheory/Comma): limit properties of subcategories defined by morphism properties

[chrisflav]

We show that under suitable assumptions on P the full subcategory of Over X defined by P has terminal objects and pullbacks.

---

• [x] depends on: #18088

[github-actions[bot]]

PR summary 3151e4dc69

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Limits.MorphismProperty	615

---

Declarations diff

+ CostructuredArrow.closedUnderLimitsOfShape_discrete_empty + Hom.hom_left + Hom.hom_right + Over.closedUnderLimitsOfShape_discrete_empty + Over.closedUnderLimitsOfShape_pullback + Over.homMk + Over.mk + Under.homMk + Under.mk + comma_iso_iff + costructuredArrow_iso_iff + createsLimitsOfShape_walkingCospan + forgetCreatesLimitOfClosed + forgetCreatesLimitsOfShapeOfClosed + hasLimit_of_closedUnderLimitsOfShape + hasLimitsOfShape_of_closedUnderLimitsOfShape + hasPullbacks + hasTerminal + instance [P.ContainsIdentities] (Y : P.Over ⊤ X) : + instance [P.ContainsIdentities] : HasTerminal (P.Over ⊤ X) + instance [P.ContainsIdentities] [P.RespectsIso] : + instance {X : T} : HasTerminal (Over X) := CostructuredArrow.hasTerminal + mkIdTerminal + of_isColimit_cocone + of_isLimit_cone + over_iso_iff

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18088~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[joelriou]

Thanks!

bors merge

[chrisflav]

Thanks for the reviews!

[kim-em]

Could you please take a look at all the import regressions described in https://github.com/leanprover-community/mathlib4/pull/18134#issuecomment-2432826861?

I don't think we should be merging (or even maintainer merging) PRs with large import regressions until there has been some investigation into how/if this can be avoided.

[chrisflav]

Sorry for ignoring the large-imports label, in this case I thought it was okay since the lemma over_iso_iff seemed to me at the right place there right next to arrow_iso_iff. I now moved it to a later file.

Maybe someone should either cancel whatever bors is still doing on this PR or give it another go.

[joelriou]

As far as I can remember, it had seemed to me the increase in imports was relatively moderate. Thanks for fixing it!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style