[Merged by Bors] - refactor(Algebra/Category): turn homs in AlgebraCat into a structure
#19065
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
chrisflav
added
t-category-theory
PR summary 04c436374eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 5090 | -6 | porting notes |
| 219 | -1 | disabled simpNF lints |
| 1547 | -6 | erw |
Current commit 04c436374e
Reference commit 54d12203eb
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
!bench |
|
Here are the benchmark results for commit 58ebaf4. |
|
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
|
!bench |
|
Here are the benchmark results for commit 11940cd. Benchmark Metric Change
===================================================================
- ~Mathlib.Algebra.Category.AlgebraCat.Limits instructions 24.8% |
|
|
!bench |
|
Here are the benchmark results for commit ebd530e. Benchmark Metric Change
===================================================================
- ~Mathlib.Algebra.Category.AlgebraCat.Limits instructions 24.8% |
|
mattrobball
reviewed
Nov 18, 2024
|
!bench |
|
Here are the benchmark results for commit 73bd116. Benchmark Metric Change
===================================================================
- ~Mathlib.Algebra.Category.AlgebraCat.Limits instructions 32.5% |
|
|
So apparently, using the anonymous constructor even made it worse? |
This reverts commit 73bd116.
mattrobball
reviewed
Nov 19, 2024
|
Can you update your PR description to explain the changes and reasoning for posterity? Let's also do one more run of benchmarking. |
|
!bench |
Updated the PR description. |
|
Here are the benchmark results for commit 24c84a4. Benchmark Metric Change
==================================================================
- ~Mathlib.Algebra.Category.AlgebraCat.Basic instructions 73.0% |
|
eric-wieser
reviewed
Nov 19, 2024
|
It seems like instructions have crept up again. |
This reverts commit affefe9.
I think this is mostly because we now use |
|
!bench |
|
Here are the benchmark results for commit 04c4363. Benchmark Metric Change
==================================================================
- ~Mathlib.Algebra.Category.AlgebraCat.Basic instructions 69.1% |
|
1 task
|
What is needed to get this merged? For the slowdown: When replacing every |
|
I agree that the slowdown is a worthy tradeoff. So I still stand by my desire to merge this. @mattrobball, what do you think? |
|
Since Matt gave this a thumbs up, let's get this merged. Thank you so much for this work and your nice results! bors r+ |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 25, 2024
#19065) In the current design of concrete categories in mathlib, there are two sources of `erw`s: - Def-Eq abuse of `A ⟶ B` and `A →ₐ [R] B`: The type of `A ⟶ B` is by definition `A →ₐ[R] B`, but not at reducible transparency. So it happens that one `rw` lemma transforms a term in a form, where the next `rw` expects `A →ₐ B`. By supplying explicit `show` lines (copying the output of the pretty-printer), Lean correctly re-synthesizes the type to be `A →ₐ B` and the `rw` succeeds. This def-eq abuse hence always causes issues in the case where a lemma from the non-category theoretic part of the library should be applied. An insightful example is the following proof excerpt from current master (proof of `AlgebraCat.adj`): ```lean import Mathlib.Algebra.Category.AlgebraCat.Basic open CategoryTheory AlgebraCat variable {R : Type u} [CommRing R] set_option pp.analyze true example : free.{u} R ⊣ forget (AlgebraCat.{u} R) := Adjunction.mkOfHomEquiv { homEquiv := fun _ _ => (FreeAlgebra.lift _).symm homEquiv_naturality_left_symm := by intro X Y Z f g apply FreeAlgebra.hom_ext ext x simp only [Equiv.symm_symm, Function.comp_apply, free_map] /- Eq (α := Z) (((FreeAlgebra.lift R) (f ≫ g) : Prefunctor.obj (Functor.toPrefunctor (free R)) X ⟶ Z) (FreeAlgebra.ι R x) : ↑Z) _ -/ erw [FreeAlgebra.lift_ι_apply] sorry homEquiv_naturality_right := sorry } ``` The `simp` lemma `FreeAlgebra.lift_ι_apply` expects an `AlgHom`, but as the `pp.analyze` shows, the type is synthesized as a `⟶`. With a show line before the `erw`, Lean correctly synthesizes the type as an `AlgHom` again and the `rw` succeeds. The solution is to strictly distinguish between `A ⟶ B` and `A →ₐ[R] B`: We define a new `AlgebraCat.Hom` structure with a single field `hom : A →ₐ[R] B`. The above proof is mostly solved by `ext; simp` then, except for the `ext` lemma `FreeAlgebra.hom_ext` not applying. This is because now the type is `AlgebraCat.of R (FreeAlgebra R X) →ₐ[R] _` and Lean can't see through the `AlgebraCat.of` at reducible transparency. Hence the solution is to make `AlgebraCat.of` an `abbrev`. Finally, the proof is `by ext; simp` or even `by aesop`. - `FunLike`: An intermediate design adapted the changes from the first point, but with keeping a `FunLike` and an `AlgHomClass` instance on `A ⟶ B`. This lead to many additional `coe` lemmas for composition of morphisms, where it mattered which of the three appearing terms of `AlgebraCat` where of the form `AlgebraCat.of R A`. Eric Wieser suggested to replace the `FunLike` by a `CoeFun` which is inlined, so an invocation of `f x` turns into `f.hom x`. This has then worked very smoothly. So the key points are: - Homs in concrete categories should be one-field structures to maintain a strict type distinction. - Use `CoeFun` instead of `FunLike`, since the latter is automatically inlined. - Make `.of` constructors an `abbrev` to obtain the def-eq `↑(AlgebraCat.of R A) = A` at reducible transparency. For more details, see the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories).
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
AlgebraCat into a structureAlgebraCat into a structure
Vierkantor
added a commit
that referenced
this pull request
Nov 26, 2024
This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other. Currently the PR consists mostly of me playing "type tetris" to get everything to compile again: I haven't looked for which proofs can be cleaned up as a result. This commit is not quite finished, please see the Zulip thread for more details.
Closed
1 task
Vierkantor
added a commit
that referenced
this pull request
Dec 3, 2024
This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other. Currently the PR consists mostly of me playing "type tetris" to get everything to compile again: I haven't looked for which proofs can be cleaned up as a result. This commit is not quite finished, please see the Zulip thread for more details.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 5, 2024
#19511) This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of `A ⟶ B` and `A →ₗ[R] B`. These are not equal reducibly, so tactics get confused if one is replaced by the other. There seem to be a few regressions caused by defeq abuse that we were able to get away with previously, but some subtle elaboration differences made it evident. Otherwise the cost is inserting many `.hom`s and `asHom`s. A few steps that might clean up the diff, but would be too much work to incorporate in this PR: * Make the `ext` tactic pick up `TensorProduct.ext` again. * Replace the defeq abuse between `(restrictScalars f).obj M` and `M` with explicit maps going back and forth. Overall quite a few proofs could be cleaned up at the cost of more bookkeeping. Co-authored-by: Christian Merten <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In the current design of concrete categories in mathlib, there are two sources of
erws:A ⟶ BandA →ₐ [R] B: The type ofA ⟶ Bis by definitionA →ₐ[R] B, but not at reducible transparency. So it happens that onerwlemma transforms a term in a form, where the nextrwexpectsA →ₐ B. By supplying explicitshowlines (copying the output of the pretty-printer), Lean correctly re-synthesizes the type to beA →ₐ Band therwsucceeds. This def-eq abuse hence always causes issues in the case where a lemma from the non-category theoretic part of the library should be applied. An insightful example is the following proof excerpt from current master (proof ofAlgebraCat.adj):The
simplemmaFreeAlgebra.lift_ι_applyexpects anAlgHom, but as thepp.analyzeshows, the type is synthesized as a⟶. With a show line before theerw, Lean correctly synthesizes the type as anAlgHomagain and therwsucceeds. The solution is to strictly distinguish betweenA ⟶ BandA →ₐ[R] B: We define a newAlgebraCat.Homstructure with a single fieldhom : A →ₐ[R] B. The above proof is mostly solved byext; simpthen, except for theextlemmaFreeAlgebra.hom_extnot applying. This is because now the type isAlgebraCat.of R (FreeAlgebra R X) →ₐ[R] _and Lean can't see through theAlgebraCat.ofat reducible transparency. Hence the solution is to makeAlgebraCat.ofanabbrev. Finally, the proof isby ext; simpor evenby aesop.FunLike: An intermediate design adapted the changes from the first point, but with keeping aFunLikeand anAlgHomClassinstance onA ⟶ B. This lead to many additionalcoelemmas for composition of morphisms, where it mattered which of the three appearing terms ofAlgebraCatwhere of the formAlgebraCat.of R A. Eric Wieser suggested to replace theFunLikeby aCoeFunwhich is inlined, so an invocation off xturns intof.hom x. This has then worked very smoothly.So the key points are:
CoeFuninstead ofFunLike, since the latter is automatically inlined..ofconstructors anabbrevto obtain the def-eq↑(AlgebraCat.of R A) = Aat reducible transparency.For more details, see the Zulip discussion.