[Merged by Bors] - feat(CategoryTheory): morphism properties that have the two-out-of-three property #12460
Conversation
…o-out-of-three-property
| simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg | ||
| #align category_theory.morphism_property.stable_under_composition.inverse_image CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage | ||
| theorem respectsIso_of_isStableUnderComposition {P : MorphismProperty C} | ||
| [P.IsStableUnderComposition] (hP : isomorphisms C ⊆ P) : |
There was a problem hiding this comment.
I noticed that a lot of these are formalized with subset rather than le. Is there a reason to this? It will require either a lot more duplication or rewrites into le when using the order API (when considering the disjunction of properties, or monotone property constructors etc.)
(out of scope of this PR)
There was a problem hiding this comment.
For MorphismProperty, I prefer ⊆ over ≤, because if h : W₁ ⊆ W₂, it can be used as h f hf, rather than h X Y f hf if it were h : W₁ ≤ W₂ (and f : X ⟶ Y).
There was a problem hiding this comment.
Hmmm good point. I'll try later if I can change up the implicitness when deriving the complete lattice instance.
joelriou
added
the
awaiting-review
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
erdOne
added
awaiting-author
|
!bench |
|
Here are the benchmark results for commit 70e66e2. |
joelriou
added
awaiting-review
|
Thanks! |
|
🚀 Pull request has been placed on the maintainer queue by erdOne. |
leanprover-community-mathlib4-bot
added
ready-to-merge
…ree property (#12460) The type class `MorphismProperty.HasTwoOutOfThreeProperty` is introduced. The structure `StableUnderComposition` is also changed into a type class `IsStableUnderComposition`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…ree property (#12460) The type class `MorphismProperty.HasTwoOutOfThreeProperty` is introduced. The structure `StableUnderComposition` is also changed into a type class `IsStableUnderComposition`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
…ree property (#12460) The type class `MorphismProperty.HasTwoOutOfThreeProperty` is introduced. The structure `StableUnderComposition` is also changed into a type class `IsStableUnderComposition`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
The type class
MorphismProperty.HasTwoOutOfThreePropertyis introduced. The structureStableUnderCompositionis also changed into a type classIsStableUnderComposition.