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
  • Rename variable Co-Authored-By: Johan Commelin
  • Fix more issues reported by @rwbarton
  • Rename variable Co-Authored-By: Reid Barton
  • 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

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 CommMon.forget
modified def CommMon.of
modified def CommMon
deleted def Mon.forget
modified def Mon.of
modified def Mon