Structures · Category theory
CategoryTheory.ExponentiableMorphism
A morphism f : I ⟶ J is exponentiable if the pullback functor Over J ⥤ Over I
has a right adjoint.
- Shape
- One type argument · adds pushforward, pullbackPushforwardAdj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CategoryTheory.ExponentiableMorphism.pushforward
- CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj
- CategoryTheory.ExponentiableMorphism.coev
- CategoryTheory.ExponentiableMorphism.ev
- CategoryTheory.ExponentiableMorphism.comp
- CategoryTheory.ExponentiableMorphism.pushforwardComp
- CategoryTheory.ExponentiableMorphism.pushforwardId
- CategoryTheory.ExponentiableMorphism.pushforwardUncurry
- CategoryTheory.ExponentiableMorphism.pushforwardCurry
- CategoryTheory.ExponentiableMorphism.ev_coev
- CategoryTheory.ExponentiableMorphism.ev_naturality
- CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit
- CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit
- CategoryTheory.ExponentiableMorphism.coev_ev
- CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom
- CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom
- CategoryTheory.ExponentiableMorphism.coev_naturality
- CategoryTheory.ExponentiableMorphism.coev_def
- CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc
- CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq
- CategoryTheory.ExponentiableMorphism.pushforward_uncurry_curry
- CategoryTheory.ExponentiableMorphism.isExponentiable
- CategoryTheory.ExponentiableMorphism.coev_naturality_assoc
- CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc
- CategoryTheory.ExponentiableMorphism.ev_coev_assoc
- CategoryTheory.ExponentiableMorphism.ev_def
- CategoryTheory.ExponentiableMorphism.OverMkHom
- CategoryTheory.ExponentiableMorphism.pushforward_curry_uncurry
- CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq
- CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc
- CategoryTheory.ExponentiableMorphism.comp_pushforward
- CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc
- CategoryTheory.ExponentiableMorphism.coev_ev_assoc
- CategoryTheory.ExponentiableMorphism.ev_naturality_assoc
Ancestors0
No ancestors.