Theorems · Definition · category theory

CategoryTheory.comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} J] →
            (R : CategoryTheory.Functor D C) →
              [CategoryTheory.ComonadicLeftAdjoint R] →
                [CategoryTheory.Limits.PreservesLimitsOfShape J R] → CategoryTheory.CreatesLimitsOfShape J R

A comonadic functor creates any limits of shapes it preserves.

Defined in

Mathlib.CategoryTheory.Monad.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.ComonadicLeftAdjointCategoryTheory.Limits.PreservesLimitsOfShape