Structures · Category theory
CategoryTheory.Limits.PreservesFiniteLimits
A functor is said to preserve finite limits, if it preserves all limits of shape J,
where J : Type is a finite category.
- Shape
- One type argument · adds preservesFiniteLimits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances20
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- HomologicalComplex
- Action
- Rep
- SheafOfModules
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- TopCat.Sheaf
- CategoryTheory.ShortComplex
- AlgebraicGeometry.Scheme.ProEt
- AlgebraicGeometry.Scheme.Etale
- FGModuleCat
- LightProfinite
- FintypeCat
- CategoryTheory.MorphismProperty.Over
- FDRep
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by123
- CategoryTheory.ShortComplex.ShortExact.map_of_exact
- CategoryTheory.Functor.mapDerivedCategory
- CategoryTheory.Abelian.Ext.mapExactFunctor
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor
- CategoryTheory.Functor.rightDerivedZeroIsoSelf
- CategoryTheory.Functor.mapDerivedCategoryFactors
- CategoryTheory.Functor.mapExtAddHom
- CategoryTheory.Abelian.Ext.mapExactFunctor_hom
- CategoryTheory.flat_of_preservesFiniteLimits
- CategoryTheory.Limits.preservesFiniteLimits_of_natIso
- CategoryTheory.StructuredArrow.projectSubobject
- CategoryTheory.Functor.mapExtLinearMap
- CategoryTheory.Abelian.Ext.mapExactFunctor.congr_simp
- CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀
- CategoryTheory.Abelian.Ext.mapExactFunctor_comp
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'
- CategoryTheory.Abelian.Ext.mapExactFunctor₀
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc
- CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms
- CategoryTheory.LeftExactFunctor.of
- CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
- CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app
- CategoryTheory.Abelian.Ext.mapExactFunctor_extClass
- CategoryTheory.ExactFunctor.of
- CategoryTheory.HasSheafify.mk'
- CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id
- CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app
- CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app
- CategoryTheory.Functor.mapDerivedCategoryFactorsh
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc
- CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id
- CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff
- CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff
- CategoryTheory.Limits.preservesFiniteColimits_of_op
- CategoryTheory.DerivedCategory.map_triangleOfSESδ
- CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app
- CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves
- CategoryTheory.HasExactColimitsOfShape.domain_of_functor
- CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc
- CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff
- CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ
- CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality
- CategoryTheory.Limits.preservesFiniteColimits_op
- CategoryTheory.instIsIsoFunctorToRightDerivedZero
- CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors
- CategoryTheory.instIsIsoAppToRightDerivedZero
- CategoryTheory.Functor.mapExtAddHom.congr_simp
- CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh
- CategoryTheory.StructuredArrow.projectSubobject.congr_simp
- CategoryTheory.Limits.comp_preservesFiniteLimits
Ancestors0
No ancestors.