Exponentiable morphisms #
We define an exponentiable morphism f : I ⟶ J to be a morphism with a functorial choice of
pullbacks, given by ChosenPullbacksAlong f, together with a right adjoint to
the pullback functor ChosenPullbacksAlong.pullback f : Over J ⥤ Over I. We call this right adjoint
the pushforward functor along f.
Main results #
- The identity morphisms are exponentiable.
- The composition of exponentiable morphisms is exponentiable.
TODO #
- Any pullback of an exponentiable morphism is exponentiable.
class
CategoryTheory.ExponentiableMorphism
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
:
Type (max u v)
A morphism f : I ⟶ J is exponentiable if the pullback functor Over J ⥤ Over I
has a right adjoint.
The pushforward functor
The pushforward functor is right adjoint to the pullback functor
Instances
@[reducible, inline]
A morphism f : I ⟶ J is exponentiable if the pullback functor Over J ⥤ Over I
has a right adjoint.
Instances For
instance
CategoryTheory.ExponentiableMorphism.isExponentiable
{C : Type u}
[Category.{v, u} C]
[ChosenPullbacks C]
{I J : C}
(f : I ⟶ J)
[ExponentiableMorphism f]
:
def
CategoryTheory.ExponentiableMorphism.ev
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
:
The dependent evaluation natural transformation as the counit of the adjunction.
Instances For
def
CategoryTheory.ExponentiableMorphism.coev
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
:
The dependent coevaluation natural transformation as the unit of the adjunction.
Instances For
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.ev_def
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
:
ev f = (pullbackPushforwardAdj f).counit
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.coev_def
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
:
coev f = (pullbackPushforwardAdj f).unit
theorem
CategoryTheory.ExponentiableMorphism.ev_naturality
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X Y : Over I}
(g : X ⟶ Y)
:
CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map ((pushforward f).map g)) ((ev f).app Y) = CategoryStruct.comp ((ev f).app X) g
theorem
CategoryTheory.ExponentiableMorphism.ev_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X Y : Over I}
(g : X ⟶ Y)
{Z : Over I}
(h : Y ⟶ Z)
:
CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map ((pushforward f).map g))
(CategoryStruct.comp ((ev f).app Y) h) = CategoryStruct.comp ((ev f).app X) (CategoryStruct.comp g h)
theorem
CategoryTheory.ExponentiableMorphism.coev_naturality
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X Y : Over J}
(g : X ⟶ Y)
:
CategoryStruct.comp g ((coev f).app Y) = CategoryStruct.comp ((coev f).app X) ((pushforward f).map ((ChosenPullbacksAlong.pullback f).map g))
theorem
CategoryTheory.ExponentiableMorphism.coev_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X Y : Over J}
(g : X ⟶ Y)
{Z : Over J}
(h : (pushforward f).obj ((ChosenPullbacksAlong.pullback f).obj Y) ⟶ Z)
:
CategoryStruct.comp g (CategoryStruct.comp ((coev f).app Y) h) = CategoryStruct.comp ((coev f).app X)
(CategoryStruct.comp ((pushforward f).map ((ChosenPullbacksAlong.pullback f).map g)) h)
theorem
CategoryTheory.ExponentiableMorphism.ev_coev
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
(X : Over J)
:
CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map ((coev f).app X))
((ev f).app ((ChosenPullbacksAlong.pullback f).obj X)) = CategoryStruct.id ((ChosenPullbacksAlong.pullback f).obj X)
The first triangle identity for the counit and unit of the adjunction.
theorem
CategoryTheory.ExponentiableMorphism.ev_coev_assoc
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
(X : Over J)
{Z : Over I}
(h : (ChosenPullbacksAlong.pullback f).obj X ⟶ Z)
:
CategoryStruct.comp ((ChosenPullbacksAlong.pullback f).map ((coev f).app X))
(CategoryStruct.comp ((ev f).app ((ChosenPullbacksAlong.pullback f).obj X)) h) = h
The first triangle identity for the counit and unit of the adjunction.
theorem
CategoryTheory.ExponentiableMorphism.coev_ev
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
(Y : Over I)
:
CategoryStruct.comp ((coev f).app ((pushforward f).obj Y)) ((pushforward f).map ((ev f).app Y)) = CategoryStruct.id ((pushforward f).obj Y)
The second triangle identity for the counit and unit of the adjunction.
theorem
CategoryTheory.ExponentiableMorphism.coev_ev_assoc
{C : Type u}
[Category.{v, u} C]
{I J : C}
(f : I ⟶ J)
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
(Y : Over I)
{Z : Over J}
(h : (pushforward f).obj Y ⟶ Z)
:
CategoryStruct.comp ((coev f).app ((pushforward f).obj Y))
(CategoryStruct.comp ((pushforward f).map ((ev f).app Y)) h) = h
The second triangle identity for the counit and unit of the adjunction.
def
CategoryTheory.ExponentiableMorphism.pushforwardCurry
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(u : (ChosenPullbacksAlong.pullback f).obj A ⟶ X)
:
The currying of (pullback f).obj A ⟶ X in Over I to a morphism A ⟶ (pushforward f).obj X
in Over J.
Instances For
def
CategoryTheory.ExponentiableMorphism.pushforwardUncurry
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(v : A ⟶ (pushforward f).obj X)
:
The uncurrying of A ⟶ (pushforward f).obj X in Over J to a morphism
(Over.pullback f).obj A ⟶ X in Over I.
Instances For
theorem
CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(u : (ChosenPullbacksAlong.pullback f).obj A ⟶ X)
:
((pullbackPushforwardAdj f).homEquiv A X) u = pushforwardCurry u
theorem
CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(v : A ⟶ (pushforward f).obj X)
:
((pullbackPushforwardAdj f).homEquiv A X).symm v = pushforwardUncurry v
theorem
CategoryTheory.ExponentiableMorphism.pushforward_uncurry_curry
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(u : (ChosenPullbacksAlong.pullback f).obj A ⟶ X)
:
pushforwardUncurry (pushforwardCurry u) = u
theorem
CategoryTheory.ExponentiableMorphism.pushforward_curry_uncurry
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
{X : Over I}
{A : Over J}
(v : A ⟶ (pushforward f).obj X)
:
pushforwardCurry (pushforwardUncurry v) = v
@[implicit_reducible]
instance
CategoryTheory.ExponentiableMorphism.instChosenPullbacksAlongHomDiscretePUnitMk
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
:
@[implicit_reducible]
instance
CategoryTheory.ExponentiableMorphism.OverMkHom
{C : Type u}
[Category.{v, u} C]
{I J : C}
{f : I ⟶ J}
[ChosenPullbacksAlong f]
[ExponentiableMorphism f]
:
@[implicit_reducible]
def
CategoryTheory.ExponentiableMorphism.id
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
:
The identity morphisms 𝟙 _ are exponentiable.
Instances For
theorem
CategoryTheory.ExponentiableMorphism.id_pushforward
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
:
pushforward (CategoryStruct.id I) = Functor.id (Over I)
def
CategoryTheory.ExponentiableMorphism.pushforwardId
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
[ExponentiableMorphism (CategoryStruct.id I)]
:
Any pushforward of the identity morphism is naturally isomorphic to the identity functor.
Instances For
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
[ExponentiableMorphism (CategoryStruct.id I)]
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
[ExponentiableMorphism (CategoryStruct.id I)]
{Z : Functor (Over I) (Over I)}
(h : (ChosenPullbacksAlong.pullback (CategoryStruct.id I)).comp (Functor.id (Over I)) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
[ExponentiableMorphism (CategoryStruct.id I)]
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc
{C : Type u}
[Category.{v, u} C]
(I : C)
[ChosenPullbacksAlong (CategoryStruct.id I)]
[ExponentiableMorphism (CategoryStruct.id I)]
{Z : Functor (Over I) (Over I)}
(h : Functor.id (Over I) ⟶ Z)
:
@[implicit_reducible]
def
CategoryTheory.ExponentiableMorphism.comp
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
:
The composition of exponentiable morphisms is exponentiable.
Instances For
theorem
CategoryTheory.ExponentiableMorphism.comp_pushforward
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
:
pushforward (CategoryStruct.comp f g) = (pushforward f).comp (pushforward g)
def
CategoryTheory.ExponentiableMorphism.pushforwardComp
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
[ExponentiableMorphism (CategoryStruct.comp f g)]
:
The natural isomorphism between pushforward of the composition and the composition of pushforward functors.
Instances For
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
[ExponentiableMorphism (CategoryStruct.comp f g)]
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
[ExponentiableMorphism (CategoryStruct.comp f g)]
{Z : Functor (Over K) (Over K)}
(h : (ChosenPullbacksAlong.pullback (CategoryStruct.comp f g)).comp ((pushforward f).comp (pushforward g)) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
[ExponentiableMorphism (CategoryStruct.comp f g)]
:
@[simp]
theorem
CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc
{C : Type u}
[Category.{v, u} C]
{I J K : C}
(f : I ⟶ J)
(g : J ⟶ K)
[ChosenPullbacksAlong f]
[ChosenPullbacksAlong g]
[ChosenPullbacksAlong (CategoryStruct.comp f g)]
[ExponentiableMorphism f]
[ExponentiableMorphism g]
[ExponentiableMorphism (CategoryStruct.comp f g)]
{Z : Functor (Over I) (Over I)}
(h : Functor.id (Over I) ⟶ Z)
: