Adjunctions related to the over category #
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.
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
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.
Instances For
The adjunction Over.map ⊣ baseChange
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
- ⋯ = ⋯
Alias of CategoryTheory.Over.star
.
The functor from C
to Over X
which sends Y : C
to π₁ : X ⨯ Y ⟶ X
, sometimes denoted X*
.
Instances For
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 ⨯ -
.