Documentation

Mathlib.CategoryTheory.Monoidal.CommGrp_

The category of commutative groups in a cartesian monoidal category #

A commutative group object internal to a cartesian monoidal category.

Instances For

    The trivial commutative group object.

    Equations
    Instances For

      The forgetful functor from commutative group objects to the ambient category.

      Equations
      Instances For

        A finite-product-preserving functor takes commutative group objects to commutative group objects.

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

          The identity functor is also the identity on commutative group objects.

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

            Natural transformations between functors lift to commutative group objects.

            Equations
            Instances For

              Natural isomorphisms between functors lift to commutative group objects.

              Equations
              Instances For

                mapCommGrp is functorial in the left-exact functor.

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

                  An adjunction of braided functors lifts to an adjunction of their lifts to commutative group objects.

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

                    An equivalence of categories lifts to an equivalence of their commutative group objects.

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