Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 08:17 4813b73a

View on Github →

feat(category_theory/adjunction): general adjoint functor theorem (#4885) A proof of the general adjoint functor theorem. This PR also adds an API for wide equalizers (essentially copied from the equalizer API), as well as results relating adjunctions to (co)structured arrow categories and weakly initial objects. I can split this into smaller PRs if necessary?

Estimated changes

Created src/category_theory/adjunction/adjoint_functor_theorems.lean

added def category_theory.solution_set_condition

added theorem category_theory.solution_set_condition_of_is_right_adjoint

Created src/category_theory/adjunction/comma.lean

added def category_theory.adjunction_of_costructured_arrow_terminals

added def category_theory.adjunction_of_structured_arrow_initials

added def category_theory.is_right_adjoint_of_costructured_arrow_terminals

added def category_theory.is_right_adjoint_of_structured_arrow_initials

added def category_theory.left_adjoint_of_structured_arrow_initials

added def category_theory.left_adjoint_of_structured_arrow_initials_aux

added def category_theory.mk_initial_of_left_adjoint

added def category_theory.mk_terminal_of_right_adjoint

added def category_theory.right_adjoint_of_costructured_arrow_terminals

added def category_theory.right_adjoint_of_costructured_arrow_terminals_aux

Created src/category_theory/limits/constructions/weakly_initial.lean

added theorem category_theory.has_initial_of_weakly_initial_and_has_wide_equalizers

added theorem category_theory.has_weakly_initial_of_weakly_initial_set_and_has_products

Created src/category_theory/limits/shapes/wide_equalizers.lean

added def category_theory.limits.cocone.of_cotrident

added theorem category_theory.limits.cocone.of_cotrident_ι

added def category_theory.limits.cone.of_trident

added theorem category_theory.limits.cone.of_trident_π

added theorem category_theory.limits.cotrident.app_one

added theorem category_theory.limits.cotrident.coequalizer_ext

added theorem category_theory.limits.cotrident.condition

added def category_theory.limits.cotrident.ext

added def category_theory.limits.cotrident.is_colimit.desc'

added theorem category_theory.limits.cotrident.is_colimit.hom_ext

added def category_theory.limits.cotrident.is_colimit.hom_iso

added theorem category_theory.limits.cotrident.is_colimit.hom_iso_natural

added def category_theory.limits.cotrident.is_colimit.mk'

added def category_theory.limits.cotrident.is_colimit.mk

added def category_theory.limits.cotrident.mk_hom

added def category_theory.limits.cotrident.of_cocone

added theorem category_theory.limits.cotrident.of_cocone_ι

added def category_theory.limits.cotrident.of_π

added def category_theory.limits.cotrident.π

added theorem category_theory.limits.cotrident.π_eq_app_one

added theorem category_theory.limits.cotrident.π_of_π

added def category_theory.limits.cotrident

added def category_theory.limits.diagram_iso_parallel_family

added theorem category_theory.limits.epi_of_is_colimit_parallel_family

added def category_theory.limits.has_wide_coequalizer

added def category_theory.limits.has_wide_coequalizers

added theorem category_theory.limits.has_wide_coequalizers_of_has_colimit_parallel_family

added def category_theory.limits.has_wide_equalizer

added def category_theory.limits.has_wide_equalizers

added theorem category_theory.limits.has_wide_equalizers_of_has_limit_parallel_family

added theorem category_theory.limits.mono_of_is_limit_parallel_family

added def category_theory.limits.parallel_family

added theorem category_theory.limits.parallel_family_map_left

added theorem category_theory.limits.parallel_family_obj_one

added theorem category_theory.limits.parallel_family_obj_zero

added theorem category_theory.limits.trident.app_zero

added theorem category_theory.limits.trident.condition

added theorem category_theory.limits.trident.equalizer_ext

added def category_theory.limits.trident.ext

added theorem category_theory.limits.trident.is_limit.hom_ext

added def category_theory.limits.trident.is_limit.hom_iso

added theorem category_theory.limits.trident.is_limit.hom_iso_natural

added def category_theory.limits.trident.is_limit.lift'

added def category_theory.limits.trident.is_limit.mk'

added def category_theory.limits.trident.is_limit.mk

added def category_theory.limits.trident.mk_hom

added def category_theory.limits.trident.of_cone

added theorem category_theory.limits.trident.of_cone_π

added def category_theory.limits.trident.of_ι

added def category_theory.limits.trident.ι

added theorem category_theory.limits.trident.ι_eq_app_zero

added theorem category_theory.limits.trident.ι_of_ι

added def category_theory.limits.trident

added def category_theory.limits.walking_parallel_family.hom.comp

added inductive category_theory.limits.walking_parallel_family.hom

added theorem category_theory.limits.walking_parallel_family.hom_id

added inductive category_theory.limits.walking_parallel_family

added def category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair

added theorem category_theory.limits.wide_coequalizer.condition

added def category_theory.limits.wide_coequalizer.cotrident

added theorem category_theory.limits.wide_coequalizer.cotrident_ι_app_one

added theorem category_theory.limits.wide_coequalizer.cotrident_π

added def category_theory.limits.wide_coequalizer.desc'

added def category_theory.limits.wide_coequalizer.desc

added theorem category_theory.limits.wide_coequalizer.hom_ext

added def category_theory.limits.wide_coequalizer.π

added theorem category_theory.limits.wide_coequalizer.π_desc

added def category_theory.limits.wide_coequalizer

added def category_theory.limits.wide_coequalizer_is_wide_coequalizer

added theorem category_theory.limits.wide_equalizer.condition

added theorem category_theory.limits.wide_equalizer.hom_ext

added def category_theory.limits.wide_equalizer.lift'

added def category_theory.limits.wide_equalizer.lift

added theorem category_theory.limits.wide_equalizer.lift_ι

added def category_theory.limits.wide_equalizer.trident

added theorem category_theory.limits.wide_equalizer.trident_ι

added theorem category_theory.limits.wide_equalizer.trident_π_app_zero

added def category_theory.limits.wide_equalizer.ι

added def category_theory.limits.wide_equalizer

added def category_theory.limits.wide_equalizer_is_wide_equalizer