Skip to content

[Merged by Bors] - chore(CategoryTheory): rename monoidal transport constructions#31022

Closed
alreadydone wants to merge 4 commits intoleanprover-community:masterfrom
alreadydone:monoidal_transport_rename_computable
Closed

[Merged by Bors] - chore(CategoryTheory): rename monoidal transport constructions#31022
alreadydone wants to merge 4 commits intoleanprover-community:masterfrom
alreadydone:monoidal_transport_rename_computable

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented Oct 28, 2025 •
edited
Loading

  • Rename symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful to SymmetricCategory.ofFaithful etc. following CategoryTheory.BraidedCategory.ofFaithful.

  • Remove some noncomputable sections and make some noncomputable defs computable.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 28, 2025 •
edited
Loading

PR summary c0ae1f3080

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ExactPairing.ofFaithful
+ ExactPairing.ofFullyFaithful
+ MonoidalLinear.ofFaithful
+ SymmetricCategory.ofFaithful
+ SymmetricCategory.ofFullyFaithful
+ tensorObj
+ tensorObj_def

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).

@alreadydone alreadydone mentioned this pull request Oct 28, 2025
Closed
1 task
@alreadydone alreadydone force-pushed the monoidal_transport_rename_computable branch from 0e0e944 to af02289 Compare October 28, 2025 18:08
jcommelin
jcommelin reviewed Oct 29, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 29, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@alreadydone
chore(CategoryTheory): rename monoidal transport constructions (#31022)
38a9a2f 
+ Rename `symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful` to `SymmetricCategory.ofFaithful` etc. following [CategoryTheory.BraidedCategory.ofFaithful](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Braided/Basic.html#CategoryTheory.BraidedCategory.ofFaithful).

+ Remove some `noncomputable section`s and make some noncomputable defs computable.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@alreadydone
chore(CategoryTheory): rename monoidal transport constructions (#31022)
98a0538 
+ Rename `symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful` to `SymmetricCategory.ofFaithful` etc. following [CategoryTheory.BraidedCategory.ofFaithful](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Braided/Basic.html#CategoryTheory.BraidedCategory.ofFaithful).

+ Remove some `noncomputable section`s and make some noncomputable defs computable.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Build failed:

alreadydone
alreadydone commented Oct 29, 2025
View reviewed changes
Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
Comment on lines +366 to +367
@[deprecated (since := "2025-10-29")] alias tensorObj := tensorObj_carrier
@[deprecated (since := "2025-10-29")] alias tensorObj_def := tensorObj_carrier
Copy link
Copy Markdown
Contributor Author

@alreadydone alreadydone Oct 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added these aliases so that these proofs in #30638 won't break and people know what to replace.

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Oct 30, 2025

bors r+
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 30, 2025

✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-bors bot pushed a commit that referenced this pull request Oct 30, 2025
@alreadydone
chore(CategoryTheory): rename monoidal transport constructions (#31022)
be26447 
+ Rename `symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful` to `SymmetricCategory.ofFaithful` etc. following [CategoryTheory.BraidedCategory.ofFaithful](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Braided/Basic.html#CategoryTheory.BraidedCategory.ofFaithful).

+ Remove some `noncomputable section`s and make some noncomputable defs computable.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 31, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(CategoryTheory): rename monoidal transport constructions [Merged by Bors] - chore(CategoryTheory): rename monoidal transport constructions Oct 31, 2025
@mathlib-bors mathlib-bors bot closed this Oct 31, 2025
@alreadydone alreadydone deleted the monoidal_transport_rename_computable branch November 6, 2025 20:03
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@alreadydone @BeibeiX0
chore(CategoryTheory): rename monoidal transport constructions (leanp…
236bbe7 
…rover-community#31022)

+ Rename `symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful` to `SymmetricCategory.ofFaithful` etc. following [CategoryTheory.BraidedCategory.ofFaithful](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monoidal/Braided/Basic.html#CategoryTheory.BraidedCategory.ofFaithful).

+ Remove some `noncomputable section`s and make some noncomputable defs computable.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@alreadydone @bryangingechen @jcommelin