Structures · Category theory
CategoryTheory.Limits.ReflectsLimit
A functor F : C ⥤ D reflects limits for K : J ⥤ C if
whenever the image of a cone over K 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.
- Shape
- 2 explicit arguments · adds reflects
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- ModuleCat
- Action
- AlgebraicGeometry.LocallyRingedSpace
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CategoryTheory.Limits.isLimitOfReflects
- CategoryTheory.IsPullback.of_map
- CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves
- CategoryTheory.IsPullback.of_map_of_faithful
- CategoryTheory.Limits.IsTerminal.isTerminalOfObj
- CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap
- CategoryTheory.Limits.reflectsColimit_of_rightOp
- CategoryTheory.Square.IsPullback.of_map
- CategoryTheory.Limits.reflectsColimit_rightOp
- CategoryTheory.Functor.Initial.reflectsLimit_of_comp
- CategoryTheory.Limits.ReflectsLimit.reflects
- CategoryTheory.Limits.reflectsColimit_leftOp
- CategoryTheory.Limits.reflectsColimit_of_op
- CategoryTheory.Square.IsPullback.map_iff
- CategoryTheory.Limits.reflectsLimit_of_natIso
- CategoryTheory.IsPullback.map_iff
- CategoryTheory.Limits.reflectsColimit_of_unop
- CategoryTheory.Limits.isLimitOfIsLimitForkMap
- CategoryTheory.Limits.reflectsColimit_unop
- CategoryTheory.Limits.reflectsColimit_of_leftOp
- CategoryTheory.Limits.reflectsColimit_op
- CategoryTheory.Limits.IsTerminal.isTerminalOfObj.congr_simp
- CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects
- CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit
- CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal
- CategoryTheory.Limits.Concrete.terminalIffUnique
- CategoryTheory.Limits.IsTerminal.isTerminalIffObj
- CategoryTheory.GlueData.vPullbackConeIsLimitOfMap
- CategoryTheory.reflects_mono_of_reflectsLimit
- CategoryTheory.Comonad.ComonadicityInternal.unitEqualizerOfCoreflectsEqualizer
- CategoryTheory.Limits.reflectsLimit_of_iso_diagram
- CategoryTheory.Limits.isLimitOfIsLimitFanMkObj
- CategoryTheory.Functor.Initial.comp_reflectsLimit
- CategoryTheory.Limits.comp_reflectsLimit
Ancestors0
No ancestors.