Documentation

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Zero objects #

A category "has a zero object" if it has an object which is both initial and terminal. Having a zero object provides zero morphisms, as the unique morphisms factoring through the zero object; see CategoryTheory.Limits.Shapes.ZeroMorphisms.

References #

An object X in a category is a zero object if for every object Y there is a unique morphism to : X → Y and a unique morphism from : Y → X.

This is a characteristic predicate for has_zero_object.

  • unique_to : ∀ (Y : C), Nonempty (Unique (X Y))

    there are unique morphisms to the object

  • unique_from : ∀ (Y : C), Nonempty (Unique (Y X))

    there are unique morphisms from the object

there are unique morphisms to the object

there are unique morphisms from the object

If h : IsZero X, then h.to_ Y is a choice of unique morphism X → Y.

Equations
  • h.to_ Y = default

If h : is_zero X, then h.from_ Y is a choice of unique morphism Y → X.

Equations
  • h.from_ Y = default
theorem CategoryTheory.Limits.IsZero.eq_from {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y X) :
f = h.from_ Y
theorem CategoryTheory.Limits.IsZero.from_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y X) :
h.from_ Y = f
theorem CategoryTheory.Limits.IsZero.eq_of_src {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hX : CategoryTheory.Limits.IsZero X) (f : X Y) (g : X Y) :
f = g
theorem CategoryTheory.Limits.IsZero.eq_of_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hX : CategoryTheory.Limits.IsZero X) (f : Y X) (g : Y X) :
f = g

Any two zero objects are isomorphic.

Equations
  • hX.iso hY = { hom := hX.to_ Y, inv := hX.from_ Y, hom_inv_id := , inv_hom_id := }

The (unique) isomorphism between any initial object and the zero object.

Equations
  • hX.isoIsInitial hY = hX.isInitial.uniqueUpToIso hY

The (unique) isomorphism between any terminal object and the zero object.

Equations
  • hX.isoIsTerminal hY = hX.isTerminal.uniqueUpToIso hY

A category "has a zero object" if it has an object which is both initial and terminal.

Instances

    Construct a Zero C for a category with a zero object. This can not be a global instance as it will trigger for every Zero C typeclass search.

    Equations

    Every zero object is isomorphic to the zero object.

    Equations
    • hX.isoZero = hX.iso

    There is a unique morphism from the zero object to any object X.

    Equations

    There is a unique morphism from any object X to the zero object.

    Equations

    A zero object is in particular initial.

    Equations
    • CategoryTheory.Limits.HasZeroObject.zeroIsInitial = .isInitial

    A zero object is in particular terminal.

    Equations
    • CategoryTheory.Limits.HasZeroObject.zeroIsTerminal = .isTerminal
    @[instance 10]

    A zero object is in particular initial.

    Equations
    • =
    @[instance 10]

    A zero object is in particular terminal.

    Equations
    • =

    The (unique) isomorphism between any initial object and the zero object.

    Equations

    The (unique) isomorphism between any terminal object and the zero object.

    Equations

    The (unique) isomorphism between the chosen initial object and the chosen zero object.

    Equations
    • CategoryTheory.Limits.HasZeroObject.zeroIsoInitial = CategoryTheory.Limits.HasZeroObject.zeroIsInitial.uniqueUpToIso CategoryTheory.Limits.initialIsInitial

    The (unique) isomorphism between the chosen terminal object and the chosen zero object.

    Equations
    • CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal = CategoryTheory.Limits.HasZeroObject.zeroIsTerminal.uniqueUpToIso CategoryTheory.Limits.terminalIsTerminal