Mathlib Map

Theorems · Definition · category theory

CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {I J : C} →
      (f : I ⟶ J) →
        {inst_1 : CategoryTheory.ChosenPullbacksAlong f} →
          [self : CategoryTheory.ExponentiableMorphism f] →
            CategoryTheory.ChosenPullbacksAlong.pullback f ⊣ CategoryTheory.ExponentiableMorphism.pushforward f

The pushforward functor is right adjoint to the pullback functor

Defined in
Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Cited by
16 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.ExponentiableMorphism
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.ExponentiableMorphism.coev · cited by 7ExponentiableMorphism.coevCategoryTheory.ExponentiableMorphism.ev · cited by 7ExponentiableMorphism.evCategoryTheory.ExponentiableMorphism.comp · cited by 5ExponentiableMorphism.compCategoryTheory.ExponentiableMorphism.pushforwardComp · cited by 4ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.pushforwardId · cited by 4ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.pushforwardCurry · cited by 3ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.pushforwardUncurry · cited by 3ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit · cited by 1ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit · cited by 1ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom · cited by 1ExponentiableMorphism.uni…CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom · cited by 1ExponentiableMorphism.uni…CategoryTheory.ExponentiableMorphism.coev_ev · cited by 1ExponentiableMorphism.coe…CategoryTheory.ExponentiableMorphism.ev_coev · cited by 1ExponentiableMorphism.ev_…CategoryTheory.ExponentiableMorphism.ev_def · cited by 0ExponentiableMorphism.ev_…CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq · cited by 0ExponentiableMorphism.hom…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Over · cited by 935CategoryTheory.OverCategoryTheory.Adjunction · cited by 524CategoryTheory.AdjunctionCategoryTheory.ChosenPullbacksAlong · cited by 73CategoryTheory.ChosenPull…CategoryTheory.ChosenPullbacksAlong.pullback · cited by 62ChosenPullbacksAlong.pull…CategoryTheory.ExponentiableMorphism.pushforward · cited by 23ExponentiableMorphism.pus…CategoryTheory.ExponentiableMorphism · cited by 23CategoryTheory.Exponentia…ExponentiableMorphism.pullbac…CITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by23

Results whose statement or proof uses this declaration.