Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-03 12:33 36dd78ee

View on Github →

feat(category_theory): full and faithful functors, switching products also the evaluation functor, and replace the ↝ arrow with ⥤, by request

Estimated changes

Modified category_theory/category.lean

Created category_theory/embedding.lean

added theorem category_theory.image_preimage

added def category_theory.preimage

added def category_theory.preimage_iso

added theorem category_theory.preimage_iso_coe

added theorem category_theory.preimage_iso_symm_coe

Modified category_theory/functor.lean

modified def category_theory.functor.comp

modified theorem category_theory.functor.comp_map

modified theorem category_theory.functor.comp_obj

modified def category_theory.functor.map

modified theorem category_theory.functor.map_comp

modified theorem category_theory.functor.map_id

modified theorem category_theory.functor.obj_eq_coe

Modified category_theory/functor_category.lean

modified theorem category_theory.functor.category.comp_app

modified theorem category_theory.functor.category.id_app

modified theorem category_theory.functor.category.nat_trans.app_naturality

modified theorem category_theory.functor.category.nat_trans.naturality_app

Modified category_theory/isomorphism.lean

modified theorem category_theory.functor.eq_to_iso

modified def category_theory.functor.on_iso

modified theorem category_theory.functor.on_iso_hom

modified theorem category_theory.functor.on_iso_inv

Modified category_theory/natural_transformation.lean

modified theorem category_theory.nat_trans.app_eq_coe

modified theorem category_theory.nat_trans.exchange

modified def category_theory.nat_trans.hcomp

modified theorem category_theory.nat_trans.hcomp_app

modified theorem category_theory.nat_trans.id_app

modified theorem category_theory.nat_trans.mk_app

modified theorem category_theory.nat_trans.naturality

modified structure category_theory.nat_trans

Modified category_theory/opposites.lean

modified theorem category_theory.functor.opposite_map

modified theorem category_theory.functor.opposite_obj

Modified category_theory/products.lean

added def category_theory.evaluation

modified def category_theory.functor.prod

modified theorem category_theory.functor.prod_map

modified theorem category_theory.functor.prod_obj

modified def category_theory.nat_trans.prod

modified theorem category_theory.nat_trans.prod_app

modified def category_theory.prod.fst

modified def category_theory.prod.inl

modified def category_theory.prod.inr

modified def category_theory.prod.snd

added def category_theory.prod.swap

added def category_theory.prod.symmetry

Modified category_theory/types.lean

Modified docs/theories/category_theory.md