Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Over.map

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

A morphism f : X ⟶ Y induces a functor Over X ⥤ Over Y in the obvious way.

Defined in
Mathlib.CategoryTheory.Comma.Over.Basic
Cited by
97 results in Mathlib
Foundations
Depth 27 from the axioms, rests on 139 definitions · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj · cited by 29ChosenPullbacksAlong.mapP…CategoryTheory.GrothendieckTopology.overMapPullback · cited by 19GrothendieckTopology.over…CategoryTheory.MonoOver.map · cited by 12MonoOver.mapCategoryTheory.Over.mapComp · cited by 10Over.mapCompCategoryTheory.presheafHom · cited by 10CategoryTheory.presheafHomCategoryTheory.Over.mapCongr · cited by 9Over.mapCongrCategoryTheory.Over.mapId · cited by 9Over.mapIdCategoryTheory.Over.mapPullbackAdj · cited by 8Over.mapPullbackAdjCategoryTheory.ChosenPullbacksAlong.hom_ext · cited by 5ChosenPullbacksAlong.hom_…CategoryTheory.ChosenPullbacksAlong.fst' · cited by 4ChosenPullbacksAlong.fst'CategoryTheory.ChosenPullbacksAlong.iso · cited by 4ChosenPullbacksAlong.isoCategoryTheory.ChosenPullbacksAlong.lift_fst · cited by 4ChosenPullbacksAlong.lift…CategoryTheory.Over.postAdjunctionRight · cited by 4Over.postAdjunctionRightCategoryTheory.Over.postEquiv · cited by 4Over.postEquivCategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app · cited by 3GrothendieckTopology.over…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorCategoryTheory.Functor.id · cited by 3333Functor.idCategoryTheory.Discrete · cited by 2447CategoryTheory.DiscreteCategoryTheory.Over · cited by 935CategoryTheory.OverCategoryTheory.Discrete.natTrans · cited by 57Discrete.natTransCategoryTheory.Comma.mapRight · cited by 52Comma.mapRightOver.mapCITED BYCITES

Cites8

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

Cited by132

Results whose statement or proof uses this declaration.