[Merged by Bors] - refactor(Algebra/Category/Ring): make morphisms a structure#19757
[Merged by Bors] - refactor(Algebra/Category/Ring): make morphisms a structure#19757
Conversation
PR summary d16e6d6e6cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4888 | -25 | porting notes |
| 201 | -1 | disabled simpNF lints |
| 1485 | -13 | erw |
Current commit d16e6d6e6c
Reference commit bfdd6039bf
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).
…/mathlib4 into chrisflav-commringcat.2
Vierkantor
left a comment
There was a problem hiding this comment.
Okay, I think we're ready for review! Kim said they'd like to take a look a look at this, so I'll contact them if you're happy too :)
|
!bench |
|
Here are the benchmark results for commit 252f33a. Benchmark Metric Change
==================================================================================
+ ~Mathlib.Algebra.Category.AlgebraCat.Basic instructions -25.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf instructions -16.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf instructions -9.8%
+ ~Mathlib.Algebra.Category.Ring.Limits instructions -17.9%
+ ~Mathlib.AlgebraicGeometry.AffineScheme instructions -14.2%
+ ~Mathlib.AlgebraicGeometry.AffineSpace instructions -6.6%
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction instructions -39.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -23.3%
+ ~Mathlib.AlgebraicGeometry.Scheme instructions -12.5%
+ ~Mathlib.AlgebraicGeometry.Stalk instructions -35.8%
+ ~Mathlib.AlgebraicGeometry.ValuativeCriterion instructions -18.8%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion instructions -4.9%
- ~Mathlib.Topology.Sheaves.CommRingCat instructions 23.6% |
| { (SemiRingCat.FilteredColimits.colimitCocone | ||
| (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι with } | ||
| { app := fun X ↦ ofHom <| ((SemiRingCat.FilteredColimits.colimitCocone | ||
| (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι.app X).hom | ||
| naturality := fun _ _ f ↦ hom_ext <| | ||
| RingHom.coe_inj ((Types.TypeMax.colimitCocone | ||
| (F ⋙ forget CommSemiRingCat)).ι.naturality f) } |
There was a problem hiding this comment.
Hmm, this seems unfortunate.
There was a problem hiding this comment.
Can we provide a function for this?
There was a problem hiding this comment.
I am afraid, I don't understand. This worked before, because it abused the def-eq of morphisms in CommSemiRingCat and SemiRingCat. Do you suggest to add some general construction for (C : Type*) [Category C] [ConcreteCategory C] [HasForget_2 C SemiRingCat]?
There was a problem hiding this comment.
Yes, I guess so. I was imagining something that can take a natural transformation, unwrap it and apply hom to the morphism, and hom_ext to the naturality condition, and put it back together. But I didn't think to hard about whether there is a type signature that makes sense. :-)
| { (SemiRingCat.FilteredColimits.colimitCocone | ||
| (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι with } | ||
| { app := fun X ↦ ofHom <| ((SemiRingCat.FilteredColimits.colimitCocone | ||
| (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι.app X).hom | ||
| naturality := fun _ _ f ↦ hom_ext <| | ||
| RingHom.coe_inj ((Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality f) } |
|
Okay, I'm happy to proceed here as is. We still have a ways to go, I guess, but this is a forward step and we might as well have it in now. bors d+ |
|
✌️ chrisflav can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Then lets merge this before it starts rotting. bors merge |
Following the pattern of #19065, we introduce a `Hom` structure for morphisms in `SemiRingCat`, `CommSemiRingCat`, `RingCat` and `CommRingCat` allowing for many `simp`lified proofs and reducing the need of `erw`. Besides the additional explicitness in form of `ofHom` and `Hom.hom`, the main regression is friction with the `FunLike` instance from the general `ConcreteCategory` API, causing the need for explicit `rw`s between `f.hom x` and `(forget RingCat).map f x`. This regression can be fixed by replacing the general `ConcreteCategory.instFunLike` by a `CoeFun` (or `FunLike`) instance that is part of the `ConcreteCategory` data. Co-authored-by: Anne Baanen <anne@anne.mx> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
|
Pull request successfully merged into master. Build succeeded: |
(Everything below is written for `CommRingCat`, but also holds for the other `RingCat`s.) As a consequence of #19757, it became harder to unify `(forget ?C).obj R =?= CommRingCat.carrier R` since `?C =?= CommRingCat` would no longer be inferred. This PR adds a unification hint that helps with all but 2 cases where we need to hint `C := CommRingCat`. The current unification hint uses `CommRingCat` as the argument to `forget`, even though we would like it to be an arbitrary category `C`, which can then trigger downstream unification of `C =?= CommRingCat`. However, it seems that dependent unification hints do not work: I cannot get Lean to typecheck `C =?= CommRingCat; (instC : Category C) =?= CommRingCat.instCategory |- ...`. I tried doing this for `ModuleCat` too and it did not seem to fix any required hints. Perhaps because `ModuleCat R` depends on the `R`?
(Everything below is written for `CommRingCat`, but also holds for the other `RingCat`s.) As a consequence of #19757, it became harder to unify `(forget ?C).obj R =?= CommRingCat.carrier R` since `?C =?= CommRingCat` would no longer be inferred. This PR adds a unification hint that helps with all but 2 cases where we need to hint `C := CommRingCat`. The current unification hint uses `CommRingCat` as the argument to `forget`, even though we would like it to be an arbitrary category `C`, which can then trigger downstream unification of `C =?= CommRingCat`. However, it seems that dependent unification hints do not work: I cannot get Lean to typecheck `C =?= CommRingCat; (instC : Category C) =?= CommRingCat.instCategory |- ...`. I tried doing this for `ModuleCat` too and it did not seem to fix any required hints. Perhaps because `ModuleCat R` depends on the `R`?
…#20075) (Everything below is written for `CommRingCat`, but also holds for the other `RingCat`s.) As a consequence of #19757, it became harder to unify `(forget ?C).obj R =?= CommRingCat.carrier R` since `?C =?= CommRingCat` would no longer be inferred. This PR adds a unification hint that helps with all but 2 cases where we need to hint `C := CommRingCat`. The current unification hint uses `CommRingCat` as the argument to `forget`, even though we would like it to be an arbitrary category `C`, which can then trigger downstream unification of `C =?= CommRingCat`. However, it seems that dependent unification hints do not work: I cannot get Lean to typecheck `C =?= CommRingCat; (instC : Category C) =?= CommRingCat.instCategory |- ...`. I tried doing this for `ModuleCat` too and it did not seem to fix any required hints. Perhaps because `ModuleCat R` depends on the `R`?
Following the pattern of #19065, we introduce a
Homstructure for morphisms inSemiRingCat,CommSemiRingCat,RingCatandCommRingCatallowing for manysimplified proofs and reducing the need oferw.Besides the additional explicitness in form of
ofHomandHom.hom, the main regression is friction with theFunLikeinstance from the generalConcreteCategoryAPI, causing the need for explicitrws betweenf.hom xand(forget RingCat).map f x. This regression can be fixed by replacing the generalConcreteCategory.instFunLikeby aCoeFun(orFunLike) instance that is part of theConcreteCategorydata.Co-authored-by: Anne Baanen anne@anne.mx