Structures · Category theory
CategoryTheory.Functor.IsLeftAdjoint
A class asserting the existence of a right adjoint.
- Defined in
- Mathlib.CategoryTheory.Adjunction.Basic
- Shape
- One type argument · adds exists_rightAdjoint
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances22
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- TopCat
- Rep
- SheafOfModules
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- AlgebraicGeometry.Scheme.Modules
- ContinuousGeneratedByCat
- CommMonCat
- TopCat.Presheaf
- TopCat.Sheaf
- CategoryTheory.Comonad.Coalgebra
- TopModuleCat
- SSet
- GeneratedByTopCat
- LightCondSet
- CategoryTheory.MorphismProperty.Over
- AlgebraicGeometry.Scheme.Opens
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- CategoryTheory.Adjunction.ofIsLeftAdjoint
- CategoryTheory.Functor.rightAdjoint
- CategoryTheory.Functor.isLeftAdjoint_of_iso
- SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint
- CategoryTheory.isLeftAdjoint_triangle_lift_comonadic
- CategoryTheory.isLeftAdjoint_triangle_lift
- CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify
- CategoryTheory.Functor.IsLeftAdjoint.op
- CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint
- CategoryTheory.Functor.isLeftAdjoint_comp
- CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint
- CategoryTheory.Functor.rightAdjoint.congr_simp
- CategoryTheory.instIsContinuousRightAdjointOfIsCocontinuous
- CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint
- CategoryTheory.Functor.IsLeftAdjoint.leftOp
- CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint
- CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint
- CategoryTheory.Over.isLeftAdjoint_post
- CategoryTheory.isLeftAdjoint_square_lift
- SheafOfModules.isLeftAdjoint_pushforward_of_isIso
- CategoryTheory.Functor.IsLeftAdjoint.rightOp
- CategoryTheory.Under.isLeftAdjoint_post
- CategoryTheory.IsCofiltered.of_isLeftAdjoint
- CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint
- CategoryTheory.Functor.IsLeftAdjoint.exists_rightAdjoint
- CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint
- CategoryTheory.Functor.initial_of_isLeftAdjoint
- CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint
- CategoryTheory.isLeftAdjoint_square_lift_comonadic
Ancestors0
No ancestors.