Structures · Category theory
CategoryTheory.Functor.IsRightAdjoint
A class asserting the existence of a left adjoint.
- Defined in
- Mathlib.CategoryTheory.Adjunction.Basic
- Shape
- One type argument · adds exists_leftAdjoint
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances25
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- AddCommGrpCat
- TopCat
- Rep
- CommGrpCat
- GrpCat
- SheafOfModules
- CommRingCat
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- AlgebraicGeometry.Scheme.Modules
- ContinuousGeneratedByCat
- CommMonCat
- TopCat.Presheaf
- TopCat.Sheaf
- TopModuleCat
- SSet
- GeneratedByTopCat
- LightCondSet
- CategoryTheory.MorphismProperty.Under
- AlgebraicGeometry.Scheme.PresheafOfModules
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by63
- CategoryTheory.Adjunction.ofIsRightAdjoint
- SheafOfModules.pullback
- SheafOfModules.pullbackPushforwardAdjunction
- CategoryTheory.Functor.leftAdjoint
- SheafOfModules.pullbackObjFreeIso
- SheafOfModules.pullbackObjUnitToUnit
- SheafOfModules.pullbackComp
- PresheafOfModules.pullbackComp
- PresheafOfModules.pullback
- PresheafOfModules.pullbackPushforwardAdjunction
- CategoryTheory.Functor.sheafPullback
- CategoryTheory.Functor.sheafAdjunctionContinuous
- CategoryTheory.Functor.isRightAdjoint_of_iso
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso
- CategoryTheory.isRightAdjoint_triangle_lift
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc
- SheafOfModules.pullback_assoc
- SheafOfModules.pullback_comp_id
- SheafOfModules.pullbackObjFreeIso_hom_naturality
- SheafOfModules.pullback_id_comp
- CategoryTheory.isRightAdjoint_triangle_lift_monadic
- SheafOfModules.conjugateEquiv_pullbackComp_inv
- SheafOfModules.pullbackIso
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app
- SheafOfModules.freeFunctorCompPullbackIso
- CategoryTheory.Functor.isRightAdjoint_comp
- SheafOfModules.instIsRightAdjointPushforward
- CategoryTheory.isRightAdjoint_square_lift
- CategoryTheory.Functor.final_of_isRightAdjoint
- CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint
- SheafOfModules.sheafificationCompPullback
- CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint
- SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit
- CategoryTheory.Functor.IsRightAdjoint.leftOp
- CategoryTheory.Functor.IsRightAdjoint.exists_leftAdjoint
- CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app
- SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit
- CategoryTheory.isRightAdjoint_square_lift_monadic
- SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous
- SheafOfModules.instIsLeftAdjointPullback
- PresheafOfModules.pullback_comp_id
- CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify
- CategoryTheory.RepresentablyFlat.of_isRightAdjoint
- PresheafOfModules.pullback_id_comp
- PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp
- SheafOfModules.PullbackConstruction.adjunction
- SheafOfModules.pullbackObjFreeIso.congr_simp
- CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint
Ancestors0
No ancestors.