Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-09 22:27 60e4bb92

View on Github →

refactor(category_theory/endomorphism): move to a dedicated file; prove simple lemmas (#1195)

Move definitions of End and Aut to a dedicated file
Adjust some proofs, use namespace, add docstrings
functor.map and functor.map_iso define homomorphisms of End/Aut
Define functor.map_End and functor.map_Aut

Estimated changes

Modified src/category/fold.lean

Modified src/category_theory/category.lean

deleted theorem category_theory.End.mul_def

deleted theorem category_theory.End.one_def

deleted def category_theory.End

Created src/category_theory/endomorphism.lean

added def category_theory.Aut.units_End_eqv_Aut

added def category_theory.Aut

added theorem category_theory.End.mul_def

added theorem category_theory.End.one_def

added def category_theory.End

added def category_theory.functor.map_Aut

added def category_theory.functor.map_End

Modified src/category_theory/isomorphism.lean

deleted def category_theory.Aut

added theorem category_theory.functor.map_iso_trans