Commit 2023-10-09 18:38 bc49eb9b

feat(CategoryTheory/Monoidal/Transport): generalize to a faithful functor (#7237) I needed this to transfer the monoidal structure from ModuleCat to QuadraticModuleCat, but would also work for transferring the same structure from ModuleCat to AlgebraCat. The changes are:

• A new CategoryTheory.Monoidal.induced definition, proven from scratch with slightly uglier proofs than what transport used. The new proofs use simp rather more than targeted slice commands, mainly due to lack of patience on my part.
• CategoryTheory.Monoidal.transport now has a trivial implementation in terms of induced, as does CategoryTheory.MonoidalCategory.fullMonoidalSubcategory (though this was already fairly trivial)
• CategoryTheory.Monoidal.laxToTransported has been removed, as it's just a less useful version of CategoryTheory.Monoidal.toTransported
• CategoryTheory.Monoidal.toTransported has been golfed to oblivion, as it now falls out trivially by showing fromTransported first.