Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 20:11 289ebe58

View on Github →

chore(category_theory/monoidal/End): Adding API for monoidal functors into C ⥤ C (#10841) Needed for the shift refactor

Estimated changes

Modified src/category_theory/functor_category.lean

added theorem category_theory.map_hom_inv_app

added theorem category_theory.map_inv_hom_app

Modified src/category_theory/monoidal/End.lean

added theorem category_theory.associativity_app

added def category_theory.equiv_of_tensor_iso_unit

added theorem category_theory.left_unitality_app

added theorem category_theory.obj_zero_map_μ_app

added theorem category_theory.obj_ε_app

added theorem category_theory.obj_ε_inv_app

added theorem category_theory.obj_μ_app

added theorem category_theory.obj_μ_inv_app

added theorem category_theory.obj_μ_zero_app

added theorem category_theory.right_unitality_app

modified def category_theory.tensoring_right_monoidal

added def category_theory.unit_of_tensor_iso_unit

added theorem category_theory.ε_app_obj

added theorem category_theory.ε_hom_inv_app

added theorem category_theory.ε_inv_app_obj

added theorem category_theory.ε_inv_hom_app

added theorem category_theory.ε_inv_naturality

added theorem category_theory.ε_naturality

added theorem category_theory.μ_hom_inv_app

added theorem category_theory.μ_inv_hom_app

added theorem category_theory.μ_inv_naturality

added theorem category_theory.μ_naturality

added theorem category_theory.μ_naturalityᵣ

added theorem category_theory.μ_naturality₂

added theorem category_theory.μ_naturalityₗ

Modified src/category_theory/monoidal/functor.lean

modified theorem category_theory.monoidal_functor.map_left_unitor

modified theorem category_theory.monoidal_functor.map_right_unitor

modified theorem category_theory.monoidal_functor.map_tensor

added theorem category_theory.monoidal_functor.ε_hom_inv_id

added theorem category_theory.monoidal_functor.ε_inv_hom_id

added theorem category_theory.monoidal_functor.ε_iso_hom

added theorem category_theory.monoidal_functor.μ_hom_inv_id

added theorem category_theory.monoidal_functor.μ_inv_hom_id

added theorem category_theory.monoidal_functor.μ_iso_hom

modified def category_theory.monoidal_functor.μ_nat_iso

Modified src/category_theory/natural_isomorphism.lean

added theorem category_theory.nat_iso.inv_inv_app