The section functor as a right adjoint to the toOver functor

We show that in a cartesian monoidal category C, for any exponentiable object I, the functor toOver I : C ⥤ Over I mapping an object X to the projection snd : X ⊗ I ⟶ I in Over I has a right adjoint sections I : Over I ⥤ C whose object part is the object of sections of X over I.

In particular, if C is cartesian closed, then for all objects I in C, toOver I : C ⥤ Over I has a right adjoint.

@[reducible, inline]

abbrev CategoryTheory.curryRightUnitorHom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] : MonoidalCategoryStruct.tensorUnit C ⟶ I ⟹ I

The first leg of a cospan to define sectionsObj as a pullback in C.

theorem CategoryTheory.toUnit_comp_curryRightUnitorHom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {I : C} [Closed I] {A : C} : CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (curryRightUnitorHom I) = MonoidalClosed.curry (SemiCartesianMonoidalCategory.fst I A)

def CategoryTheory.Over.sections {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] : Functor (Over I) C

The functor mapping an object X : Over I to the object of sections of X over I, defined by the following pullback diagram. The functor's mapping of morphisms is induced by pullbackMap, that is by the universal property of chosen pullbacks.

 sections X -->  I ⟹ X
   |               |
   |               |
   v               v
  𝟙_ C   ----->  I ⟹ I

@[simp]

theorem CategoryTheory.Over.sections_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] {X✝ Y✝ : Over I} (u : X✝ ⟶ Y✝) : (sections I).map u = ChosenPullbacksAlong.pullbackMap ((ihom I).map Y✝.hom) (curryRightUnitorHom I) ((ihom I).map X✝.hom) (curryRightUnitorHom I) ((ihom I).map u.left) (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.id (I ⟹ (Functor.fromPUnit I).obj X✝.right)) ⋯ ⋯

@[simp]

theorem CategoryTheory.Over.sections_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] (X : Over I) : (sections I).obj X = ChosenPullbacksAlong.pullbackObj ((ihom I).map X.hom) (curryRightUnitorHom I)

def CategoryTheory.Over.sectionsCurry {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {I : C} [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] {X : Over I} {A : C} (u : (toOver I).obj A ⟶ X) : A ⟶ (sections I).obj X

The currying operation Hom ((toOver I).obj A) X → Hom A (I ⟹ X.left).

def CategoryTheory.Over.sectionsUncurry {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {I : C} [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) : (toOver I).obj A ⟶ X

The uncurrying operation Hom A (section X) → Hom ((toOver I).obj A) X.

@[simp]

theorem CategoryTheory.Over.sectionsCurry_sectionUncurry {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {I : C} [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] {X : Over I} {A : C} {v : A ⟶ (sections I).obj X} : sectionsCurry (sectionsUncurry v) = v

@[simp]

theorem CategoryTheory.Over.sectionsUncurry_sectionsCurry {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {I : C} [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] {X : Over I} {A : C} {u : (toOver I).obj A ⟶ X} : sectionsUncurry (sectionsCurry u) = u

def CategoryTheory.Over.coreHomEquivToOverSections {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] : Adjunction.CoreHomEquiv (toOver I) (sections I)

An auxiliary definition which is used to define the adjunction between the star functor and the sections functor. See starSectionsAdjunction.

@[simp]

theorem CategoryTheory.Over.coreHomEquivToOverSections_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] (A : C) (X : Over I) : (coreHomEquivToOverSections I).homEquiv A X = { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }

def CategoryTheory.Over.toOverSectionsAdj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] : toOver I ⊣ sections I

The adjunction between the toOver functor and the sections functor.

@[simp]

theorem CategoryTheory.Over.toOverSectionsAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] (X : C) : (toOverSectionsAdj I).unit.app X = sectionsCurry (CategoryStruct.id ((toOver I).obj X))

@[simp]

theorem CategoryTheory.Over.toOverSectionsAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] [ChosenPullbacksAlong (curryRightUnitorHom I)] [BraidedCategory C] (Y : Over I) : (toOverSectionsAdj I).counit.app Y = sectionsUncurry (CategoryStruct.id (ChosenPullbacksAlong.pullbackObj ((ihom I).map Y.hom) (curryRightUnitorHom I)))