Documentation

Mathlib.CategoryTheory.Limits.Preserves.Filtered

Preservation of filtered colimits and cofiltered limits. #

Typically forgetful functors from algebraic categories preserve filtered colimits (although not general colimits). See e.g. Algebra/Category/MonCat/FilteredColimits.

PreservesFilteredColimitsOfSize.{w', w} F means that F sends all colimit cocones over any filtered diagram J ⥤ C to colimit cocones, where J : Type w with [Category.{w'} J].

Instances
    @[reducible, inline]

    A functor is said to preserve filtered colimits, if it preserves all colimits of shape J, where J is a filtered category which is small relative to the universe in which morphisms of the source live.

    Equations
    Instances For

      PreservesFilteredColimitsOfSize_shrink.{w, w'} F tries to obtain PreservesFilteredColimitsOfSize.{w, w'} F from some other PreservesFilteredColimitsOfSize F.

      ReflectsFilteredColimitsOfSize.{w', w} F means that whenever the image of a filtered cocone under F is a colimit cocone, the original cocone was already a colimit.

      Instances
        @[reducible, inline]

        A functor is said to reflect filtered colimits, if it reflects all colimits of shape J, where J is a filtered category which is small relative to the universe in which morphisms of the source live.

        Equations
        Instances For

          ReflectsFilteredColimitsOfSize_shrink.{w, w'} F tries to obtain ReflectsFilteredColimitsOfSize.{w, w'} F from some other ReflectsFilteredColimitsOfSize F.

          PreservesCofilteredLimitsOfSize.{w', w} F means that F sends all limit cones over any cofiltered diagram J ⥤ C to limit cones, where J : Type w with [Category.{w'} J].

          Instances
            @[reducible, inline]

            A functor is said to preserve cofiltered limits, if it preserves all limits of shape J, where J is a cofiltered category which is small relative to the universe in which morphisms of the source live.

            Equations
            Instances For

              PreservesCofilteredLimitsOfSizeShrink.{w, w'} F tries to obtain PreservesCofilteredLimitsOfSize.{w, w'} F from some other PreservesCofilteredLimitsOfSize F.

              ReflectsCofilteredLimitsOfSize.{w', w} F means that whenever the image of a cofiltered cone under F is a limit cone, the original cone was already a limit.

              Instances
                @[reducible, inline]

                A functor is said to reflect cofiltered limits, if it reflects all limits of shape J, where J is a cofiltered category which is small relative to the universe in which morphisms of the source live.

                Equations
                Instances For

                  ReflectsCofilteredLimitsOfSize_shrink.{w, w'} F tries to obtain ReflectsCofilteredLimitsOfSize.{w, w'} F from some other ReflectsCofilteredLimitsOfSize F.