Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: make MorphismProperty.RespectsIso a typeclass #14353

Closed
wants to merge 20 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Jul 2, 2024

Most of the properties of properties of morphisms should be made typeclasses. For example, IsMultiplicative, HasTwoOutOfThreeProperty are already typeclasses (because it is convenient for the localization of categories). In this PR, MorphismProperty.RespectsIso is made a typeclass. One of the reasons to do so is that it should ease the development of the notion of "representable" morphisms of presheaves #14208. Another is that most of the reasonable properties of morphisms which we encounter satisfy this property: we should not have to remember the names of lemmas which assert this trivial property!


The main changes are in the file CategoryTheory.MorphismProperty.Basic.

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Jul 2, 2024
Copy link

github-actions bot commented Jul 2, 2024

PR summary e2c69ac0fc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AffineTargetMorphismProperty.cancel_left_of_respectsIso
+ AffineTargetMorphismProperty.cancel_right_of_respectsIso
+ arrow_iso_iff
+ arrow_mk_iso_iff
+ cancel_left_of_respectsIso
+ cancel_right_of_respectsIso
+ instance : MorphismProperty.RespectsIso @IsSeparated := by
+ instance : QuasiCompact.affineProperty.toProperty.RespectsIso := by
+ isoClosure_eq_self
+-- respectsIso

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@joelriou
Copy link
Collaborator Author

joelriou commented Jul 3, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit c154949.
The entire run failed.
Found no significant differences.

@joelriou
Copy link
Collaborator Author

joelriou commented Jul 3, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 2f36b97.
There were no significant changes against commit 73d9fbb.

@joelriou joelriou added awaiting-review and removed WIP Work in progress labels Jul 3, 2024
@erdOne
Copy link
Member

erdOne commented Jul 4, 2024

Thanks a lot!
maintainer merge

Copy link

github-actions bot commented Jul 4, 2024

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

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2024
Most of the properties of properties of morphisms should be made typeclasses. For example, `IsMultiplicative`, `HasTwoOutOfThreeProperty` are already typeclasses (because it is convenient for the localization of categories). In this PR, `MorphismProperty.RespectsIso` is made a typeclass. One of the reasons to do so is that it should ease the development of the notion of "representable" morphisms of presheaves #14208. Another is that most of the reasonable properties of morphisms which we encounter satisfy this property: we should not have to remember the names of lemmas which assert this trivial property!
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: make MorphismProperty.RespectsIso a typeclass [Merged by Bors] - chore: make MorphismProperty.RespectsIso a typeclass Jul 5, 2024
@mathlib-bors mathlib-bors bot closed this Jul 5, 2024
@mathlib-bors mathlib-bors bot deleted the morphism-property-respects-iso-typeclass branch July 5, 2024 07:08
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants