Mathlib Map

Theorems · Definition · category theory

CategoryTheory.toOver

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.CartesianMonoidalCategory C] → (X : C) → CategoryTheory.Functor C (CategoryTheory.Over X)

The functor which maps an object A in C to the projection A ⊗ X ⟶ X in Over X. This is the computable analogue of the functor Over.star.

Defined in
Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Cited by
18 results in Mathlib
Foundations
Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategory
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.forgetAdjToOver · cited by 7CategoryTheory.forgetAdjT…CategoryTheory.Over.sectionsUncurry · cited by 5Over.sectionsUncurryCategoryTheory.Over.sectionsCurry · cited by 4Over.sectionsCurryCategoryTheory.toOver_map · cited by 3CategoryTheory.toOver_mapCategoryTheory.toOverUnitPullback · cited by 2CategoryTheory.toOverUnit…CategoryTheory.Over.sectionsUncurry_sectionsCurry · cited by 2Over.sectionsUncurry_sect…CategoryTheory.Over.toOverSectionsAdj · cited by 2Over.toOverSectionsAdjCategoryTheory.toOverIsoToOverUnit · cited by 2CategoryTheory.toOverIsoT…CategoryTheory.toOverIteratedSliceForwardIsoPullback · cited by 2CategoryTheory.toOverIter…CategoryTheory.toOverPullbackIsoToOver · cited by 2CategoryTheory.toOverPull…CategoryTheory.forgetAdjToOver_counit_app · cited by 1CategoryTheory.forgetAdjT…CategoryTheory.Over.coreHomEquivToOverSections · cited by 1Over.coreHomEquivToOverSe…CategoryTheory.toOverUnitPullback_hom_app_left · cited by 0CategoryTheory.toOverUnit…CategoryTheory.toOverUnitPullback_inv_app_left · cited by 0CategoryTheory.toOverUnit…CategoryTheory.forgetAdjToOver.homEquiv_symm · cited by 0forgetAdjToOver.homEquiv_…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorCategoryTheory.CartesianMonoidalCategory · cited by 947CategoryTheory.CartesianM…CategoryTheory.Over · cited by 935CategoryTheory.OverCategoryTheory.MonoidalCategoryStruct.whiskerRight · cited by 903MonoidalCategoryStruct.wh…CategoryTheory.Over.mk · cited by 203Over.mkCategoryTheory.SemiCartesianMonoidalCategory.snd · cited by 181SemiCartesianMonoidalCate…CategoryTheory.Over.homMk · cited by 115Over.homMkCategoryTheory.toOverCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by27

Results whose statement or proof uses this declaration.