Documentation

Mathlib.CategoryTheory.Adjunction.Over

Construct the left adjoint star X to Over.forget X : Over X ⥤ C.

TODO #

Show star X itself has a left adjoint provided C is locally cartesian closed.

@[simp]

theorem CategoryTheory.Over.baseChange_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) :

∀ {X_1 Y_1 : CategoryTheory.Over Y} (i : X_1 ⟶ Y_1), ((CategoryTheory.Over.baseChange f).map i).left = CategoryTheory.Limits.pullback.map X_1.hom f Y_1.hom f i.left (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯

@[simp]

theorem CategoryTheory.Over.baseChange_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Over Y) :

((CategoryTheory.Over.baseChange f).obj g).hom = CategoryTheory.Limits.pullback.snd

@[simp]

theorem CategoryTheory.Over.baseChange_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Over Y) :

((CategoryTheory.Over.baseChange f).obj g).left = CategoryTheory.Limits.pullback g.hom f

def CategoryTheory.Over.baseChange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)

Given a morphism f : X ⟶ Y, the functor baseChange f takes morphisms over Y to morphisms over X via pullbacks.

Equations

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

Instances For

@[deprecated CategoryTheory.Over.baseChange]

def CategoryTheory.Over.Limits.baseChange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)

Alias of CategoryTheory.Over.baseChange.

Given a morphism f : X ⟶ Y, the functor baseChange f takes morphisms over Y to morphisms over X via pullbacks.

Equations

@CategoryTheory.Over.Limits.baseChange = @CategoryTheory.Over.baseChange

Instances For

@[simp]

theorem CategoryTheory.Over.mapAdjunction_unit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X✝ ⟶ Y) (X : CategoryTheory.Over X✝) :

(CategoryTheory.Over.mapAdjunction f).unit.app X = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X.left) X.hom ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.mapAdjunction_counit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y✝) (Y : CategoryTheory.Over Y✝) :

(CategoryTheory.Over.mapAdjunction f).counit.app Y = CategoryTheory.Over.homMk CategoryTheory.Limits.pullback.fst ⋯

def CategoryTheory.Over.mapAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.Over.map f ⊣ CategoryTheory.Over.baseChange f

The adjunction Over.map ⊣ baseChange

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Over.star_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

∀ {X_1 Y : C} (f : X_1 ⟶ Y), ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.Over.star_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :

((CategoryTheory.Over.star X✝).obj X).hom = CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.Over.star_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :

((CategoryTheory.Over.star X✝).obj X).left = (X✝ ⨯ X)

def CategoryTheory.Over.star {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

CategoryTheory.Functor C (CategoryTheory.Over X)

The functor from C to Over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.

Equations

CategoryTheory.Over.star X = (CategoryTheory.prodComonad X).cofree.comp (CategoryTheory.coalgebraToOver X)

Instances For

def CategoryTheory.Over.forgetAdjStar {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

CategoryTheory.Over.forget X ⊣ CategoryTheory.Over.star X

The functor Over.forget X : Over X ⥤ C has a right adjoint given by star X.

Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

Equations

CategoryTheory.Over.forgetAdjStar X = (CategoryTheory.coalgebraEquivOver X).symm.toAdjunction.comp (CategoryTheory.prodComonad X).adj

Instances For

instance CategoryTheory.Over.instIsLeftAdjointForgetOfHasBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

(CategoryTheory.Over.forget X).IsLeftAdjoint

Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

Equations

⋯ = ⋯

@[deprecated CategoryTheory.Over.star]

def CategoryTheory.star {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

CategoryTheory.Functor C (CategoryTheory.Over X)

Alias of CategoryTheory.Over.star.

The functor from C to Over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.

Equations

@CategoryTheory.star = @CategoryTheory.Over.star

Instances For

@[deprecated CategoryTheory.Over.forgetAdjStar]

def CategoryTheory.forgetAdjStar {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] :

CategoryTheory.Over.forget X ⊣ CategoryTheory.Over.star X

Alias of CategoryTheory.Over.forgetAdjStar.

The functor Over.forget X : Over X ⥤ C has a right adjoint given by star X.

Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

Equations

@CategoryTheory.forgetAdjStar = @CategoryTheory.Over.forgetAdjStar

Instances For