Mathlib Map

Structures · Category theory

CategoryTheory.Limits.ReflectsLimitsOfSize

A functor F : C ⥤ D reflects limits if whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D, the cone was already a limit cone in C. Note that we do not assume a priori that D actually has any limits.

Defined in
Mathlib.CategoryTheory.Limits.Preserves.Basic
Shape
One type argument · adds reflectsLimitsOfShape

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances3

  • ModuleCat
  • Rep
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by20

Ancestors0

No ancestors.