[Merged by Bors] - feat(CategoryTheory): calculus of fractions#8041
[Merged by Bors] - feat(CategoryTheory): calculus of fractions#8041
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| have := hL _ φ.hs | ||
| L.map φ.f ≫ inv (L.map φ.s) | ||
|
|
||
| @[reassoc (attr := simp, nolint unusedHavesSuffices)] |
There was a problem hiding this comment.
This nolint points at a bug. Is there already an issue for that?
There was a problem hiding this comment.
Using letI instead of have fixed the problem...
|
Thanks 🎉 If CI passes, please remove the label bors d+ |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
| ext : ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X) (_ : W s) | ||
| (_ : s ≫ f₁ = s ≫ f₂), ∃ (Y' : C) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t |
There was a problem hiding this comment.
Why not
| ext : ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X) (_ : W s) | |
| (_ : s ≫ f₁ = s ≫ f₂), ∃ (Y' : C) (t : Y ⟶ Y') (_ : W t), f₁ ≫ t = f₂ ≫ t | |
| ext : ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X), | |
| W s → s ≫ f₁ = s ≫ f₂ → ∃ (Y' : C) (t : Y ⟶ Y'), W t ∧ f₁ ≫ t = f₂ ≫ t |
|
|
||
| namespace MorphismProperty | ||
|
|
||
| variable {C D : Type _} [Category C] [Category D] |
There was a problem hiding this comment.
I think Type* is preferred now
This PR introduces notions of left and right fractions for a morphism property in a category. The typeclasses `MorphismProperty.HasLeftCalculusOfFractions` and `MorphismProperty.HasRightCalculusOfFractions` are also introduced.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
This PR introduces notions of left and right fractions for a morphism property in a category. The typeclasses `MorphismProperty.HasLeftCalculusOfFractions` and `MorphismProperty.HasRightCalculusOfFractions` are also introduced.
This PR introduces notions of left and right fractions for a morphism property in a category. The typeclasses `MorphismProperty.HasLeftCalculusOfFractions` and `MorphismProperty.HasRightCalculusOfFractions` are also introduced.
3 participants
This PR introduces notions of left and right fractions for a morphism property in a category. The typeclasses
MorphismProperty.HasLeftCalculusOfFractionsandMorphismProperty.HasRightCalculusOfFractionsare also introduced.