[Merged by Bors] - feat(Algebra/Category): symmetric monoidal structure on SemimoduleCat#30638
[Merged by Bors] - feat(Algebra/Category): symmetric monoidal structure on SemimoduleCat#30638alreadydone wants to merge 4 commits intoleanprover-community:masterfrom
SemimoduleCat#30638Conversation
PR summary eaf3ffb2d4
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic | 1008 | 1010 | +2 (+0.20%) |
| Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric | 1022 | 1023 | +1 (+0.10%) |
Import changes for all files
| Files | Import difference |
|---|---|
21 filesMathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid |
1 |
3 filesMathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.RingTheory.Flat.CategoryTheory |
2 |
Declarations diff
+ MonoidalCategory.instMonoidalCategoryStruct
+ associator_hom_apply
+ associator_inv_apply
+ braiding_hom_apply
+ braiding_inv_apply
+ hom_hom_associator
+ hom_hom_leftUnitor
+ hom_hom_rightUnitor
+ hom_inv_associator
+ hom_inv_leftUnitor
+ hom_inv_rightUnitor
+ hom_tensorHom
+ hom_whiskerLeft
+ hom_whiskerRight
+ instance : BraidedCategory (ModuleCat.{u} R)
+ instance : CommSemiring ((𝟙_ (SemimoduleCat.{u} R) : SemimoduleCat.{u} R) : Type u)
+ instance : equivalenceSemimoduleCat (R := R).functor.Braided
+ leftUnitor_hom_apply
+ leftUnitor_inv_apply
+ rightUnitor_hom_apply
+ rightUnitor_inv_apply
+ tensorHom_tmul
+ tensorLift
+ tensorLift_tmul
+ tensor_ext
+ tensor_ext₃
+ tensor_ext₃'
+ tensorμ_apply
+ tensorμ_eq_tensorTensorTensorComm
+ whiskerLeft_apply
+ whiskerRight_apply
+-+ symmetricCategory
-++ monoidalCategory
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
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).
a910e88 to
a7102d9
Compare
|
Have you considered generalizing |
|
This approach was pursued in #30636 but defeq issues with the forgetful functor to AddCommGrp is hard to fix. |
|
Aha, that makes a lot of sense. Could you please mention that in the implementation notes? Besides that, this PR is doing quite a lot. It adds a large new file. It adds new material in other files. And it generalizes existing material to the new setting. |
SemimoduleCat, category of modules over semiringSemimoduleCat
67b46b3 to
71be3e7
Compare
|
This PR/issue depends on: |
…t` (#30638) + Construct the symmetric monoidal structure on SemimoduleCat, and transport it to the same structure on ModuleCat (in a way preserving pre-existing defeqs) using the equivalence `ModuleCat.equivalenceSemimoduleCat` between the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.
|
Pull request successfully merged into master. Build succeeded: |
SemimoduleCatSemimoduleCat
…t` (leanprover-community#30638) + Construct the symmetric monoidal structure on SemimoduleCat, and transport it to the same structure on ModuleCat (in a way preserving pre-existing defeqs) using the equivalence `ModuleCat.equivalenceSemimoduleCat` between the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.
ModuleCat.equivalenceSemimoduleCatbetween the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.SemimoduleCat, category of modules over semiring #31023