Documentation

Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Constructing equalizers from pullbacks and binary products. #

If a category has pullbacks and binary products, then it has equalizers.

TODO: generalize universe

@[reducible, inline]

Define the equalizing object

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define the equalizing morphism

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define the equalizing cone

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

Show the equalizing cone is a limit

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

Any category with pullbacks and binary products, has equalizers.

@[reducible, inline]

Define the equalizing object

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define the equalizing morphism

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define the equalizing cocone

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

Show the equalizing cocone is a colimit

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

Any category with pullbacks and binary products, has equalizers.