Structures · Category theory
CategoryTheory.Coreflective
A functor is coreflective, or a coreflective inclusion, if it is fully faithful and left adjoint.
- Shape
- One type argument · adds R, adj
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- GeneratedByTopCat
- SSet.Truncated
- CategoryTheory.SimplicialObject.Truncated
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- CategoryTheory.coreflectorAdjunction
- CategoryTheory.coreflector
- CategoryTheory.hasColimit_of_coreflective
- CategoryTheory.Functor.essImage.counit_isIso
- CategoryTheory.hasLimitsOfShape_of_coreflective
- CategoryTheory.hasColimitsOfShape_of_coreflective
- CategoryTheory.δ_iso_of_coreflective
- CategoryTheory.hasColimits_of_coreflective
- CategoryTheory.rightAdjoint_preservesInitial_of_coreflective
- CategoryTheory.instIsRightAdjointCoreflector
- CategoryTheory.Coreflective.R
- CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA
- CategoryTheory.Coreflective.comparison_essSurj
- CategoryTheory.Coreflective.toFaithful
- CategoryTheory.instIsLeftAdjointOfCoreflective
- CategoryTheory.comonadicOfCoreflective
- CategoryTheory.Coreflective.comp
- CategoryTheory.counit_obj_eq_map_counit
- CategoryTheory.Coreflective.toFull
- CategoryTheory.mem_essImage_of_counit_isSplitEpi
- CategoryTheory.hasLimits_of_coreflective
- CategoryTheory.Functor.fullyFaithfulOfCoreflective
- CategoryTheory.Coreflective.adj