Theorems · Definition · category theory

CategoryTheory.PreservesFiniteLimitsOfFlat.lift

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type v₁} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            [CategoryTheory.FinCategory J] →
              {K : CategoryTheory.Functor J C} →
                (F : CategoryTheory.Functor C D) →
                  [CategoryTheory.RepresentablyFlat F] →
                    {c : CategoryTheory.Limits.Cone K} →
                      CategoryTheory.Limits.IsLimit c → (s : CategoryTheory.Limits.Cone (K.comp F)) → s.pt ⟶ F.obj c.pt

(Implementation). Given a limit cone c : cone K and a cone s : cone (K ⋙ F) with F representably flat, s can factor through F.mapCone c.

Defined in

Mathlib.CategoryTheory.Functor.Flat

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.FinCategoryCategoryTheory.RepresentablyFlat