Documentation

Mathlib.CategoryTheory.Abelian.Opposite

The opposite of an abelian category is abelian. #

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

Instances For

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

    Instances For

      The kernel of g.unop is the opposite of cokernel g.

      Instances For

        The cokernel of g.unop is the opposite of kernel g.

        Instances For

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

          Instances For

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

            Instances For

              The kernel of g.unop is the opposite of cokernel g.

              Instances For

                The cokernel of g.unop is the opposite of kernel g.

                Instances For

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

                  Instances For

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

                    Instances For

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

                      Instances For

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

                        Instances For