Documentation

Mathlib.CategoryTheory.Abelian.Opposite

The opposite of an abelian category is abelian. #

The kernel of f.op is the opposite of cokernel f.

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

    The cokernel of f.op is the opposite of kernel f.

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

      The kernel of f.op is the opposite of cokernel f.

      Equations
      Instances For

        The cokernel of f.op is the opposite of kernel f.

        Equations
        Instances For

          The opposite of the image of g.unop is the image of g.

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

            The opposite of the image of f is the image of f.op.

            Equations
            Instances For

              The image of f.op is the opposite of the image of f.

              Equations
              Instances For

                The image of g is the opposite of the image of g.unop.

                Equations
                Instances For