Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-01 18:03 d3c565d4

View on Github →

feat(category_theory/monoidal): the monoidal coherence theorem (#7324) This PR contains a proof of the monoidal coherence theorem, stated in the following way: if C is any type, then the free monoidal category over C is a preorder. This should immediately imply the statement needed in the coherence branch.

Estimated changes

Modified docs/references.bib

Modified src/category_theory/monoidal/category.lean

modified theorem category_theory.monoidal_category.triangle_assoc_comp_left_inv

modified theorem category_theory.monoidal_category.triangle_assoc_comp_right

modified theorem category_theory.monoidal_category.triangle_assoc_comp_right_inv

Created src/category_theory/monoidal/free/basic.lean

added inductive category_theory.free_monoidal_category.hom

added inductive category_theory.free_monoidal_category.hom_equiv

added theorem category_theory.free_monoidal_category.mk_comp

added theorem category_theory.free_monoidal_category.mk_id

added theorem category_theory.free_monoidal_category.mk_l_hom

added theorem category_theory.free_monoidal_category.mk_l_inv

added theorem category_theory.free_monoidal_category.mk_tensor

added theorem category_theory.free_monoidal_category.mk_α_hom

added theorem category_theory.free_monoidal_category.mk_α_inv

added theorem category_theory.free_monoidal_category.mk_ρ_hom

added theorem category_theory.free_monoidal_category.mk_ρ_inv

added def category_theory.free_monoidal_category.project

added def category_theory.free_monoidal_category.project_map

added def category_theory.free_monoidal_category.project_map_aux

added def category_theory.free_monoidal_category.project_obj

added def category_theory.free_monoidal_category.setoid_hom

added theorem category_theory.free_monoidal_category.tensor_eq_tensor

added theorem category_theory.free_monoidal_category.unit_eq_unit

added inductive category_theory.free_monoidal_category

Created src/category_theory/monoidal/free/coherence.lean

added def category_theory.free_monoidal_category.full_normalize

added def category_theory.free_monoidal_category.full_normalize_iso

added def category_theory.free_monoidal_category.inclusion

added def category_theory.free_monoidal_category.inclusion_obj

added def category_theory.free_monoidal_category.inverse_aux

added inductive category_theory.free_monoidal_category.normal_monoidal_object

added def category_theory.free_monoidal_category.normalize'

added def category_theory.free_monoidal_category.normalize

added def category_theory.free_monoidal_category.normalize_iso

added def category_theory.free_monoidal_category.normalize_iso_app

added theorem category_theory.free_monoidal_category.normalize_iso_app_tensor

added theorem category_theory.free_monoidal_category.normalize_iso_app_unitor

added def category_theory.free_monoidal_category.normalize_iso_aux

added def category_theory.free_monoidal_category.normalize_map_aux

added def category_theory.free_monoidal_category.normalize_obj

added theorem category_theory.free_monoidal_category.normalize_obj_tensor

added theorem category_theory.free_monoidal_category.normalize_obj_unitor

added def category_theory.free_monoidal_category.tensor_func

added theorem category_theory.free_monoidal_category.tensor_func_map_app

added theorem category_theory.free_monoidal_category.tensor_func_obj_map