Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-20 23:12 73933b73

View on Github →

feat(category_theory): assorted small changes from the old limits PR (#512)

Estimated changes

Modified algebra/pi_instances.lean

added def pi.is_ring_hom_pi

Modified category_theory/category.lean

added theorem category_theory.bundled_hom_coe

added theorem category_theory.category.assoc_symm

Created category_theory/discrete_category.lean

added theorem category_theory.discrete.functor_map_id

added def category_theory.discrete.lift

added def category_theory.discrete

added def category_theory.functor.of_function

added def category_theory.nat_trans.of_function

Modified category_theory/examples/rings.lean

modified def category_theory.examples.CommRing.forget_to_CommMon

added theorem category_theory.examples.CommRing_hom_coe_app

deleted def category_theory.examples.is_comm_ring_hom

Modified category_theory/examples/topological_spaces.lean

deleted def category_theory.examples.map

deleted def category_theory.examples.map_id

deleted theorem category_theory.examples.map_id_obj

deleted def category_theory.examples.map_iso

deleted def category_theory.examples.map_iso_id

added def topological_space.opens.map

added def topological_space.opens.map_id

added theorem topological_space.opens.map_id_obj

added def topological_space.opens.map_iso

added def topological_space.opens.map_iso_id

Modified category_theory/functor.lean

Modified category_theory/functor_category.lean

Modified category_theory/limits/cones.lean

Modified category_theory/limits/limits.lean

added theorem category_theory.limits.colimit.desc_extend

added theorem category_theory.limits.limit.lift_extend

Modified category_theory/opposites.lean

Modified category_theory/pempty.lean

modified def category_theory.functor.empty

Modified category_theory/punit.lean

deleted theorem category_theory.functor.of.map_app

deleted theorem category_theory.functor.of.obj_map

deleted theorem category_theory.functor.of.obj_obj

deleted def category_theory.functor.of

Created data/ulift.lean

added theorem plift.rec.constant

added theorem ulift.rec.constant

Modified tactic/ext.lean

added theorem plift.ext