Mathlib Map

Structures · Category theory

CategoryTheory.Limits.PreservesLimitsOfShape

We say that F preserves limits of shape J if F preserves limits for every diagram K : J ⥤ C, i.e., F maps limit cones over K to limit cones.

Defined in
Mathlib.CategoryTheory.Limits.Preserves.Basic
Shape
2 explicit arguments · adds preservesLimit
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Forgetful instances

Every CategoryTheory.Limits.PreservesLimitsOfShape is also a

Concrete types that are instances25

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • HomologicalComplex
  • Action
  • CategoryTheory.Mon
  • AddCommGrpCat
  • TopologicalSpace.Opens
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • SheafOfModules
  • PresheafOfModules
  • CategoryTheory.Under
  • CategoryTheory.CostructuredArrow
  • CommMonCat
  • AddCommMonCat
  • MonCat
  • CategoryTheory.ShortComplex
  • AddMonCat
  • TopModuleCat
  • SSet
  • LightProfinite
  • CategoryTheory.MorphismProperty.CostructuredArrow
  • AlgebraicGeometry.Scheme.Opens
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by185

Ancestors1