category_theory.limits.shapes.zero_objects

structure category_theory.limits.is_zero {C : Type u} [category_theory.category C] (X : C) :

Prop

unique_to : ∀ (Y : C), nonempty (unique (X ⟶ Y))
unique_from : ∀ (Y : C), nonempty (unique (Y ⟶ X))

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.

source

@[protected]

noncomputable def category_theory.limits.is_zero.to {C : Type u} [category_theory.category C] {X : C} (h : category_theory.limits.is_zero X) (Y : C) :

X ⟶ Y

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

Equations

h.to Y = inhabited.default

source

theorem category_theory.limits.is_zero.eq_to {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_zero X) (f : X ⟶ Y) :

f = h.to Y

source

theorem category_theory.limits.is_zero.to_eq {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_zero X) (f : X ⟶ Y) :

h.to Y = f

source

@[protected]

noncomputable def category_theory.limits.is_zero.from {C : Type u} [category_theory.category C] {X : C} (h : category_theory.limits.is_zero X) (Y : C) :

Y ⟶ X

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

Equations

h.from Y = inhabited.default

source

theorem category_theory.limits.is_zero.eq_from {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_zero X) (f : Y ⟶ X) :

f = h.from Y

source

theorem category_theory.limits.is_zero.from_eq {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_zero X) (f : Y ⟶ X) :

h.from Y = f

source

theorem category_theory.limits.is_zero.eq_of_src {C : Type u} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_zero X) (f g : X ⟶ Y) :

f = g

source

theorem category_theory.limits.is_zero.eq_of_tgt {C : Type u} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_zero X) (f g : Y ⟶ X) :

f = g

source

noncomputable def category_theory.limits.is_zero.iso {C : Type u} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_zero X) (hY : category_theory.limits.is_zero Y) :

X ≅ Y

Any two zero objects are isomorphic.

Equations

hX.iso hY = {hom := hX.to Y, inv := hX.from Y, hom_inv_id' := _, inv_hom_id' := _}

source

@[protected]

noncomputable def category_theory.limits.is_zero.is_initial {C : Type u} [category_theory.category C] {X : C} (hX : category_theory.limits.is_zero X) :

category_theory.limits.is_initial X

A zero object is in particular initial.

Equations

hX.is_initial = category_theory.limits.is_initial.of_unique X

source

@[protected]

noncomputable def category_theory.limits.is_zero.is_terminal {C : Type u} [category_theory.category C] {X : C} (hX : category_theory.limits.is_zero X) :

category_theory.limits.is_terminal X

A zero object is in particular terminal.

Equations

hX.is_terminal = category_theory.limits.is_terminal.of_unique X

source

noncomputable def category_theory.limits.is_zero.iso_is_initial {C : Type u} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_zero X) (hY : category_theory.limits.is_initial Y) :

X ≅ Y

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

Equations

hX.iso_is_initial hY = hX.is_initial.unique_up_to_iso hY

source

noncomputable def category_theory.limits.is_zero.iso_is_terminal {C : Type u} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_zero X) (hY : category_theory.limits.is_terminal Y) :

X ≅ Y

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

Equations

hX.iso_is_terminal hY = hX.is_terminal.unique_up_to_iso hY

source

theorem category_theory.limits.is_zero.of_iso {C : Type u} [category_theory.category C] {X Y : C} (hY : category_theory.limits.is_zero Y) (e : X ≅ Y) :

category_theory.limits.is_zero X

source

theorem category_theory.limits.is_zero.op {C : Type u} [category_theory.category C] {X : C} (h : category_theory.limits.is_zero X) :

category_theory.limits.is_zero (opposite.op X)

source

theorem category_theory.limits.is_zero.unop {C : Type u} [category_theory.category C] {X : Cᵒᵖ} (h : category_theory.limits.is_zero X) :

category_theory.limits.is_zero (opposite.unop X)

source

theorem category_theory.iso.is_zero_iff {C : Type u} [category_theory.category C] {X Y : C} (e : X ≅ Y) :

category_theory.limits.is_zero X ↔ category_theory.limits.is_zero Y

source

