Structures · Category theory
CategoryTheory.Functor.Final
A functor F : C ⥤ D is final if for every d : D, the comma category of morphisms d ⟶ F.obj c
is connected.
- Defined in
- Mathlib.CategoryTheory.Limits.Final
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances14
- Nat
- CategoryTheory.Comma
- CategoryTheory.Under
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- CategoryTheory.Pairwise
- CategoryTheory.Grothendieck
- CategoryTheory.FinallySmall.FilteredFinalModel
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.IndObjectPresentation.I
- CategoryTheory.FinalModel
- Subtype
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by116
- CategoryTheory.Functor.Final.extendCocone
- CategoryTheory.Functor.Final.colimitIso
- CategoryTheory.Functor.Final.isColimitWhiskerEquiv
- CategoryTheory.Functor.final_of_natIso
- CategoryTheory.Limits.ColimitPresentation.reindex
- CategoryTheory.Functor.Final.lift
- SheafOfModules.pullbackObjFreeIso
- CategoryTheory.Functor.Final.homToLift
- CategoryTheory.Functor.final_of_final_comp
- CategoryTheory.Functor.final_of_comp_full_faithful
- CategoryTheory.Functor.Final.coconesEquiv
- CategoryTheory.Functor.Final.colimIso
- CategoryTheory.Functor.Final.colimitCoconeOfComp
- CategoryTheory.FinallySmall.mk'
- CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final
- CategoryTheory.IsFiltered.of_final
- CategoryTheory.ObjectProperty.ColimitOfShape.reindex
- CategoryTheory.Functor.initial_of_final_op
- CategoryTheory.IsFilteredOrEmpty.of_final
- CategoryTheory.finallySmall_of_final_of_finallySmall
- CategoryTheory.Functor.Final.hasColimit_of_comp
- CategoryTheory.Functor.final_of_comp_full_faithful'
- CategoryTheory.Functor.isConnected_iff_of_final
- CategoryTheory.Functor.Final.colimitCoconeComp
- CategoryTheory.Functor.Final.hasColimitsOfShape_of_final
- CategoryTheory.Functor.Final.ι_colimitIso_hom
- CategoryTheory.hasExactColimitsOfShape_of_final
- CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom
- CategoryTheory.Functor.Final.induction
- CategoryTheory.Functor.IsDenseAt.iff_of_final
- CategoryTheory.IsSifted.of_final_functor_from_sifted'
- CategoryTheory.Functor.Final.preservesColimit_of_comp
- CategoryTheory.isFiltered_of_isFiltered_costructuredArrow
- CategoryTheory.Functor.IsDenseAt.of_final
- CategoryTheory.Functor.DenseAt.precompEquivOfFinal
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc
- CategoryTheory.Functor.Final.hasColimit_comp_iff
- CategoryTheory.Functor.Final.reflectsColimit_of_comp
- CategoryTheory.MorphismProperty.colimitsOfShape_le_of_final
- CategoryTheory.Limits.ColimitPresentation.reindex.congr_simp
- CategoryTheory.Functor.final_equivalence_comp
- CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv
- CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final
- CategoryTheory.Functor.Final.exists_coeq_of_locally_small
- CategoryTheory.Functor.Final.ι_colimitIso_inv
- SheafOfModules.pullbackObjFreeIso_hom_naturality
- CategoryTheory.Limits.IsColimit.underPost
- CategoryTheory.Functor.final_of_equivalence_comp
- CategoryTheory.Functor.final_comp_equivalence
Ancestors0
No ancestors.