Theorems · Theorem · category theory

CategoryTheory.PreservesFiniteLimitsOfFlat.fac

∀ {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] [inst_3 : CategoryTheory.FinCategory J]
  {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.RepresentablyFlat F]
  {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (K.comp F))
  (x : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesFiniteLimitsOfFlat.lift F hc s) ((F.mapCone c).π.app x) =
    s.π.app x

Defined in

Mathlib.CategoryTheory.Functor.Flat

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.FinCategoryCategoryTheory.RepresentablyFlat