Theorems · Inductive type · category theory

CategoryTheory.LiftableCone

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.Limits.Cone (K.comp F) → Type (max (max (max u₁ v₁) v₂) w)

Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K which is a lift of c, i.e. the image of it under F is (iso) to c. We will then use this as part of the definition of creation of limits: every limit cone has a lift. Note this definition is really only useful when c is a limit already.

Defined in

Mathlib.CategoryTheory.Limits.Creates

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category