Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 23:58 a7960085

View on Github →

feat(category_theory): cartesian closed categories (#2894) Cartesian closed categories, from my topos project.

Estimated changes

Created src/category_theory/closed/cartesian.lean

added def category_theory.binary_product_exponentiable

added def category_theory.cartesian_closed

added def category_theory.cartesian_closed_of_equiv

added def category_theory.coev

added theorem category_theory.coev_ev

added theorem category_theory.curry_eq

added theorem category_theory.curry_eq_iff

added theorem category_theory.curry_id_eq_coev

added theorem category_theory.curry_injective

added theorem category_theory.curry_natural_left

added theorem category_theory.curry_natural_right

added theorem category_theory.curry_uncurry

added theorem category_theory.eq_curry_iff

added def category_theory.ev

added theorem category_theory.ev_coev

added def category_theory.exp.adjunction

added def category_theory.exp

added def category_theory.exp_comparison

added theorem category_theory.exp_comparison_natural_left

added theorem category_theory.exp_comparison_natural_right

added def category_theory.exp_terminal_iso_self

added def category_theory.exponentiable

added def category_theory.internal_hom

added def category_theory.internalize_hom

added def category_theory.is_cartesian_closed.curry

added def category_theory.is_cartesian_closed.uncurry

added def category_theory.mul_zero

added def category_theory.pow_zero

added def category_theory.pre

added theorem category_theory.pre_id

added theorem category_theory.pre_map

added theorem category_theory.pre_post_comm

added def category_theory.prod_coprod_distrib

added def category_theory.terminal_exponentiable

added theorem category_theory.uncurry_curry

added theorem category_theory.uncurry_eq

added theorem category_theory.uncurry_id_eq_ev

added theorem category_theory.uncurry_injective

added theorem category_theory.uncurry_natural_left

added theorem category_theory.uncurry_natural_right

added def category_theory.zero_mul

Created src/category_theory/closed/monoidal.lean

Modified src/category_theory/epi_mono.lean

added def category_theory.is_iso_of_epi_of_split_mono

added def category_theory.is_iso_of_mono_of_split_epi

Modified src/category_theory/limits/shapes/binary_products.lean

added theorem category_theory.limits.inv_prod_comparison_map_fst

added theorem category_theory.limits.inv_prod_comparison_map_snd

added theorem category_theory.limits.prod_comparison_inv_natural

Modified src/category_theory/monoidal/category.lean

added def category_theory.monoidal_category.tensor_left

added def category_theory.monoidal_category.tensor_left_tensor

added theorem category_theory.monoidal_category.tensor_left_tensor_hom_app

added theorem category_theory.monoidal_category.tensor_left_tensor_inv_app

added def category_theory.monoidal_category.tensor_right

added def category_theory.monoidal_category.tensor_right_tensor

added theorem category_theory.monoidal_category.tensor_right_tensor_hom_app

added theorem category_theory.monoidal_category.tensor_right_tensor_inv_app

Modified src/category_theory/monoidal/of_has_finite_products.lean

added theorem category_theory.monoidal_of_has_finite_coproducts.tensor_hom

added theorem category_theory.monoidal_of_has_finite_coproducts.tensor_obj

added theorem category_theory.monoidal_of_has_finite_products.tensor_hom

added theorem category_theory.monoidal_of_has_finite_products.tensor_obj