Finite

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

Statistics

Metric	Count
Definitions PreservesFiniteColimits, PreservesFiniteCoproducts, PreservesFiniteLimits, PreservesFiniteProducts, ReflectsFiniteColimits, ReflectsFiniteCoproducts, ReflectsFiniteLimits, ReflectsFiniteProducts	8
Theorems preservesFiniteColimits, preservesFiniteColimits, preservesFiniteColimits, preservesFiniteColimits, preserves, preservesFiniteLimits, preserves, preservesFiniteLimits, preservesFiniteLimits, preservesFiniteLimits, reflectsFiniteColimits, reflects, reflects, reflects, reflects, reflectsFiniteLimits, comp_preservesFiniteColimits, comp_preservesFiniteCoproducts, comp_preservesFiniteLimits, comp_preservesFiniteProducts, comp_reflectsFiniteCoproducts, comp_reflectsFiniteProducts, instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts, instPreservesFiniteCoproductsOfPreservesFiniteColimits, instPreservesFiniteProductsOfPreservesFiniteLimits, instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts, instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite, instReflectsFiniteColimitsOfReflectsColimits, instReflectsFiniteColimitsOfReflectsColimitsOfSize, instReflectsFiniteCoproductsOfReflectsFiniteColimits, instReflectsFiniteLimitsOfReflectsLimits, instReflectsFiniteLimitsOfReflectsLimitsOfSize, instReflectsFiniteProductsOfReflectsFiniteLimits, instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite, preservesColimitsOfShapeOfPreservesFiniteColimits, preservesFiniteColimits_of_natIso, preservesFiniteColimits_of_preservesFiniteColimitsOfSize, preservesFiniteColimits_of_reflects_of_preserves, preservesFiniteCoproducts_of_reflects_of_preserves, preservesFiniteLimits_of_natIso, preservesFiniteLimits_of_preservesFiniteLimitsOfSize, preservesFiniteLimits_of_reflects_of_preserves, preservesFiniteProducts_of_reflects_of_preserves, preservesLimitsOfShapeOfPreservesFiniteLimits, reflectsFiniteColimitsOfReflectsIsomorphisms, reflectsFiniteCoproductsOfReflectsIsomorphisms, reflectsFiniteLimits_of_reflectsIsomorphisms, reflectsFiniteProducts_of_reflectsIsomorphisms	48
Total	56

CategoryTheory.Limits

Definitions

