Documentation

Mathlib.Algebra.Category.Ring.Limits

The category of (commutative) rings has all limits #

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

The flat sections of a functor into SemiRingCat form a subsemiring of all sections.

Equations
Instances For

    limit.π (F ⋙ forget SemiRingCat) j as a RingHom.

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

      Construction of a limit cone in SemiRingCat. (Internal use only; use the limits API.)

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

        Witness that the limit cone in SemiRingCat is a limit cone. (Internal use only; use the limits API.)

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

          If (F ⋙ forget SemiRingCat).sections is u-small, F has a limit.

          Equations
          • =

          If J is u-small, SemiRingCat.{u} has limits of shape J.

          Equations
          • =

          The forgetful functor from semirings to additive commutative monoids preserves all limits.

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

          The forgetful functor from semirings to monoids preserves all limits.

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

          The forgetful functor from semirings to types preserves all limits.

          Equations
          • One or more equations did not get rendered due to their size.
          @[reducible, inline]
          abbrev CommSemiRingCatMax :
          Type ((max u1 u2) + 1)

          An alias for CommSemiring.{max u v}, to deal with unification issues.

          Equations
          Instances For

            We show that the forgetful functor CommSemiRingCatSemiRingCat creates limits.

            All we need to do is notice that the limit point has a CommSemiring instance available, and then reuse the existing limit.

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

            If (F ⋙ forget CommSemiRingCat).sections is u-small, F has a limit.

            Equations
            • =

            If J is u-small, CommSemiRingCat.{u} has limits of shape J.

            Equations
            • =

            The forgetful functor from rings to semirings preserves all limits.

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

            The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

            Equations
            • One or more equations did not get rendered due to their size.
            @[reducible, inline]
            abbrev RingCatMax :
            Type ((max u1 u2) + 1)

            An alias for RingCat.{max u v}, to deal around unification issues.

            Equations
            Instances For

              The flat sections of a functor into RingCat form a subring of all sections.

              Equations
              Instances For

                We show that the forgetful functor CommRingCatRingCat creates limits.

                All we need to do is notice that the limit point has a Ring instance available, and then reuse the existing limit.

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

                A choice of limit cone for a functor into RingCat. (Generally, you'll just want to use limit F.)

                Equations
                Instances For

                  If (F ⋙ forget RingCat).sections is u-small, F has a limit.

                  Equations
                  • =

                  If J is u-small, RingCat.{u} has limits of shape J.

                  Equations
                  • =

                  The category of rings has all limits.

                  Equations
                  • =

                  The forgetful functor from rings to semirings preserves all limits.

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

                  The forgetful functor from rings to additive commutative groups preserves all limits.

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

                  The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[reducible, inline]
                  abbrev CommRingCatMax :
                  Type ((max u1 u2) + 1)

                  An alias for CommRingCat.{max u v}, to deal around unification issues.

                  Equations
                  Instances For

                    If (F ⋙ forget CommRingCat).sections is u-small, F has a limit.

                    Equations
                    • =

                    If J is u-small, CommRingCat.{u} has limits of shape J.

                    Equations
                    • =

                    The category of commutative rings has all limits.

                    Equations
                    • =

                    The forgetful functor from commutative rings to rings preserves all limits. (That is, the underlying rings could have been computed instead as limits in the category of rings.)

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

                    The forgetful functor from commutative rings to commutative semirings preserves all limits. (That is, the underlying commutative semirings could have been computed instead as limits in the category of commutative semirings.)

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

                    The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

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