Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 11:42 93e90432

View on Github →

style(category_theory): concrete categories as type class

Estimated changes

Modified category_theory/category.lean

added structure category_theory.concrete_category

deleted def category_theory.concrete_category

Modified category_theory/examples/rings.lean

deleted def category_theory.examples.CommRing

deleted def category_theory.examples.comm_ring_hom.comp

deleted theorem category_theory.examples.comm_ring_hom.comp_map

deleted theorem category_theory.examples.comm_ring_hom.ext

deleted def category_theory.examples.comm_ring_hom.id

deleted theorem category_theory.examples.comm_ring_hom.id_map

modified theorem category_theory.examples.comm_ring_hom.map_add

modified theorem category_theory.examples.comm_ring_hom.map_mul

modified theorem category_theory.examples.comm_ring_hom.map_one

deleted structure category_theory.examples.comm_ring_hom

added def category_theory.examples.is_comm_ring_hom

added def category_theory.examples.{u}

Modified category_theory/examples/topological_spaces.lean

modified def category_theory.examples.topological_spaces.Top

deleted theorem category_theory.examples.topological_spaces.continuous_map.ext

deleted structure category_theory.examples.topological_spaces.continuous_map

modified structure category_theory.examples.topological_spaces.open_set

Modified category_theory/functor.lean

modified theorem category_theory.functor.comp_map

modified theorem category_theory.functor.map_comp

modified theorem category_theory.functor.map_id

modified theorem category_theory.functor.mk_map

modified theorem category_theory.functor.mk_obj

Modified category_theory/types.lean

added def category_theory.forget

modified theorem category_theory.functor_to_types.map_id

modified theorem category_theory.functor_to_types.naturality

modified theorem category_theory.types_hom

added def category_theory.ulift_functor