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.

Instances For

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

    Instances For

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

      Instances For
        @[inline, reducible]
        abbrev CommSemiRingCatMax :
        Type ((max u1 u2) + 1)

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

        Instances For

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

          Instances For

            The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

            Instances For

              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.)

              @[inline, reducible]
              abbrev RingCatMax :
              Type ((max u1 u2) + 1)

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

              Instances For

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

                Instances For

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

                  Instances For

                    The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

                    Instances For

                      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.)

                      @[inline, reducible]
                      abbrev CommRingCatMax :
                      Type ((max u1 u2) + 1)

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

                      Instances For

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

                        Instances For

                          The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

                          Instances For

                            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.)

                            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.)

                            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.)