Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-22 11:28 d09ef4ab

View on Github →

feat(category_theory/monoidal): transport monoidal structure along an equivalence (#4123)

Estimated changes

Modified src/category_theory/equivalence.lean

modified theorem category_theory.equivalence.functor_unit_comp

Modified src/category_theory/monoidal/category.lean

modified theorem category_theory.monoidal_category.id_tensor_comp_tensor_id

modified theorem category_theory.monoidal_category.tensor_id_comp_id_tensor

Modified src/category_theory/monoidal/functor.lean

added def category_theory.lax_monoidal_functor.id

Created src/category_theory/monoidal/transport.lean

added def category_theory.monoidal.from_transported

added def category_theory.monoidal.lax_from_transported

added def category_theory.monoidal.lax_to_transported

added def category_theory.monoidal.to_transported

added def category_theory.monoidal.transport

added def category_theory.monoidal.transported

added def category_theory.monoidal.transported_monoidal_counit_iso

added def category_theory.monoidal.transported_monoidal_unit_iso