Commit 2023-10-13 13:56 7a8ef174

View on Github →

feat: MonoidalCategory (AlgebraCat R) (#7598) Some of these proofs are a little awkward as they have to fight with:

non-reducible type issues with Quiver.Hom vs AlgHom
mazes of coercions between AlgEquiv and LinearMap
defeqs not matching between module and algebra tensor product This also corrects an accidental mis-statement of Algebra.TensorProduct.assoc_tmul.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Basic.lean

added theorem AlgebraCat.forget₂_module_map

added theorem AlgebraCat.forget₂_module_obj

Created Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

added theorem AlgebraCat.instMonoidalCategory.forget₂_map_associator_hom

added theorem AlgebraCat.instMonoidalCategory.forget₂_map_associator_inv

added def AlgebraCat.toModuleCatMonoidalFunctor

Created Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean

added def AlgebraCat.toModuleCatBraidedFunctor

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.rid_eq_rid

Modified Mathlib/RingTheory/TensorProduct.lean

added theorem Algebra.TensorProduct.assoc_toLinearEquiv

added theorem Algebra.TensorProduct.comm_toLinearEquiv

added theorem Algebra.TensorProduct.congr_toLinearEquiv

added theorem Algebra.TensorProduct.lid_toLinearEquiv

added theorem Algebra.TensorProduct.rid_toLinearEquiv