The section functor as a right adjoint to the star functor #

We show that if C is cartesian closed then star I : C ⥤ Over I has a right adjoint sectionsFunctor whose object part is the object of sections of X over I.

source

def CategoryTheory.prodIsoTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] (X Y : C) :

X ⨯ Y ≅ MonoidalCategoryStruct.tensorObj X Y

The isomorphism between X ⨯ Y and X ⊗ Y for objects X and Y in C. This is tautological by the definition of the cartesian monoidal structure on C. This isomorphism provides an interface between prod.fst and CartesianMonoidalCategory.fst as well as between prod.map and tensorHom.

Equations

CategoryTheory.prodIsoTensorObj X Y = CategoryTheory.Iso.refl (X ⨯ Y)

Instances For

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y : C} :

CategoryStruct.comp (prodIsoTensorObj X Y).inv Limits.prod.fst = CartesianMonoidalCategory.fst X Y

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (prodIsoTensorObj X Y).inv (CategoryStruct.comp Limits.prod.fst h) = CategoryStruct.comp (CartesianMonoidalCategory.fst X Y) h

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y : C} :

CategoryStruct.comp (prodIsoTensorObj X Y).inv Limits.prod.snd = CartesianMonoidalCategory.snd X Y

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (prodIsoTensorObj X Y).inv (CategoryStruct.comp Limits.prod.snd h) = CategoryStruct.comp (CartesianMonoidalCategory.snd X Y) h

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y : C} :

CategoryStruct.comp (prodIsoTensorObj X Y).hom (CartesianMonoidalCategory.fst X Y) = Limits.prod.fst

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (prodIsoTensorObj X Y).hom (CategoryStruct.comp (CartesianMonoidalCategory.fst X Y) h) = CategoryStruct.comp Limits.prod.fst h

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y : C} :

CategoryStruct.comp (prodIsoTensorObj X Y).hom (CartesianMonoidalCategory.snd X Y) = Limits.prod.snd

source

@[simp]

theorem CategoryTheory.prodIsoTensorObj_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (prodIsoTensorObj X Y).hom (CategoryStruct.comp (CartesianMonoidalCategory.snd X Y) h) = CategoryStruct.comp Limits.prod.snd h

source

@[simp]

theorem CategoryTheory.prodMap_comp_prodIsoTensorObj_hom {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) :

CategoryStruct.comp (Limits.prod.map f g) (prodIsoTensorObj Y W).hom = CategoryStruct.comp (prodIsoTensorObj X Z).hom (MonoidalCategoryStruct.tensorHom f g)

source

@[simp]

theorem CategoryTheory.prodMap_comp_prodIsoTensorObj_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y W ⟶ Z✝) :

CategoryStruct.comp (Limits.prod.map f g) (CategoryStruct.comp (prodIsoTensorObj Y W).hom h) = CategoryStruct.comp (prodIsoTensorObj X Z).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) h)

source

def CategoryTheory.curryId {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] :

⊤_ C ⟶ I ⟹ I

The first leg of a cospan constructing a pullback diagram in C used to define sections .

Equations

CategoryTheory.curryId I = CategoryTheory.CartesianClosed.curry (CategoryTheory.CartesianMonoidalCategory.fst I (⊤_ C))

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.Over.sectionsObj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] (X : Over I) :

Given X : Over I, sectionsObj X is the object of sections of X defined by the following pullback diagram:

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

Equations

X.sectionsObj = CategoryTheory.Limits.pullback (CategoryTheory.curryId I) ((CategoryTheory.exp I).map X.hom)

Instances For

source

def CategoryTheory.Over.sectionsMap {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X X' : Over I} (u : X ⟶ X') :

X.sectionsObj ⟶ X'.sectionsObj

The functoriality of sectionsObj.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Over.sectionsMap_id {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} :

sectionsMap (CategoryStruct.id X) = CategoryStruct.id X.sectionsObj

source

@[simp]

theorem CategoryTheory.Over.sectionsMap_comp {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X X' X'' : Over I} (u : X ⟶ X') (v : X' ⟶ X'') :

sectionsMap (CategoryStruct.comp u v) = CategoryStruct.comp (sectionsMap u) (sectionsMap v)

source

def CategoryTheory.Over.sections {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] :

Functor (Over I) C

The functor mapping an object X in C to the object of sections of X over I.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Over.sections_obj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] (X : Over I) :

(sections I).obj X = X.sectionsObj

source

@[simp]

theorem CategoryTheory.Over.sections_map {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] {X✝ Y✝ : Over I} (u : X✝ ⟶ Y✝) :

(sections I).map u = sectionsMap u

source

def CategoryTheory.Over.sectionsCurryAux {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :

A ⟶ I ⟹ X.left

An auxiliary morphism used to define the currying of a morphism in Over I to a morphism in C. See sectionsCurry.

Equations

CategoryTheory.Over.sectionsCurryAux u = CategoryTheory.CartesianClosed.curry u.left

Instances For

source

def CategoryTheory.Over.sectionsCurry {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :

A ⟶ (sections I).obj X

The currying operation Hom ((star 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] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) :

(star I).obj A ⟶ X

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Over.sections_curry_uncurry {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} {A : C} {v : A ⟶ (sections I).obj X} :

sectionsCurry (sectionsUncurry v) = v

source

@[simp]

theorem CategoryTheory.Over.sections_uncurry_curry {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] {X : Over I} {A : C} {u : (star I).obj A ⟶ X} :

sectionsUncurry (sectionsCurry u) = u

source

def CategoryTheory.Over.coreHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {I : C} [Exponentiable I] :

Adjunction.CoreHomEquiv (star 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

def CategoryTheory.Over.starSectionsAdj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] :

star I ⊣ sections I

The adjunction between the star functor and the sections functor.

Equations

CategoryTheory.Over.starSectionsAdj I = CategoryTheory.Adjunction.mkOfHomEquiv CategoryTheory.Over.coreHomEquiv

Instances For

source

@[simp]

theorem CategoryTheory.Over.starSectionsAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] (X : C) :

(starSectionsAdj I).unit.app X = (coreHomEquiv.homEquiv X ((star I).obj X)) (CategoryStruct.id ((star I).obj X))

source

@[simp]

theorem CategoryTheory.Over.starSectionsAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (I : C) [Exponentiable I] (Y : Over I) :

(starSectionsAdj I).counit.app Y = (coreHomEquiv.homEquiv Y.sectionsObj Y).symm (CategoryStruct.id Y.sectionsObj)

Documentation

Poly.ForMathlib.CategoryTheory.Comma.Over.Sections

The section functor as a right adjoint to the star functor #