Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-28 21:31 3b195032

View on Github →

refactor(category_theory/single_obj): migrate to bundled morphisms (#1330)

Define equivalence between { f // is_monoid_hom f } and monoid_hom
Migrate single_obj to bundled homomorphisms Fix a bug in to_End: the old implementation used a wrong monoid structure on End.
Fix Mon.hom_equiv_monoid_hom as suggested by @jcommelin

Estimated changes

Modified src/algebra/Mon/basic.lean

added def Mon.hom_equiv_monoid_hom

Modified src/category_theory/single_obj.lean

modified def category_theory.single_obj.map_hom

modified theorem category_theory.single_obj.map_hom_comp

deleted def category_theory.single_obj.map_hom_equiv

modified theorem category_theory.single_obj.map_hom_id

modified def category_theory.single_obj.to_End

modified theorem category_theory.single_obj.to_End_def

deleted def category_theory.single_obj.to_End_equiv

added theorem monoid_hom.comp_to_functor

added theorem monoid_hom.id_to_functor

added def monoid_hom.to_functor

added def units.to_Aut

added theorem units.to_Aut_hom

added theorem units.to_Aut_inv