theorem category_theory.functor.is_zero {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (F : C ⥤ D) (hF : ∀ (X : C), category_theory.limits.is_zero (F.obj X)) :

category_theory.limits.is_zero F

source

@[class]

structure category_theory.limits.has_zero_object (C : Type u) [category_theory.category C] :

Prop

zero : ∃ (X : C), category_theory.limits.is_zero X

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

Instances of this typeclass

source

@[protected, instance]

def category_theory.limits.has_zero_object_punit :

category_theory.limits.has_zero_object (category_theory.discrete punit)

source

@[protected]

noncomputable def category_theory.limits.has_zero_object.has_zero (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] :

has_zero C

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

Equations

category_theory.limits.has_zero_object.has_zero C = {zero := category_theory.limits.has_zero_object.zero.some}

source

theorem category_theory.limits.is_zero_zero (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.is_zero 0

source

@[protected, instance]

def category_theory.limits.has_zero_object_op (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.has_zero_object Cᵒᵖ

source

theorem category_theory.limits.has_zero_object_unop (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object Cᵒᵖ] :

category_theory.limits.has_zero_object C

source

theorem category_theory.limits.is_zero.has_zero_object {C : Type u} [category_theory.category C] {X : C} (hX : category_theory.limits.is_zero X) :

category_theory.limits.has_zero_object C

source

noncomputable def category_theory.limits.is_zero.iso_zero {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (hX : category_theory.limits.is_zero X) :

X ≅ 0

Every zero object is isomorphic to the zero object.

Equations

hX.iso_zero = hX.iso _

source

theorem category_theory.limits.is_zero.obj {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_zero_object D] {F : C ⥤ D} (hF : category_theory.limits.is_zero F) (X : C) :

category_theory.limits.is_zero (F.obj X)

source

@[protected]

noncomputable def category_theory.limits.has_zero_object.unique_to {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] (X : C) :

unique (0 ⟶ X)

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

Equations

category_theory.limits.has_zero_object.unique_to X = _.some

source

@[protected]

noncomputable def category_theory.limits.has_zero_object.unique_from {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] (X : C) :

unique (X ⟶ 0)

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

Equations

category_theory.limits.has_zero_object.unique_from X = _.some

source

@[ext]

theorem category_theory.limits.has_zero_object.to_zero_ext {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (f g : X ⟶ 0) :

f = g

source

@[ext]

theorem category_theory.limits.has_zero_object.from_zero_ext {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (f g : 0 ⟶ X) :

f = g

source

@[protected, instance]

def category_theory.limits.has_zero_object.category_theory.iso.subsingleton {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] (X : C) :

subsingleton (X ≅ 0)

source

@[protected, instance]

def category_theory.limits.has_zero_object.category_theory.mono {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (f : 0 ⟶ X) :

category_theory.mono f

source

@[protected, instance]

def category_theory.limits.has_zero_object.category_theory.epi {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (f : X ⟶ 0) :

category_theory.epi f

source

@[protected, instance]

def category_theory.limits.has_zero_object.zero_to_zero_is_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] (f : 0 ⟶ 0) :

category_theory.is_iso f

source

noncomputable def category_theory.limits.has_zero_object.zero_is_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.is_initial 0

A zero object is in particular initial.

Equations

category_theory.limits.has_zero_object.zero_is_initial = _.is_initial

source

noncomputable def category_theory.limits.has_zero_object.zero_is_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.is_terminal 0

A zero object is in particular terminal.

Equations

category_theory.limits.has_zero_object.zero_is_terminal = _.is_terminal

source

@[protected, instance]

def category_theory.limits.has_zero_object.has_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.has_initial C

A zero object is in particular initial.

source

@[protected, instance]

def category_theory.limits.has_zero_object.has_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.has_terminal C

A zero object is in particular terminal.

source

noncomputable def category_theory.limits.has_zero_object.zero_iso_is_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (t : category_theory.limits.is_initial X) :

0 ≅ X

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

Equations

category_theory.limits.has_zero_object.zero_iso_is_initial t = category_theory.limits.has_zero_object.zero_is_initial.unique_up_to_iso t

source

noncomputable def category_theory.limits.has_zero_object.zero_iso_is_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] {X : C} (t : category_theory.limits.is_terminal X) :

0 ≅ X

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

Equations

category_theory.limits.has_zero_object.zero_iso_is_terminal t = category_theory.limits.has_zero_object.zero_is_terminal.unique_up_to_iso t

source

noncomputable def category_theory.limits.has_zero_object.zero_iso_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_initial C] :

0 ≅ ⊥_ C

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

Equations

category_theory.limits.has_zero_object.zero_iso_initial = category_theory.limits.has_zero_object.zero_is_initial.unique_up_to_iso category_theory.limits.initial_is_initial

source

noncomputable def category_theory.limits.has_zero_object.zero_iso_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_terminal C] :

0 ≅ ⊤_ C

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

Equations

category_theory.limits.has_zero_object.zero_iso_terminal = category_theory.limits.has_zero_object.zero_is_terminal.unique_up_to_iso category_theory.limits.terminal_is_terminal

source

@[protected, instance]

def category_theory.limits.has_zero_object.has_strict_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] :

category_theory.limits.initial_mono_class C

source

theorem category_theory.functor.is_zero_iff {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_zero_object D] (F : C ⥤ D) :

category_theory.limits.is_zero F ↔ ∀ (X : C), category_theory.limits.is_zero (F.obj X)

mathlib3 documentation

Zero objects #

References #