Documentation

Mathlib.CategoryTheory.Filtered.Small

A functor from a small category to a filtered category factors through a small filtered category #

A consequence of this is that if C is filtered and finally small, then C is also "finally filtered-small", i.e., there is a final functor from a small filtered category to C. This is occasionally useful, for example in the proof of the recognition theorem for ind-objects (Proposition 6.1.5 in [Kashiwara2006]).

inductive CategoryTheory.IsFiltered.FilteredClosure {C : Type u} [Category.{v, u} C] [IsFilteredOrEmpty C] {α : Type w} (f : αC) :
CProp

The "filtered closure" of an α-indexed family of objects in C is the set of objects in C obtained by starting with the family and successively adding maxima and coequalizers.

Instances For

    The full subcategory induced by the filtered closure of a family of objects is filtered.

    Our goal for this section is to show that the size of the filtered closure of an α-indexed family of objects in C only depends on the size of α and the morphism types of C, not on the size of the objects of C. More precisely, if α lives in Type w, the objects of C live in Type u and the morphisms of C live in Type v, then we want Small.{max v w} (FullSubcategory (FilteredClosure f)).

    The strategy is to define a type `AbstractFilteredClosure` which should be an inductive type
    similar to `FilteredClosure`, which lives in the correct universe and surjects onto the full
    subcategory. The difficulty with this is that we need to define it at the same time as the map
    `AbstractFilteredClosure → C`, as the coequalizer constructor depends on the actual morphisms
    in `C`. This would require some kind of inductive-recursive definition, which Lean does not
    allow. Our solution is to define a function `ℕ → Σ t : Type (max v w), t → C` by (strong)
    induction and then take the union over all natural numbers, mimicking what one would do in a
    set-theoretic setting. 
    

    Every functor from a small category to a filtered category factors fully faithfully through a small filtered category. This is that category.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The first part of a factoring of a functor from a small category to a filtered category through a small filtered category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The second, fully faithful part of a factoring of a functor from a small category to a filtered category through a small filtered category.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The factorization through a small filtered category is in fact a factorization, up to natural isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            inductive CategoryTheory.IsCofiltered.CofilteredClosure {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty C] {α : Type w} (f : αC) :
            CProp

            The "cofiltered closure" of an α-indexed family of objects in C is the set of objects in C obtained by starting with the family and successively adding minima and equalizers.

            Instances For

              The full subcategory induced by the cofiltered closure of a family is cofiltered.

              Every functor from a small category to a cofiltered category factors fully faithfully through a small cofiltered category. This is that category.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The first part of a factoring of a functor from a small category to a cofiltered category through a small filtered category.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The second, fully faithful part of a factoring of a functor from a small category to a filtered category through a small filtered category.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The factorization through a small filtered category is in fact a factorization, up to natural isomorphism.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For