Name	Category	Theorems
PreservesFiniteColimits 📖	CompData	57 math math: CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁, CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology, CategoryTheory.preservesFiniteColimits_liftToFinset, PreservesColimits.preservesFiniteColimits, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits, preservesFiniteColimits_of_op, CategoryTheory.Abelian.freyd_mitchell, CategoryTheory.preservesFiniteColimits_of_coflat, ModuleCat.instPreservesFiniteColimitsUliftFunctor, preservesFiniteColimits_of_preservesInitial_and_pushouts, preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, preservesFiniteColimits_rightOp, CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels, ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor, preservesFiniteColimits_of_leftOp, preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits, CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂, preservesFiniteColimits_leftOp, PreservesColimitsOfSize0.preservesFiniteColimits, CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi, PreservesFiniteColimits.underPost, CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective, preservesFiniteColimits_op, CategoryTheory.ObjectProperty.preservesFiniteColimits_iff, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃, Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits, Action.instPreservesFiniteColimitsForgetOfHasFiniteColimits, FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomCarrier, PreservesColimitsOfSize.preservesFiniteColimits, CategoryTheory.preservesFiniteColimits_iff_coflat, PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits, preservesFiniteColimits_of_unop, CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor, HomologicalComplex.instPreservesFiniteColimitsSingle, CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor, CategoryTheory.rightExactFunctor_iff, preservesFiniteColimits_of_reflects_of_preserves, HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits, CategoryTheory.instPreservesFiniteColimitsObjFunctorExactFunctor, preservesFiniteColimits_unop, PresheafOfModules.Finite.evaluation_preservesFiniteColimits, instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits, comp_preservesFiniteColimits, CategoryTheory.exactFunctor_iff, CategoryTheory.Functor.exact_tfae, preservesFiniteColimits_of_preservesFiniteColimitsOfSize, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding, CategoryTheory.Functor.preservesFiniteColimits_tfae, preservesFiniteColimits_of_rightOp, FintypeCat.inclusion_preservesFiniteColimits, CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits, preservesFiniteColimits_of_natIso, CategoryTheory.instPreservesFiniteColimitsIndYoneda
PreservesFiniteCoproducts 📖	CompData	12 math math: CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts, preservesFiniteCoproducts_rightOp, CategoryTheory.Functor.preservesFiniteCoproductsOfAdditive, preservesFiniteCoproducts_unop, instPreservesFiniteCoproductsOfPreservesFiniteColimits, CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts, comp_preservesFiniteCoproducts, preservesFiniteCoproducts_op, CompHausLike.instPreservesFiniteCoproductsToCompHausLike, preservesFiniteCoproducts_leftOp, preservesFiniteCoproducts_of_reflects_of_preserves
PreservesFiniteLimits 📖	CompData	95 math math: CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology, CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits, CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels, preservesFiniteLimits_of_leftOp, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, PresheafOfModules.toPresheaf_preservesFiniteLimits, preservesFiniteLimits_of_op, CategoryTheory.lan_preservesFiniteLimits_of_flat, CategoryTheory.Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback, preservesFiniteLimits_op, HomologicalComplex.instPreservesFiniteLimitsEvalOfHasFiniteLimits, ModuleCat.preservesFiniteLimits_extendScalars_of_flat, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat, CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify, CategoryTheory.Abelian.freyd_mitchell, CategoryTheory.GrothendieckTopology.preserveFiniteLimits_plusFunctor, CategoryTheory.preservesFiniteLimits_liftToFinset, PreservesFiniteLimits.overPost, CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits, CommRingCat.Under.preservesFiniteLimits_of_flat, preservesFiniteLimits_of_reflects_of_preserves, CategoryTheory.HasSheafify.isLeftExact, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, CommRingCat.Under.instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, preservesFiniteLimits_of_rightOp, Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits, instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits, Action.instPreservesFiniteLimitsForgetOfHasFiniteLimits, preservesFiniteLimits_leftOp, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits, CategoryTheory.ObjectProperty.preservesFiniteLimits_iff, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, preservesFiniteLimits_of_preservesFiniteLimitsOfSize, isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits, CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁, CategoryTheory.preservesFiniteLimits_presheafToSheaf, FintypeCat.inclusion_preservesFiniteLimits, CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor, preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts, PresheafOfModules.evaluation_preservesFiniteLimits, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, CategoryTheory.Functor.preservesFiniteLimits_tfae, instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget, AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux, CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor, preservesFiniteLimits_of_preservesTerminal_and_pullbacks, isIndObject_iff_preservesFiniteLimits, CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono, CategoryTheory.leftExactFunctor_iff, CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget, preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda, CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits, preservesFiniteLimits_rightOp, CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₂, SheafOfModules.Finite.forgetPreservesFiniteLimits, CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, preservesFiniteLimits_unop, CategoryTheory.GrothendieckTopology.preservesFiniteLimits_sheafification, CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits, ModuleCat.instPreservesFiniteLimitsUliftFunctor, PreservesLimits.preservesFiniteLimits, Module.Flat.iff_preservesFiniteLimits_tensorLeft, PreservesLimitsOfSize0.preservesFiniteLimits, ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, preservesFiniteLimits_of_unop, ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor, FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier, Module.Flat.instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, CategoryTheory.preservesFiniteLimits_iff_flat, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, HomologicalComplex.instPreservesFiniteLimitsSingle, PreservesLimitsOfSize.preservesFiniteLimits, CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₃, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CategoryTheory.exactFunctor_iff, preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits, CategoryTheory.Functor.exact_tfae, comp_preservesFiniteLimits, filtered_colim_preservesFiniteLimits_of_types, CategoryTheory.instPreservesFiniteLimitsObjFunctorExactFunctor, SheafOfModules.Finite.evaluationPreservesFiniteLimits, preservesFiniteLimits_of_natIso, CategoryTheory.preservesFiniteLimits_of_flat, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding
PreservesFiniteProducts 📖	CompData	33 math math: PreservesFiniteProducts.of_preserves_binary_and_terminal, instPreservesFiniteProductsOfPreservesFiniteLimits, CategoryTheory.instPreservesFiniteProductsOppositeVal, CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts, PreservesFiniteProducts.of_exponentialIdeal, CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts, CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q', CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, Condensed.instPreservesFiniteProductsOppositeCompHausVal, CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts, CategoryTheory.hoFunctor.preservesFiniteProducts, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive, CategoryTheory.IsSifted.colim_preservesFiniteProducts_of_isSifted, preservesFiniteProducts_leftOp, preservesFiniteProducts_op, CategoryTheory.Localization.preservesFiniteProducts, CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective, preservesFiniteProducts_unop, preservesFiniteProducts_rightOp, instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat, CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal, CommRingCat.Under.instPreservesFiniteProductsUnderTensorProd, Condensed.instPreservesFiniteProductsOppositeStoneanVal, CategoryTheory.Functor.preservesFiniteProductsOfAdditive, comp_preservesFiniteProducts, preservesFiniteProducts_of_reflects_of_preserves, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ, CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf'
ReflectsFiniteColimits 📖	CompData	4 math math: ReflectsColimitsOfSize.reflectsFiniteColimits, instReflectsFiniteColimitsOfReflectsColimits, reflectsFiniteColimitsOfReflectsIsomorphisms, instReflectsFiniteColimitsOfReflectsColimitsOfSize
ReflectsFiniteCoproducts 📖	CompData	3 math math: reflectsFiniteCoproductsOfReflectsIsomorphisms, comp_reflectsFiniteCoproducts, instReflectsFiniteCoproductsOfReflectsFiniteColimits
ReflectsFiniteLimits 📖	CompData	5 math math: reflectsFiniteLimits_of_reflectsIsomorphisms, ReflectsLimitsOfSize.reflectsFiniteLimits, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, instReflectsFiniteLimitsOfReflectsLimitsOfSize, instReflectsFiniteLimitsOfReflectsLimits
ReflectsFiniteProducts 📖	CompData	3 math math: comp_reflectsFiniteProducts, reflectsFiniteProducts_of_reflectsIsomorphisms, instReflectsFiniteProductsOfReflectsFiniteLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_preservesFiniteColimits 📖	mathematical	—	PreservesFiniteColimits CategoryTheory.Functor.comp	—	comp_preservesColimitsOfShape PreservesFiniteColimits.preservesFiniteColimits
comp_preservesFiniteCoproducts 📖	mathematical	—	PreservesFiniteCoproducts CategoryTheory.Functor.comp	—	comp_preservesColimitsOfShape instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
comp_preservesFiniteLimits 📖	mathematical	—	PreservesFiniteLimits CategoryTheory.Functor.comp	—	comp_preservesLimitsOfShape PreservesFiniteLimits.preservesFiniteLimits
comp_preservesFiniteProducts 📖	mathematical	—	PreservesFiniteProducts CategoryTheory.Functor.comp	—	comp_preservesLimitsOfShape instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
comp_reflectsFiniteCoproducts 📖	mathematical	—	ReflectsFiniteCoproducts CategoryTheory.Functor.comp	—	comp_reflectsColimitsOfShape instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite Finite.of_fintype
comp_reflectsFiniteProducts 📖	mathematical	—	ReflectsFiniteProducts CategoryTheory.Functor.comp	—	comp_reflectsLimitsOfShape instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite Finite.of_fintype
instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts 📖	mathematical	—	PreservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin PreservesFiniteCoproducts.preserves preservesColimitsOfShape_of_equiv
instPreservesFiniteCoproductsOfPreservesFiniteColimits 📖	mathematical	—	PreservesFiniteCoproducts	—	PreservesFiniteColimits.preservesFiniteColimits
instPreservesFiniteProductsOfPreservesFiniteLimits 📖	mathematical	—	PreservesFiniteProducts	—	PreservesFiniteLimits.preservesFiniteLimits
instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts 📖	mathematical	—	PreservesLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin PreservesFiniteProducts.preserves preservesLimitsOfShape_of_equiv
instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite 📖	mathematical	—	ReflectsColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin ReflectsFiniteCoproducts.reflects reflectsColimitsOfShape_of_equiv
instReflectsFiniteColimitsOfReflectsColimits 📖	mathematical	—	ReflectsFiniteColimits	—	ReflectsColimitsOfSize.reflectsFiniteColimits
instReflectsFiniteColimitsOfReflectsColimitsOfSize 📖	mathematical	—	ReflectsFiniteColimits	—	ReflectsColimitsOfSize.reflectsFiniteColimits
instReflectsFiniteCoproductsOfReflectsFiniteColimits 📖	mathematical	—	ReflectsFiniteCoproducts	—	ReflectsFiniteColimits.reflects
instReflectsFiniteLimitsOfReflectsLimits 📖	mathematical	—	ReflectsFiniteLimits	—	ReflectsLimitsOfSize.reflectsFiniteLimits
instReflectsFiniteLimitsOfReflectsLimitsOfSize 📖	mathematical	—	ReflectsFiniteLimits	—	ReflectsLimitsOfSize.reflectsFiniteLimits
instReflectsFiniteProductsOfReflectsFiniteLimits 📖	mathematical	—	ReflectsFiniteProducts	—	ReflectsFiniteLimits.reflects
instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite 📖	mathematical	—	ReflectsLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	Finite.exists_equiv_fin ReflectsFiniteProducts.reflects reflectsLimitsOfShape_of_equiv
preservesColimitsOfShapeOfPreservesFiniteColimits 📖	mathematical	—	PreservesColimitsOfShape	—	preservesColimitsOfShape_of_equiv PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteColimits_of_natIso 📖	mathematical	—	PreservesFiniteColimits	—	preservesColimitsOfShape_of_natIso PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteColimits_of_preservesFiniteColimitsOfSize 📖	mathematical	PreservesColimitsOfShape	PreservesFiniteColimits	—	preservesColimitsOfShape_of_equiv
preservesFiniteColimits_of_reflects_of_preserves 📖	mathematical	—	PreservesFiniteColimits	—	preservesColimitsOfShape_of_reflects_of_preserves PreservesFiniteColimits.preservesFiniteColimits ReflectsFiniteColimits.reflects
preservesFiniteCoproducts_of_reflects_of_preserves 📖	mathematical	—	PreservesFiniteCoproducts	—	preservesColimitsOfShape_of_reflects_of_preserves instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite
preservesFiniteLimits_of_natIso 📖	mathematical	—	PreservesFiniteLimits	—	preservesLimitsOfShape_of_natIso PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteLimits_of_preservesFiniteLimitsOfSize 📖	mathematical	PreservesLimitsOfShape	PreservesFiniteLimits	—	preservesLimitsOfShape_of_equiv
preservesFiniteLimits_of_reflects_of_preserves 📖	mathematical	—	PreservesFiniteLimits	—	preservesLimitsOfShape_of_reflects_of_preserves PreservesFiniteLimits.preservesFiniteLimits ReflectsFiniteLimits.reflects
preservesFiniteProducts_of_reflects_of_preserves 📖	mathematical	—	PreservesFiniteProducts	—	preservesLimitsOfShape_of_reflects_of_preserves instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite
preservesLimitsOfShapeOfPreservesFiniteLimits 📖	mathematical	—	PreservesLimitsOfShape	—	preservesLimitsOfShape_of_equiv PreservesFiniteLimits.preservesFiniteLimits
reflectsFiniteColimitsOfReflectsIsomorphisms 📖	mathematical	—	ReflectsFiniteColimits	—	reflectsColimitsOfShape_of_reflectsIsomorphisms hasColimitsOfShape_of_hasFiniteColimits PreservesFiniteColimits.preservesFiniteColimits
reflectsFiniteCoproductsOfReflectsIsomorphisms 📖	mathematical	—	ReflectsFiniteCoproducts	—	reflectsColimitsOfShape_of_reflectsIsomorphisms hasColimitsOfShape_discrete Finite.of_fintype instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts
reflectsFiniteLimits_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsFiniteLimits	—	reflectsLimitsOfShape_of_reflectsIsomorphisms hasLimitsOfShape_of_hasFiniteLimits PreservesFiniteLimits.preservesFiniteLimits
reflectsFiniteProducts_of_reflectsIsomorphisms 📖	mathematical	—	ReflectsFiniteProducts	—	reflectsLimitsOfShape_of_reflectsIsomorphisms hasLimitsOfShape_discrete Finite.of_fintype instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts

