feat(Algebra/Category): ConcreteCategory instances for rings
#20815
+349
−120
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
This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR adds basic support for `ConcreteCategory` to the `elementwise` attribute and elaborator: it still uses `HasForget` when a fresh instance is needed, but now will replace the `forget`-based operations with `ConcreteCategory`-based ones. So as long as there is only a `HasForget` instance, or no instance at all, in scope, `elementwise` will behave the same. But when there is a `ConcreteCategory` instance, all the `(forget C).obj X`es turn into `ToType X` and `(forget C).map f`s turn into `hom f`. In the future, when we have replaced enough `HasForget` instances with `ConcreteCategory`, we can apply the changes from the branch `redesign-ConcreteCategory` to make `elementwise` use `ConcreteCategory` when it creates fresh instances.
This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR adds a `ConcreteCategory` instance for the categories of rings: `SemiRingCat`, `RingCat`, `CommSemiRingCat` and `CommRingCat`. It also replaces the `Hom.hom` structure projection with an alias for `ConcreteCategory.hom`. The latter requires a few fixes downstream where things get mistakenly unfolded (especially involving `ModuleCat.restrictScalars`) or where `rw` doesn't see through the definitional equality `ConcreteCategory.hom (ConcreteCategory.ofHom f) = f`. Finally, a few places where the proof works around the old `forget` <-> `FunLike` mismatch, and needs updating. I have not tried to look for code that can be cleaned up now, only at what broke. Better do that when the other concrete categories are in.
Vierkantor
added
t-category-theory
PR summary b0815d4c32Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4618 | 3 | porting notes |
| 1412 | -2 | erw |
| 12 | 1 | maxHeartBeats modifications |
Current commit b0815d4c32
Reference commit 9ca037a451
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).
Vierkantor
commented
Jan 17, 2025
| @@ -787,6 +787,7 @@ theorem self_le_basicOpen_union_iff (s : Set Γ(X, U)) : | |||
|
|
|||
| end IsAffineOpen | |||
|
|
|||
| set_option maxHeartbeats 400000 in | |||
There was a problem hiding this comment.
This proof needs heavy cleanup, specifically it seems we should get rid of the second show statement, but I couldn't figure out how to get that done...
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
!bench |
|
Here are the benchmark results for commit b0815d4. Benchmark Metric Change
==================================================================================
- ~Mathlib.Algebra.Category.Grp.Biproducts instructions 136.0%
- ~Mathlib.Algebra.Category.ModuleCat.Biproducts instructions 82.5%
- ~Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf instructions 66.9%
- ~Mathlib.Algebra.Category.ModuleCat.Images instructions 85.2%
- ~Mathlib.Algebra.Category.ModuleCat.Kernels instructions 119.4%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf instructions 17.7%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal instructions 25.3%
- ~Mathlib.Algebra.Category.ModuleCat.Products instructions 127.5%
- ~Mathlib.Algebra.Category.Ring.Limits instructions 42.3%
- ~Mathlib.Algebra.Homology.ShortComplex.ModuleCat instructions 137.3%
- ~Mathlib.AlgebraicGeometry.AffineScheme instructions 15.7%
- ~Mathlib.AlgebraicGeometry.AffineSpace instructions 7.6%
- ~Mathlib.AlgebraicGeometry.Modules.Tilde instructions 17.0%
- ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions 12.2%
- ~Mathlib.CategoryTheory.ConcreteCategory.Elementwise instructions 502.3%
- ~Mathlib.CategoryTheory.Sites.LocallySurjective instructions 103.1%
- ~Mathlib.CategoryTheory.Subobject.Limits instructions 48.2%
- ~Mathlib.Geometry.Manifold.Sheaf.Smooth instructions 60.2%
- ~Mathlib.Geometry.RingedSpace.OpenImmersion instructions 13.0%
- ~Mathlib.Geometry.RingedSpace.Stalks instructions 64.3%
+ ~Mathlib.Topology.Sheaves.CommRingCat instructions -16.0%
- ~Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts instructions 10.8%
- ~Mathlib.Topology.Sheaves.Stalks instructions 30.1% |
2 files, Instructions +40.0⬝10⁹
2 files, Instructions +13.0⬝10⁹
2 files, Instructions +8.0⬝10⁹
2 files, Instructions +7.0⬝10⁹
2 files, Instructions +6.0⬝10⁹
2 files, Instructions +5.0⬝10⁹
3 files, Instructions +4.0⬝10⁹
4 files, Instructions +3.0⬝10⁹
10 files, Instructions +2.0⬝10⁹
7 files, Instructions +1.0⬝10⁹
|
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.
This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980
This PR adds a
ConcreteCategoryinstance for the categories of rings:SemiRingCat,RingCat,CommSemiRingCatandCommRingCat. It also replaces theHom.homstructure projection with an alias forConcreteCategory.hom. The latter requires a few fixes downstream where things get mistakenly unfolded (especially involvingModuleCat.restrictScalars) or whererwdoesn't see through the definitional equalityConcreteCategory.hom (ConcreteCategory.ofHom f) = f. Finally, a few places where the proof works around the oldforget<->FunLikemismatch, and needs updating.I have not tried to look for code that can be cleaned up now, only at what broke. I want to get started on cleanup when the other concrete category instances are in.