Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-09 18:34 5b7edecf

View on Github →

feat(category_theory): redesign of concrete categories Also exercising it further with def forget_to_Mon : CommRing ⥤ Mon := …

Estimated changes

Modified algebra/group.lean

Modified algebra/ring.lean

Modified category_theory/category.lean

added structure category_theory.bundled

modified structure category_theory.concrete_category

added def category_theory.mk_ob

Modified category_theory/embedding.lean

added theorem category_theory.functor.image_preimage

added def category_theory.functor.injectivity

added def category_theory.functor.preimage

deleted theorem category_theory.image_preimage

deleted def category_theory.preimage

modified theorem category_theory.preimage_iso_coe

modified theorem category_theory.preimage_iso_symm_coe

Modified category_theory/examples/measurable_space.lean

modified def category_theory.examples.Meas

Created category_theory/examples/monoids.lean

added def category_theory.examples.CommMon.forget_to_Mon

added def category_theory.examples.CommMon

added def category_theory.examples.Mon

added def category_theory.examples.is_comm_monoid_hom

Modified category_theory/examples/rings.lean

added def category_theory.examples.CommRing.forget_to_CommMon

added def category_theory.examples.CommRing

added def category_theory.examples.Ring

deleted theorem category_theory.examples.comm_ring_hom.map_add

deleted theorem category_theory.examples.comm_ring_hom.map_mul

deleted theorem category_theory.examples.comm_ring_hom.map_one

deleted def category_theory.examples.{u}

Modified category_theory/examples/topological_spaces.lean

modified def category_theory.examples.Top

Modified category_theory/functor.lean

added def category_theory.bundled.map

Modified category_theory/types.lean

modified def category_theory.forget