CategoryTheory.Limits.PreservesColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits	—	CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits

CategoryTheory.Limits.PreservesColimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits	—	CategoryTheory.Limits.preservesColimitsOfShape_of_equiv preservesColimitsOfShape CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits

CategoryTheory.Limits.PreservesColimitsOfSize0

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits	—	CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits

CategoryTheory.Limits.PreservesFiniteColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	—

CategoryTheory.Limits.PreservesFiniteCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.Limits.PreservesFiniteLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape	—	—

CategoryTheory.Limits.PreservesFiniteProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.Limits.PreservesLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits

CategoryTheory.Limits.PreservesLimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits	—	CategoryTheory.Limits.preservesLimitsOfShape_of_equiv preservesLimitsOfShape CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits

CategoryTheory.Limits.PreservesLimitsOfSize0

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits

CategoryTheory.Limits.ReflectsColimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.ReflectsFiniteColimits	—	CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits

CategoryTheory.Limits.ReflectsFiniteColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfShape	—	—

CategoryTheory.Limits.ReflectsFiniteCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.Limits.ReflectsFiniteLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfShape	—	—

CategoryTheory.Limits.ReflectsFiniteProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

CategoryTheory.Limits.ReflectsLimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.ReflectsFiniteLimits	—	CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits

---

← Back to Index