Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-19 02:38 b11f0f14

View on Github →

refactor(category_theory): refactor concrete categories (#1380)

  • trying to use bundled homs
  • bundled monoids should use bundled homs
  • fixes
  • fixes
  • refactor(*): rewrite concrete categories
  • Add module documentation
  • local instance
  • Move files around; don't touch content yet
  • Move code around, fix some compile errors
  • Add unbundled_hom.lean
  • Turn hom into an argument of (un)bundled_hom For some reason, it helps Lean find coercions from Ring category morphisms to functions.
  • Define unbundled_hom.mk_has_forget; fix compile
  • Add some documentation
  • Fix compile
  • chore(category_theory): require morphisms live in Type
  • move back to Type
  • tweaks to doc-comments
  • fixing some formatting
  • Revert most of the changes to data/mv_polynomials
  • Drop unused argument, add a comment
  • Simplify universe levels in concrete_category/basic. Still fails to compile.
  • Simplify universe levels in concrete_category/{un,}bundled_hom
  • fixes
  • Fix an import
  • Doc cleanup
  • update post #1412
  • Drop simp
  • Rename variable Co-Authored-By: Johan Commelin johan@commelin.net
  • Rename variable Co-Authored-By: Johan Commelin johan@commelin.net
  • Fix more issues reported by @rwbarton
  • Rename variable Co-Authored-By: Reid Barton rwbarton@gmail.com
  • Use subtype.eq instead of subtype.ext.2
  • Cleanup
  • Fix compile: now ring_hom.ext takes fewer explicit args
  • Fix compile
  • Run sanity_check on all files modified in this branch
  • Fix most of the issues reported
  • Except for the old ones in mv_polynomial (postponed to a separate PR) and a false positive in single_obj
  • Review ∀ vs Π
  • Remove some unnecessary parentheses
  • add comment
  • punit_instances: no need to explicitly provide constants and operations
  • Rename has_forget to has_forget₂
  • add comment, simplify comm_ring punit
  • Drop private def free_obj
  • documentation
  • fix comment
  • tweaks
  • comments
  • documentation on touched files
  • many doc-strings

Estimated changes

modified def CommRing.adj
added theorem CommRing.free_map_coe
deleted theorem CommRing.free_map_val
added theorem CommRing.free_obj_coe
deleted theorem CommRing.free_obj_α
deleted def CommRing.hom_equiv
deleted def CommRing.Int.cast
added theorem CommRing.comp_eq
deleted def CommRing.forget
added theorem CommRing.id_eq
modified def CommRing.of
deleted def CommRing.to_Ring
added def CommSemiRing.of
added def CommSemiRing
deleted def Ring.forget
modified def Ring.of
added def SemiRing.of
added def SemiRing
deleted def CommRing.limit
deleted def AddCommGroup.of
deleted def AddCommGroup
added def CommGroup.of
added def CommGroup
modified def Group.of
modified def Group
deleted def CommMon.forget
modified def CommMon.of
modified def CommMon
deleted def Mon.forget
modified def Mon.of
modified def Mon
added theorem ring_hom.coe_comp
added theorem ring_hom.coe_of
modified def ring_hom.comp
added def ring_hom.of
deleted structure category_theory.bundled
added structure category_theory.bundled
modified def Borel
modified def Meas.of
modified def Top.adj₁
modified def Top.adj₂
deleted def Top.forget
added theorem Top.id_app
deleted def TopCommRing.forget
added theorem UniformSpace.coe_comp
added theorem UniformSpace.coe_id
added theorem UniformSpace.coe_mk
deleted def UniformSpace.forget
added theorem UniformSpace.hom_ext
modified def Top.CommRing_yoneda
modified theorem uniform_continuous.comp