[Merged by Bors] - feat: port AlgebraicTopology.SimplicialObject #3302
Conversation
joelriou
commented
Apr 6, 2023
•
joelriou
commented
- depends on: [Merged by Bors] - feat: port AlgebraicTopology.SimplexCategory #3286
- depends on: [Merged by Bors] - chore: forward port of #18742, no simps lemmas for Category.Hom #3340
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
…o port/Order.Category.Lat
… port/Order.Category.PartOrd
…o port/Order.Category.Lat
…o port/Order.Category.Lat
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
…rt/Order.Category.LinOrd
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
… port/Order.Category.NonemptyFinLinOrd
semorrison
added
the
blocked-by-other-PR
semorrison
added
merge-conflict
semorrison
removed
the
merge-conflict
Parcly-Taxel
added
the
awaiting-review
| SimplexCategoryᵒᵖ ⥤ C | ||
| #align category_theory.simplicial_object CategoryTheory.SimplicialObject | ||
|
|
||
| @[simps!] |
There was a problem hiding this comment.
I'm a bit confused about all these simps! attributes. There was nothing similar in mathlib3 right? Are they strictly necessary, and would it perhaps be better to make SimplicialObject a reducible instead?
There was a problem hiding this comment.
Without the reducible attribute, the simps! for the Category instance (and extra ext lemmas for morphisms) were necessary. I have made SimplicialObject reducible in the last commit.
There was a problem hiding this comment.
Okay, I'll ping @jcommelin , @semorrison and @adamtopaz to see if they're happy with the change.
There was a problem hiding this comment.
I mean, I'd prefer that we don't make it reducible. It's more work to set up here, unfortunately. We have a tendency to regret making things less opaque, however...
There was a problem hiding this comment.
Ok. I have reverted back to the previous situation where SimplicialObject was not declared reducible.
There was a problem hiding this comment.
I'll let someone else take over the review of this PR, but I'm not sure that simp lemmas unfolding the definition of a type is a particularly good idea either for the same reasons. Probably a lot of the simp lemmas that become accessible after unfolding definitions should be proved on SimplicialObject directly.
There was a problem hiding this comment.
Indeed, a lemma like
theorem SimplicialObject.δ_naturality {X' X : SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) :
X.δ i ≫ f.app (op [n]) = f.app (op [n + 1]) ≫ X'.δ iis a particular case of NatTrans.naturality, and it is stated as a simp lemma that is specific to SimplicialObject.
There was a problem hiding this comment.
simps! currently produces simp lemmas unfolding the definition of Hom on all of these instances. I have a commit locally that replaces simps! with simps! id_app comp_app or similar to avoid unfolding the definition of Hom. The whole file builds without any other changes. Let me know if you think I should push this. Maybe @semorrison has an opinion on that, I'm not too familiar with CategoryTheory.
There was a problem hiding this comment.
Sorry, a bit of a tangle here. I have a PR open on mathlib proposing to adjust the simps projections for category so we don't unfold Hom. I should have got that done and forwarded port faster...
There was a problem hiding this comment.
Okay, I propose that I will quickly forward port that PR, and then merge that into this before we proceed?
This reverts commit 7219909.
ChrisHughes24
added
WIP
semorrison
added
blocked-by-other-PR
|
This PR/issue depends on: |
joelriou
added
awaiting-review
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
