Commit 2023-03-13 13:03 b8574d74

View on Github →

feat: port CategoryTheory.Limits.Final (#2820)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Final.lean

added def CategoryTheory.Functor.Final.coconesEquiv

added theorem CategoryTheory.Functor.Final.cofinal_of_colimit_comp_coyoneda_iso_pUnit

added def CategoryTheory.Functor.Final.colimitCoconeComp

added def CategoryTheory.Functor.Final.colimitCoconeOfComp

added def CategoryTheory.Functor.Final.colimitCompCoyonedaIso

added def CategoryTheory.Functor.Final.colimitIso'

added def CategoryTheory.Functor.Final.colimitIso

added theorem CategoryTheory.Functor.Final.colimit_cocone_comp_aux

added theorem CategoryTheory.Functor.Final.colimit_pre_is_iso_aux

added def CategoryTheory.Functor.Final.extendCocone

added theorem CategoryTheory.Functor.Final.hasColimit_of_comp

added def CategoryTheory.Functor.Final.homToLift

added def CategoryTheory.Functor.Final.induction

added def CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv

added def CategoryTheory.Functor.Final.isColimitWhiskerEquiv

added def CategoryTheory.Functor.Final.lift

added theorem CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel

added def CategoryTheory.Functor.Initial.conesEquiv

added def CategoryTheory.Functor.Initial.extendCone

added theorem CategoryTheory.Functor.Initial.hasLimit_of_comp

added def CategoryTheory.Functor.Initial.homToLift

added def CategoryTheory.Functor.Initial.induction

added def CategoryTheory.Functor.Initial.isLimitExtendConeEquiv

added def CategoryTheory.Functor.Initial.isLimitWhiskerEquiv

added def CategoryTheory.Functor.Initial.lift

added def CategoryTheory.Functor.Initial.limitConeComp

added def CategoryTheory.Functor.Initial.limitConeOfComp

added def CategoryTheory.Functor.Initial.limitIso'

added def CategoryTheory.Functor.Initial.limitIso

added theorem CategoryTheory.Functor.Initial.limit_cone_comp_aux

added theorem CategoryTheory.Functor.Initial.limit_pre_is_iso_aux

added theorem CategoryTheory.Functor.final_of_adjunction

added theorem CategoryTheory.Functor.final_of_initial_op

added theorem CategoryTheory.Functor.initial_of_adjunction

added theorem CategoryTheory.Functor.initial_of_final_op