Structures · Category theory
CategoryTheory.Reflective
A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.
- Shape
- One type argument · adds L, adj
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- CategoryTheory.Functor
- CategoryTheory.Over
- AlgebraicGeometry.Scheme
- TopCat
- AlgebraicGeometry.LocallyRingedSpace
- SSet
- CategoryTheory.Cat
- CategoryTheory.SimplicialObject
- CompHaus
- UniformSpaceCat
- SSet.Truncated
How is a type an instance?
Loading the hierarchy index…
Assumed by49
- CategoryTheory.reflector
- CategoryTheory.reflectorAdjunction
- CategoryTheory.unitCompPartialBijective
- CategoryTheory.equivEssImageOfReflective
- CategoryTheory.bijection
- CategoryTheory.hasLimitsOfShape_of_reflective
- CategoryTheory.hasLimit_of_reflective
- CategoryTheory.hasColimitsOfShape_of_reflective
- CategoryTheory.unitCompPartialBijectiveAux
- CategoryTheory.Functor.essImage.unit_isIso
- CategoryTheory.unitCompPartialBijective_symm_apply
- CategoryTheory.hasColimits_of_reflective
- CategoryTheory.unitCompPartialBijective_symm_natural
- CategoryTheory.bijection_symm_apply_id
- CategoryTheory.bijection_natural
- CategoryTheory.unitCompPartialBijectiveAux_symm_apply
- CategoryTheory.Functor.fullyFaithfulOfReflective
- CategoryTheory.preservesBinaryProducts_of_exponentialIdeal
- CategoryTheory.unitCompPartialBijective_natural
- CategoryTheory.leftAdjoint_preservesTerminal_of_reflective
- CategoryTheory.Reflective.L
- CategoryTheory.prodComparison_iso
- CategoryTheory.mem_essImage_of_unit_isSplitMono
- CategoryTheory.Reflective.adj
- CategoryTheory.instIsRightAdjointOfReflective
- CategoryTheory.exponentialIdeal_of_preservesBinaryProducts
- CategoryTheory.equivEssImageOfReflective_unitIso
- CategoryTheory.μ_iso_of_reflective
- CategoryTheory.cartesianClosedOfReflective'
- CategoryTheory.reflective_products
- CategoryTheory.instIsLeftAdjointReflector
- CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage
- CategoryTheory.Limits.PreservesFiniteProducts.of_exponentialIdeal
- CategoryTheory.CartesianMonoidalCategory.ofReflective
- CategoryTheory.Reflective.comp
- CategoryTheory.monadicOfReflective
- CategoryTheory.cartesianClosedOfReflective
- CategoryTheory.exponentialIdealReflective
- CategoryTheory.Reflective.toFaithful
- CategoryTheory.Reflective.comparison_essSurj
- CategoryTheory.unit_obj_eq_map_unit
- CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA
- CategoryTheory.equivEssImageOfReflective_inverse
- CategoryTheory.ExponentialIdeal.mk_of_iso
- CategoryTheory.equivEssImageOfReflective_counitIso
- CategoryTheory.Reflective.toFull
- CategoryTheory.unitCompPartialBijective.congr_simp
- CategoryTheory.equivEssImageOfReflective_functor
- CategoryTheory.hasLimits_of_reflective