Commit 2023-08-06 07:06 87d6e2ea

View on Github →

feat: composition properties of final functors (#6250)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Final.lean

deleted theorem CategoryTheory.Functor.Final.cofinal_of_colimit_comp_coyoneda_iso_pUnit

modified def CategoryTheory.Functor.Final.colimitCompCoyonedaIso

added theorem CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit

added theorem CategoryTheory.Functor.final_comp

added theorem CategoryTheory.Functor.final_comp_equivalence

added theorem CategoryTheory.Functor.final_equivalence_comp

added theorem CategoryTheory.Functor.final_iff_comp_equivalence

added theorem CategoryTheory.Functor.final_iff_comp_final_full_faithful

added theorem CategoryTheory.Functor.final_iff_equivalence_comp

added theorem CategoryTheory.Functor.final_iff_final_comp

added theorem CategoryTheory.Functor.final_iff_isIso_colimit_pre

added theorem CategoryTheory.Functor.final_natIso_iff

added theorem CategoryTheory.Functor.final_of_comp_full_faithful'

added theorem CategoryTheory.Functor.final_of_comp_full_faithful

added theorem CategoryTheory.Functor.final_of_equivalence_comp

added theorem CategoryTheory.Functor.final_of_final_comp

added theorem CategoryTheory.Functor.initial_comp

added theorem CategoryTheory.Functor.initial_comp_equivalence

added theorem CategoryTheory.Functor.initial_equivalence_comp

added theorem CategoryTheory.Functor.initial_iff_comp_equivalence

added theorem CategoryTheory.Functor.initial_iff_comp_initial_full_faithful

added theorem CategoryTheory.Functor.initial_iff_equivalence_comp

added theorem CategoryTheory.Functor.initial_iff_initial_comp

added theorem CategoryTheory.Functor.initial_natIso_iff

added theorem CategoryTheory.Functor.initial_of_comp_full_faithful'

added theorem CategoryTheory.Functor.initial_of_comp_full_faithful

added theorem CategoryTheory.Functor.initial_of_equivalence_comp

added theorem CategoryTheory.Functor.initial_of_initial_comp