Commit 2020-11-23 13:47 3c1cf603

View on Github →

feat(category_theory/sigma): disjoint union of categories (#5020)

Estimated changes

Created src/category_theory/sigma/basic.lean

added def category_theory.sigma.desc

added def category_theory.sigma.desc_map

added theorem category_theory.sigma.desc_map_mk

added def category_theory.sigma.desc_uniq

added theorem category_theory.sigma.desc_uniq_hom_app

added theorem category_theory.sigma.desc_uniq_inv_app

added def category_theory.sigma.functor.sigma

added def category_theory.sigma.incl

added def category_theory.sigma.incl_comp_map

added def category_theory.sigma.incl_desc

added theorem category_theory.sigma.incl_desc_hom_app

added theorem category_theory.sigma.incl_desc_inv_app

added theorem category_theory.sigma.incl_obj

added def category_theory.sigma.map

added def category_theory.sigma.map_comp

added def category_theory.sigma.map_id

added theorem category_theory.sigma.map_map

added theorem category_theory.sigma.map_obj

added def category_theory.sigma.nat_iso

added def category_theory.sigma.nat_trans.sigma

added def category_theory.sigma.nat_trans

added theorem category_theory.sigma.nat_trans_app

added theorem category_theory.sigma.sigma_hom.assoc

added def category_theory.sigma.sigma_hom.comp

added theorem category_theory.sigma.sigma_hom.comp_def

added theorem category_theory.sigma.sigma_hom.comp_id

added def category_theory.sigma.sigma_hom.id

added theorem category_theory.sigma.sigma_hom.id_comp

added inductive category_theory.sigma.sigma_hom