Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-04 12:27 8cd16b97

View on Github →

feat(category_theory/sums): sums (disjoint unions) of categories (#1357)

feat(category_theory/sum): direct sums of categories
minor
tidying
Fix white space, remove old comments
rearranging, associator
add TODO comment about unitors
fix import
create /basic.lean files

Estimated changes

Created src/category_theory/hom_functor.lean

added theorem category_theory.functor.hom_obj

added theorem category_theory.functor.hom_pairing_map

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/monoidal/category.lean

Modified src/category_theory/opposites.lean

deleted theorem category_theory.functor.hom_obj

deleted theorem category_theory.functor.hom_pairing_map

Modified src/category_theory/products/associator.lean

Created src/category_theory/products/basic.lean

added def category_theory.evaluation

added theorem category_theory.evaluation_map_app

added theorem category_theory.evaluation_obj_map

added theorem category_theory.evaluation_obj_obj

added def category_theory.evaluation_uncurried

added theorem category_theory.evaluation_uncurried_map

added theorem category_theory.evaluation_uncurried_obj

added def category_theory.functor.prod

added theorem category_theory.functor.prod_map

added theorem category_theory.functor.prod_obj

added def category_theory.nat_trans.prod

added theorem category_theory.nat_trans.prod_app

added def category_theory.prod.braiding

added def category_theory.prod.fst

added theorem category_theory.prod.fst_map

added theorem category_theory.prod.fst_obj

added def category_theory.prod.inl

added theorem category_theory.prod.inl_map

added theorem category_theory.prod.inl_obj

added def category_theory.prod.inr

added theorem category_theory.prod.inr_map

added theorem category_theory.prod.inr_obj

added def category_theory.prod.snd

added theorem category_theory.prod.snd_map

added theorem category_theory.prod.snd_obj

added def category_theory.prod.swap

added theorem category_theory.prod.swap_map

added theorem category_theory.prod.swap_obj

added def category_theory.prod.symmetry

added theorem category_theory.prod_comp

added theorem category_theory.prod_comp_fst

added theorem category_theory.prod_comp_snd

added theorem category_theory.prod_id

added theorem category_theory.prod_id_fst

added theorem category_theory.prod_id_snd

Modified src/category_theory/products/bifunctor.lean

Modified src/category_theory/products/default.lean

deleted def category_theory.evaluation

deleted theorem category_theory.evaluation_map_app

deleted theorem category_theory.evaluation_obj_map

deleted theorem category_theory.evaluation_obj_obj

deleted def category_theory.evaluation_uncurried

deleted theorem category_theory.evaluation_uncurried_map

deleted theorem category_theory.evaluation_uncurried_obj

deleted def category_theory.functor.prod

deleted theorem category_theory.functor.prod_map

deleted theorem category_theory.functor.prod_obj

deleted def category_theory.nat_trans.prod

deleted theorem category_theory.nat_trans.prod_app

deleted def category_theory.prod.fst

deleted theorem category_theory.prod.fst_map

deleted theorem category_theory.prod.fst_obj

deleted def category_theory.prod.inl

deleted theorem category_theory.prod.inl_map

deleted theorem category_theory.prod.inl_obj

deleted def category_theory.prod.inr

deleted theorem category_theory.prod.inr_map

deleted theorem category_theory.prod.inr_obj

deleted def category_theory.prod.snd

deleted theorem category_theory.prod.snd_map

deleted theorem category_theory.prod.snd_obj

deleted def category_theory.prod.swap

deleted theorem category_theory.prod.swap_map

deleted theorem category_theory.prod.swap_obj

deleted def category_theory.prod.symmetry

deleted theorem category_theory.prod_comp

deleted theorem category_theory.prod_comp_fst

deleted theorem category_theory.prod_comp_snd

deleted theorem category_theory.prod_id

deleted theorem category_theory.prod_id_fst

deleted theorem category_theory.prod_id_snd

Created src/category_theory/sums/associator.lean

added def category_theory.sum.associativity

added def category_theory.sum.associator

added theorem category_theory.sum.associator_map_inl_inl

added theorem category_theory.sum.associator_map_inl_inr

added theorem category_theory.sum.associator_map_inr

added theorem category_theory.sum.associator_obj_inl_inl

added theorem category_theory.sum.associator_obj_inl_inr

added theorem category_theory.sum.associator_obj_inr

added def category_theory.sum.inverse_associator

added theorem category_theory.sum.inverse_associator_map_inl

added theorem category_theory.sum.inverse_associator_map_inr_inl

added theorem category_theory.sum.inverse_associator_map_inr_inr

added theorem category_theory.sum.inverse_associator_obj_inl

added theorem category_theory.sum.inverse_associator_obj_inr_inl

added theorem category_theory.sum.inverse_associator_obj_inr_inr

Created src/category_theory/sums/basic.lean

added def category_theory.functor.sum

added theorem category_theory.functor.sum_map_inl

added theorem category_theory.functor.sum_map_inr

added theorem category_theory.functor.sum_obj_inl

added theorem category_theory.functor.sum_obj_inr

added def category_theory.nat_trans.sum

added theorem category_theory.nat_trans.sum_app_inl

added theorem category_theory.nat_trans.sum_app_inr

added def category_theory.sum.inl_

added theorem category_theory.sum.inl_map

added theorem category_theory.sum.inl_obj

added def category_theory.sum.inr_

added theorem category_theory.sum.inr_map

added theorem category_theory.sum.inr_obj

added def category_theory.sum.swap.equivalence

added def category_theory.sum.swap.symmetry

added def category_theory.sum.swap

added theorem category_theory.sum.swap_map_inl

added theorem category_theory.sum.swap_map_inr

added theorem category_theory.sum.swap_obj_inl

added theorem category_theory.sum.swap_obj_inr

added theorem category_theory.sum_comp_inl

added theorem category_theory.sum_comp_inr

Created src/category_theory/sums/default.lean

Modified src/category_theory/yoneda.lean