Documentation

Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

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.

source
@[reducible, inline]
abbrev CategoryTheory.curryRightUnitorHom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (I : C) [Closed I] :
MonoidalCategoryStruct.tensorUnit C ⟶ (ihom I).obj I

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

Equations
Instances For
    source
    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)
    source
    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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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 ((ihom I).obj ((Functor.fromPUnit I).obj X✝.right))) ⋯ ⋯
      source
      @[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)
      source
      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).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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
          source
          @[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
          source
          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`.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[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 := ⋯ }
            source
            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.

            Equations
            Instances For
              source
              @[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))
              source
              @[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)))