Commit 2025-10-30 23:57 be264471

View on Github →

chore(CategoryTheory): rename monoidal transport constructions (#31022)

Rename symmetricCategory/monoidalLinear/exactPairingOf(Fully)Faithful to SymmetricCategory.ofFaithful etc. following CategoryTheory.BraidedCategory.ofFaithful.
Remove some noncomputable sections and make some noncomputable defs computable.

Estimated changes

Modified Mathlib/Algebra/Category/AlgCat/Symmetric.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

Modified Mathlib/CategoryTheory/Action/Monoidal.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

added def CategoryTheory.SymmetricCategory.ofFaithful

deleted def CategoryTheory.symmetricCategoryOfFaithful

Modified Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

added theorem CategoryTheory.MonoidalLinear.ofFaithful

deleted theorem CategoryTheory.monoidalLinearOfFaithful

Modified Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

added def CategoryTheory.ExactPairing.ofFaithful

deleted def CategoryTheory.exactPairingOfFaithful

deleted def CategoryTheory.exactPairingOfFullyFaithful

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean

Modified Mathlib/RepresentationTheory/Rep.lean