[Merged by Bors] - feat(CategoryTheory): the monoidal category structure on a localization by joelriou · Pull Request #20951 · leanprover-community/mathlib4

joelriou · 2025-01-22T14:59:48Z

In #12728, we shall show that if C is a monoidal category and W is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the MonoidalCategoryStruct instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728.

Co-authored-by: Dagur Asgeirsson dagurtomas@gmail.com

github-actions · 2025-01-22T15:00:40Z

PR summary 663b23bc2e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Localization.Monoidal` (new file)	426

Declarations diff

+ Functor.postcompose₂
+ IsMonoidal
+ LocalizedMonoidal
+ associator
+ associator_hom_app
+ associator_naturality
+ associator_naturality₁
+ associator_naturality₂
+ associator_naturality₃
+ id_tensorHom
+ instance (X : C) :
+ instance (Y : C) :
+ instance : (L').IsLocalization W := inferInstanceAs (L.IsLocalization W)
+ instance : Category (LocalizedMonoidal L W ε)
+ instance : Lifting₂ L' L' W W (curriedTensor C ⋙ (whiskeringRight C C
+ isInvertedBy₂
+ leftUnitor
+ leftUnitor_hom_app
+ monoidalCategoryStruct
+ rightUnitor
+ rightUnitor_hom_app
+ tensorBifunctor
+ tensorBifunctorIso
+ tensorHom_id
+ tensorHom_mem
+ tensor_comp
+ tensor_id
+ toMonoidalCategory
+ whiskerLeft_comp
+ whiskerLeft_id
+ whiskerLeft_mem
+ whiskerRight_comp
+ whiskerRight_id
+ whiskerRight_mem
+ whisker_exchange
+ ε'
+ μ
+ μ_inv_natural_left
+ μ_inv_natural_right
+ μ_natural_left
+ μ_natural_right

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

jcommelin

Thanks 🎉

bors merge

…on (#20951) In #12728, we shall show that if `C` is a monoidal category and `W` is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the `MonoidalCategoryStruct` instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

mathlib-bors · 2025-01-31T16:21:16Z

Build failed (retrying...):

Build

…gory-struct

mathlib-bors · 2025-01-31T16:51:15Z

Canceled.

joelriou · 2025-01-31T17:22:28Z

Retrying...

bors merge

…on (#20951) In #12728, we shall show that if `C` is a monoidal category and `W` is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the `MonoidalCategoryStruct` instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

mathlib-bors · 2025-01-31T18:03:23Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

…on (#20951) In #12728, we shall show that if `C` is a monoidal category and `W` is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal. In this PR, we only define the `MonoidalCategoryStruct` instance and check the easy compatibilities. The pentagon and the triangle identities will be done in the separate PR #12728. Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

feat(CategoryTheory): the monoidal category structure on a localization

1f1f059

joelriou added the t-category-theory Category theory label Jan 22, 2025

joelriou mentioned this pull request Jan 22, 2025

[Merged by Bors] - feat(CategoryTheory): the localized category is monoidal #12728

Closed

6 tasks

joelriou added 2 commits January 22, 2025 16:00

fix

50ece0e

fixing imports

c410b6a

jcommelin reviewed Jan 31, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 31, 2025

Merge remote-tracking branch 'origin' into localization-monoidal-cate…

663b23b

…gory-struct

mathlib-bors bot changed the title ~~feat(CategoryTheory): the monoidal category structure on a localization~~ [Merged by Bors] - feat(CategoryTheory): the monoidal category structure on a localization Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the localization-monoidal-category-struct branch January 31, 2025 18:03

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): the monoidal category structure on a localization#20951

[Merged by Bors] - feat(CategoryTheory): the monoidal category structure on a localization#20951
joelriou wants to merge 4 commits intomasterfrom
localization-monoidal-category-struct

joelriou commented Jan 22, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 22, 2025 •

edited

Loading

Declarations diff

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

joelriou commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

joelriou commented Jan 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 663b23bc2e

Import changes for modified files

Declarations diff

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

joelriou commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

joelriou commented Jan 22, 2025 •

edited

Loading

github-actions bot commented Jan 22, 2025 •

edited

Loading