Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-30 12:43 c49ac06f

View on Github →

feat(category_theory/monoidal): monoidal categories, monoidal functors (#1002)

feat(category_theory/iso): missing lemmas
formatting
formatting
almost
oops
getting there
one more
sleep
good to go
fix names
renaming
linebreak
temporary notations
notations for associator, unitors?
more notation
names
more names
oops
renaming, and namespaces
comment
fix comment
remove unnecessary open, formatting
removing dsimps
replace with simp lemmas
fix

Estimated changes

Created src/category_theory/monoidal/category.lean

added theorem category_theory.monoidal_category.associator_inv_naturality

added def category_theory.monoidal_category.associator_nat_iso

added theorem category_theory.monoidal_category.comp_tensor_id

added theorem category_theory.monoidal_category.id_tensor_comp

added theorem category_theory.monoidal_category.id_tensor_comp_tensor_id

added theorem category_theory.monoidal_category.inv_tensor

added def category_theory.monoidal_category.left_assoc_tensor

added theorem category_theory.monoidal_category.left_assoc_tensor_map

added theorem category_theory.monoidal_category.left_assoc_tensor_obj

added theorem category_theory.monoidal_category.left_unitor_inv_naturality

added def category_theory.monoidal_category.left_unitor_nat_iso

added theorem category_theory.monoidal_category.left_unitor_product_aux

added theorem category_theory.monoidal_category.left_unitor_product_aux_perimeter

added theorem category_theory.monoidal_category.left_unitor_product_aux_square

added theorem category_theory.monoidal_category.left_unitor_product_aux_triangle

added theorem category_theory.monoidal_category.left_unitor_tensor

added theorem category_theory.monoidal_category.left_unitor_tensor_inv

added theorem category_theory.monoidal_category.pentagon_inv

added def category_theory.monoidal_category.right_assoc_tensor

added theorem category_theory.monoidal_category.right_assoc_tensor_map

added theorem category_theory.monoidal_category.right_assoc_tensor_obj

added theorem category_theory.monoidal_category.right_unitor_inv_naturality

added def category_theory.monoidal_category.right_unitor_nat_iso

added theorem category_theory.monoidal_category.right_unitor_product_aux

added theorem category_theory.monoidal_category.right_unitor_product_aux_perimeter

added theorem category_theory.monoidal_category.right_unitor_product_aux_square

added theorem category_theory.monoidal_category.right_unitor_product_aux_triangle

added theorem category_theory.monoidal_category.right_unitor_tensor

added theorem category_theory.monoidal_category.right_unitor_tensor_inv

added def category_theory.monoidal_category.tensor

added theorem category_theory.monoidal_category.tensor_id_comp_id_tensor

added theorem category_theory.monoidal_category.tensor_left_iff

added theorem category_theory.monoidal_category.tensor_right_iff

added def category_theory.monoidal_category.tensor_unit_left

added def category_theory.monoidal_category.tensor_unit_right

added theorem category_theory.monoidal_category.triangle_assoc_comp_left

added theorem category_theory.monoidal_category.triangle_assoc_comp_left_inv

added theorem category_theory.monoidal_category.triangle_assoc_comp_right

added theorem category_theory.monoidal_category.triangle_assoc_comp_right_inv

added def category_theory.tensor_iso

Created src/category_theory/monoidal/category_aux.lean

added def category_theory.assoc_natural

added def category_theory.assoc_obj

added def category_theory.left_unitor_natural

added def category_theory.left_unitor_obj

added def category_theory.pentagon

added def category_theory.right_unitor_natural

added def category_theory.right_unitor_obj

added def category_theory.tensor_hom_type

added def category_theory.tensor_obj_type

added def category_theory.triangle

Created src/category_theory/monoidal/functor.lean

added def category_theory.lax_monoidal_functor.comp

added theorem category_theory.lax_monoidal_functor.comp_map

added theorem category_theory.lax_monoidal_functor.comp_obj

added theorem category_theory.lax_monoidal_functor.comp_ε

added theorem category_theory.lax_monoidal_functor.comp_μ

added structure category_theory.lax_monoidal_functor

added def category_theory.monoidal_functor.comp

added def category_theory.monoidal_functor.id

added theorem category_theory.monoidal_functor.id_map

added theorem category_theory.monoidal_functor.id_obj

added theorem category_theory.monoidal_functor.id_ε

added theorem category_theory.monoidal_functor.id_μ

added def category_theory.monoidal_functor.ε_iso

added def category_theory.monoidal_functor.μ_iso

added def category_theory.monoidal_functor.μ_nat_iso

added structure category_theory.monoidal_functor