Documentation

Mathlib.CategoryTheory.Abelian.Opposite

The opposite of an abelian category is abelian. #

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

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

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

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

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

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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.

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

Equations

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

Equations

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

Equations