Commit 2021-04-02 21:56 36e5ff4c

View on Github →

feat(category_theory/with_term): formally adjoin terminal / initial objects. (#6966) Adds the construction which formally adjoins a terminal resp. initial object to a category.

Estimated changes

Modified src/category_theory/limits/shapes/terminal.lean

added def category_theory.limits.is_initial.of_iso

added def category_theory.limits.is_terminal.of_iso

Created src/category_theory/with_terminal.lean

added def category_theory.with_initial.comp

added def category_theory.with_initial.hom

added def category_theory.with_initial.hom_to

added def category_theory.with_initial.id

added def category_theory.with_initial.incl

added def category_theory.with_initial.incl_lift

added def category_theory.with_initial.incl_lift_to_initial

added def category_theory.with_initial.lift

added def category_theory.with_initial.lift_star

added theorem category_theory.with_initial.lift_star_lift_map

added def category_theory.with_initial.lift_to_initial

added def category_theory.with_initial.lift_to_initial_unique

added def category_theory.with_initial.lift_unique

added def category_theory.with_initial.map

added def category_theory.with_initial.star_initial

added inductive category_theory.with_initial

added def category_theory.with_terminal.comp

added def category_theory.with_terminal.hom

added def category_theory.with_terminal.hom_from

added def category_theory.with_terminal.id

added def category_theory.with_terminal.incl

added def category_theory.with_terminal.incl_lift

added def category_theory.with_terminal.incl_lift_to_terminal

added def category_theory.with_terminal.lift

added theorem category_theory.with_terminal.lift_map_lift_star

added def category_theory.with_terminal.lift_star

added def category_theory.with_terminal.lift_to_terminal

added def category_theory.with_terminal.lift_to_terminal_unique

added def category_theory.with_terminal.lift_unique

added def category_theory.with_terminal.map

added def category_theory.with_terminal.star_terminal

added inductive category_theory.with_terminal