Theorems · Definition · category theory

CategoryTheory.Limits.limMap

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F G : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            [inst_3 : CategoryTheory.Limits.HasLimit G] →
              (F ⟶ G) → (CategoryTheory.Limits.limit F ⟶ CategoryTheory.Limits.limit G)

Functoriality of limits. Usually this morphism should be accessed through lim.map, but may be needed separately when you have specified limits for the source and target functors, but not necessarily for all functors of shape J.

Defined in

Mathlib.CategoryTheory.Limits.HasLimits

Cited by

29 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitCategoryTheory.Limits.HasLimit