Documentation

Mathlib.Algebra.Category.Ring.FilteredColimits

The forgetful functor from (commutative) (semi-) rings preserves filtered colimits. #

Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.

In this file, we start with a small filtered category J and a functor F : J ⥤ SemiRingCatMax. We show that the colimit of F ⋙ forget₂ SemiRingCatMax MonCat (in MonCat) carries the structure of a semiring, thereby showing that the forgetful functor forget₂ SemiRingCatMax MonCat preserves filtered colimits. In particular, this implies that forget SemiRingCatMax preserves filtered colimits. Similarly for CommSemiRingCat, RingCat and CommRingCat.

@[reducible, inline]

The colimit of F ⋙ forget₂ SemiRingCat MonCat in the category MonCat. In the following, we will show that this has the structure of a semiring.

Equations
Instances For

    The cocone over the proposed colimit semiring.

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

      The proposed colimit cocone is a colimit in SemiRingCat.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]

        The colimit of F ⋙ forget₂ CommSemiRingCat SemiRingCat in the category SemiRingCat. In the following, we will show that this has the structure of a commutative semiring.

        Equations
        Instances For

          The cocone over the proposed colimit commutative semiring.

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

            The proposed colimit cocone is a colimit in CommSemiRingCat.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[reducible, inline]

              The colimit of F ⋙ forget₂ RingCat SemiRingCat in the category SemiRingCat. In the following, we will show that this has the structure of a ring.

              Equations
              Instances For

                The cocone over the proposed colimit ring.

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

                  The proposed colimit cocone is a colimit in Ring.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible, inline]

                    The colimit of F ⋙ forget₂ CommRingCat RingCat in the category RingCat. In the following, we will show that this has the structure of a commutative ring.

                    Equations
                    Instances For

                      The cocone over the proposed colimit commutative ring.

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

                        The proposed colimit cocone is a colimit in CommRingCat.

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