Structures · Category theory
CategoryTheory.IsCardinalFiltered
A category J is κ-filtered (for a regular cardinal κ) if
any functor F : A ⥤ J from a category A such that HasCardinalLT (Arrow A) κ
admits a cocone. See isCardinalFiltered_iff for a more
concrete characterization of κ-filtered categories.
- Shape
- 2 explicit arguments · adds nonempty_cocone
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances10
- Ordinal.ToType
- CategoryTheory.Under
- CategoryTheory.CostructuredArrow
- PartOrdEmb.carrier
- HasCardinalLT.Set
- CategoryTheory.CardinalDirectedPoset.SetCardinalLT
- Subtype
- Prod
- Set.Elem
- WithTop
How is a type an instance?
Loading the hierarchy index…
Assumed by61
- CategoryTheory.isFiltered_of_isCardinalFiltered
- CategoryTheory.IsCardinalFiltered.toMax
- CategoryTheory.IsCardinalFiltered.max
- CategoryTheory.IsCardinalFiltered.toCoeq
- CategoryTheory.IsCardinalFiltered.coeq
- CategoryTheory.IsCardinalFiltered.coeqHom
- CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
- CategoryTheory.IsCardinalFiltered.coeq_condition
- CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet
- CategoryTheory.IsCardinalFiltered.cocone
- CategoryTheory.IsCardinalFiltered.of_le
- CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall
- CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered
- CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet
- CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable
- CategoryTheory.IsCardinalFiltered.wideSpan
- CategoryTheory.IsCardinalFiltered.of_equivalence
- CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit'
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι
- CategoryTheory.MorphismProperty.isClosedUnderColimitsOfShape_isLocal
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux
- CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity
- CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functor
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀
- CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall
- PartOrdEmb.instIsClosedUnderColimitsOfShapeIsCardinalFilteredOfIsCardinalFiltered
- CategoryTheory.CardinalFilteredPoset.isColimitCoconeOfPredicateSet
- PartOrdEmb.Limits.CoconePt.isCardinalFiltered_pt
- CategoryTheory.IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_map_hom_hom_apply_coe
- CategoryTheory.IsCardinalFiltered.nonempty_cocone
- CategoryTheory.IsCardinalFiltered.multicoequalizer
- CategoryTheory.IsCardinalFiltered.of_final
- CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective
- CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_obj_obj_coe
- CategoryTheory.isCardinalFiltered_prod
- CategoryTheory.IsCardinalFiltered.coeq_condition_assoc
- CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow
- CategoryTheory.CardinalFilteredPoset.functorOfPredicateSet
Ancestors0
No ancestors.