Commit 2022-10-11 13:09 94fc87ee

View on Github →

feat(category_theory/groupoid/free): functoriality of the free groupoid plus some cleanup (#16907) Add lemmas witnessing functoriality of the free groupoid construction, and clean up some style/doc issues.

Estimated changes

Modified src/category_theory/groupoid/free_groupoid.lean

added def category_theory.free_groupoid

added def category_theory.free_groupoid_functor

deleted def category_theory.groupoid.free.free_groupoid

added theorem category_theory.groupoid.free.free_groupoid_functor_comp

added theorem category_theory.groupoid.free.free_groupoid_functor_id

modified theorem category_theory.groupoid.free.lift_spec

added theorem category_theory.groupoid.free.lift_unique

deleted theorem category_theory.groupoid.free.lift_unique_spec

modified def category_theory.groupoid.free.of

modified theorem category_theory.groupoid.free.of_eq

Modified src/category_theory/path_category.lean

modified theorem category_theory.paths.lift_cons

modified theorem category_theory.paths.lift_nil

deleted theorem category_theory.paths.lift_spec_unique

added theorem category_theory.paths.lift_unique

Modified src/category_theory/quotient.lean

deleted theorem category_theory.quotient.lift_spec_unique

added theorem category_theory.quotient.lift_unique

Modified src/combinatorics/quiver/basic.lean

Modified src/combinatorics/quiver/connected_component.lean

deleted theorem quiver.symmetrify.lift_spec_unique

added theorem quiver.symmetrify.lift_unique