Sifted

📁 Source: Mathlib/CategoryTheory/Limits/Sifted.lean

Statistics

Metric	Count
Definitions IsSifted, IsSiftedOrEmpty	2
Theorems colim_preservesBinaryProducts_of_isSifted, colim_preservesFiniteProducts_of_isSifted, colim_preservesLimitsOfShape_pempty_of_isSifted, colim_preservesLimits_pair_of_sSifted, colim_preservesTerminal_of_isSifted, factorization_prodComparison_colim, instIsConnected, instIsIsoObjFunctorTypeColimTensorObjProdComparison, instIsSiftedOrEmptyOfHasBinaryCoproducts, isSiftedOrEmpty_of_colim_preservesBinaryProducts, isSiftedOrEmpty_of_colim_preservesFiniteProducts, isSifted_iff_asSmallIsSifted, isSifted_of_equiv, isSifted_of_hasBinaryCoproducts_and_nonempty, nonempty, nonempty_of_colim_preservesLimitsOfShapeFinZero, of_colim_preservesFiniteProducts, of_final_functor_from_sifted, of_final_functor_from_sifted', toFinal, instFinalProdProd'	21
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
IsSifted 📖	CompData	8 math math: IsSifted.of_final_functor_from_sifted, IsSifted.of_final_functor_from_sifted', IsSifted.isSifted_of_equiv, IsFiltered.isSifted, GrothendieckTopology.Point.instIsSiftedOppositeElementsFiber, IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty, IsSifted.isSifted_iff_asSmallIsSifted, IsSifted.of_colim_preservesFiniteProducts
IsSiftedOrEmpty 📖	MathDef	4 math math: IsSifted.instIsSiftedOrEmptyOfHasBinaryCoproducts, IsSifted.isSiftedOrEmpty_of_colim_preservesFiniteProducts, IsFilteredOrEmpty.isSiftedOrEmpty, IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFinalProdProd' 📖	mathematical	—	Functor.Final prod' Functor.prod'	—	Functor.final_comp instFinalProdProd

CategoryTheory.IsSifted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colim_preservesBinaryProducts_of_isSifted 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.preservesLimit_of_iso_diagram colim_preservesLimits_pair_of_sSifted
colim_preservesFiniteProducts_of_isSifted 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self colim_preservesBinaryProducts_of_isSifted colim_preservesLimitsOfShape_pempty_of_isSifted CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts
colim_preservesLimitsOfShape_pempty_of_isSifted 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self colim_preservesTerminal_of_isSifted
colim_preservesLimits_pair_of_sSifted 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self instIsIsoObjFunctorTypeColimTensorObjProdComparison
colim_preservesTerminal_of_isSifted 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.Limits.preservesTerminal_of_iso CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.Types.instHasColimitConstPUnitFunctor instIsConnected CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
factorization_prodComparison_colim 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Limits.colimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.tensor CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.externalProductBifunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.diag CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Iso.hom CategoryTheory.Limits.HasColimit.isoOfNatIso CategoryTheory.Iso.symm CategoryTheory.Iso.app CategoryTheory.MonoidalCategory.externalProductCompDiagIso CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Limits.instHasColimitProd CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Functor.curry CategoryTheory.Limits.colim CategoryTheory.Limits.colimit.pre CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left CategoryTheory.instBraidedCategoryType CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.instIsLeftAdjointTensorLeft CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Functor.cartesianMonoidalCategory	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Limits.instHasColimitProd CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.instIsLeftAdjointTensorLeft CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc CategoryTheory.Limits.colimit.ι_pre_assoc CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.Limits.ι_colimMap CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp
instIsConnected 📖	mathematical	—	CategoryTheory.IsConnected	—	CategoryTheory.isConnected_of_zigzag nonempty CategoryTheory.IsConnected.is_nonempty CategoryTheory.Functor.Final.out toFinal CategoryTheory.Zag.of_hom CategoryTheory.Zag.of_inv
instIsIsoObjFunctorTypeColimTensorObjProdComparison 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colim CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.cartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.prodComparison	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.instHasColimitProd CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.instIsLeftAdjointTensorLeft factorization_prodComparison_colim CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Functor.Final.colimit_pre_isIso toFinal
instIsSiftedOrEmptyOfHasBinaryCoproducts 📖	mathematical	—	CategoryTheory.IsSiftedOrEmpty	—	CategoryTheory.isConnected_of_zigzag CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Zag.of_inv CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Zag.of_hom
isSiftedOrEmpty_of_colim_preservesBinaryProducts 📖	mathematical	—	CategoryTheory.IsSiftedOrEmpty	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit CategoryTheory.Limits.Types.hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
isSiftedOrEmpty_of_colim_preservesFiniteProducts 📖	mathematical	—	CategoryTheory.IsSiftedOrEmpty	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self isSiftedOrEmpty_of_colim_preservesBinaryProducts CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
isSifted_iff_asSmallIsSifted 📖	mathematical	—	CategoryTheory.IsSifted CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall	—	isSifted_of_equiv
isSifted_of_equiv 📖	mathematical	—	CategoryTheory.IsSifted	—	CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Category.assoc CategoryTheory.Equivalence.counitIso_inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Functor.final_iff_comp_equivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.final_iff_final_comp CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.final_of_natIso toFinal nonempty
isSifted_of_hasBinaryCoproducts_and_nonempty 📖	mathematical	—	CategoryTheory.IsSifted	—	instIsSiftedOrEmptyOfHasBinaryCoproducts
nonempty 📖	—	—	—	—	—
nonempty_of_colim_preservesLimitsOfShapeFinZero 📖	—	—	—	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimit univLE_of_max CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.preservesLimitsOfShape_of_equiv CategoryTheory.IsConnected.is_nonempty
of_colim_preservesFiniteProducts 📖	mathematical	—	CategoryTheory.IsSifted	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self isSiftedOrEmpty_of_colim_preservesFiniteProducts nonempty_of_colim_preservesLimitsOfShapeFinZero CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
of_final_functor_from_sifted 📖	mathematical	—	CategoryTheory.IsSifted	—	isSifted_iff_asSmallIsSifted of_final_functor_from_sifted' CategoryTheory.Functor.final_comp CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
of_final_functor_from_sifted' 📖	mathematical	—	CategoryTheory.IsSifted	—	CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.preservesLimitsOfShape_of_natIso CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.whiskeringLeft_preservesLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts colim_preservesFiniteProducts_of_isSifted of_colim_preservesFiniteProducts
toFinal 📖	mathematical	—	CategoryTheory.Functor.Final CategoryTheory.uniformProd CategoryTheory.Functor.diag	—	—

---

← Back to Index