Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 04:52 d7e320e6

View on Github →

feat(category_theory/limits): Cone limiting iff terminal. (#10266)

Estimated changes

Created src/category_theory/limits/cone_category.lean

added def category_theory.limits.cocone.is_colimit_equiv_is_initial

added def category_theory.limits.cone.is_limit_equiv_is_terminal

added theorem category_theory.limits.is_colimit.desc_cocone_morphism_eq_is_initial_to

added def category_theory.limits.is_colimit.of_preserves_cocone_initial

added def category_theory.limits.is_colimit.of_reflects_cocone_initial

added theorem category_theory.limits.is_initial.to_eq_desc_cocone_morphism

added theorem category_theory.limits.is_limit.lift_cone_morphism_eq_is_terminal_from

added def category_theory.limits.is_limit.of_preserves_cone_terminal

added def category_theory.limits.is_limit.of_reflects_cone_terminal

added theorem category_theory.limits.is_terminal.from_eq_lift_cone_morphism

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

added theorem category_theory.limits.has_initial_of_has_initial_of_preserves_colimit

added def category_theory.limits.is_colimit_map_cocone_empty_cocone_equiv

added def category_theory.limits.is_colimit_of_has_initial_of_preserves_colimit

added def category_theory.limits.is_initial.is_initial_obj

added def category_theory.limits.is_initial.is_initial_of_obj

added def category_theory.limits.is_terminal.is_terminal_obj

added def category_theory.limits.is_terminal.is_terminal_of_obj

deleted def category_theory.limits.is_terminal_obj_of_is_terminal

deleted def category_theory.limits.is_terminal_of_is_terminal_obj

added def category_theory.limits.preserves_initial.iso

added theorem category_theory.limits.preserves_initial.iso_hom

added def category_theory.limits.preserves_initial.of_iso_comparison

added def category_theory.limits.preserves_initial_of_is_iso

added def category_theory.limits.preserves_initial_of_iso