category_theory.limits.shapes.terminal

@[simp]

theorem category_theory.limits.as_empty_cone_π_app {C : Type u₁} [category_theory.category C] (X : C) (X_1 : category_theory.discrete pempty) :

(category_theory.limits.as_empty_cone X).π.app X_1 = category_theory.limits.as_empty_cone._aux_1 X X_1

source

@[simp]

theorem category_theory.limits.as_empty_cone_X {C : Type u₁} [category_theory.category C] (X : C) :

(category_theory.limits.as_empty_cone X).X = X

source

def category_theory.limits.as_empty_cone {C : Type u₁} [category_theory.category C] (X : C) :

category_theory.limits.cone (category_theory.functor.empty C)

Construct a cone for the empty diagram given an object.

Equations

category_theory.limits.as_empty_cone X = {X := X, π := {app := category_theory.limits.as_empty_cone._aux_1 X, naturality' := _}}

source

@[simp]

theorem category_theory.limits.as_empty_cocone_X {C : Type u₁} [category_theory.category C] (X : C) :

(category_theory.limits.as_empty_cocone X).X = X

source

def category_theory.limits.as_empty_cocone {C : Type u₁} [category_theory.category C] (X : C) :

category_theory.limits.cocone (category_theory.functor.empty C)

Construct a cocone for the empty diagram given an object.

Equations

category_theory.limits.as_empty_cocone X = {X := X, ι := {app := category_theory.limits.as_empty_cocone._aux_1 X, naturality' := _}}

source

@[simp]

theorem category_theory.limits.as_empty_cocone_ι_app {C : Type u₁} [category_theory.category C] (X : C) (X_1 : category_theory.discrete pempty) :

(category_theory.limits.as_empty_cocone X).ι.app X_1 = category_theory.limits.as_empty_cocone._aux_1 X X_1

source

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

Type (max u₁ v₁)

X is terminal if the cone it induces on the empty diagram is limiting.

source

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

Type (max u₁ v₁)

X is initial if the cocone it induces on the empty diagram is colimiting.

source

def category_theory.limits.is_terminal_equiv_unique {C : Type u₁} [category_theory.category C] (F : category_theory.discrete pempty ⥤ C) (Y : C) :

category_theory.limits.is_limit {X := Y, π := {app := category_theory.limits.is_terminal_equiv_unique._aux_1 F Y, naturality' := _}} ≃ Π (X : C), unique (X ⟶ Y)

An object Y is terminal iff for every X there is a unique morphism X ⟶ Y.

Equations

category_theory.limits.is_terminal_equiv_unique F Y = {to_fun := λ (t : category_theory.limits.is_limit {X := Y, π := {app := category_theory.limits.is_terminal_equiv_unique._aux_1 F Y, naturality' := _}}) (X : C), {to_inhabited := {default := t.lift {X := X, π := id (λ (F : category_theory.discrete pempty ⥤ C) (Y : C) (t : category_theory.limits.is_limit {X := Y, π := {app := category_theory.limits.is_terminal_equiv_unique._aux_1 F Y, naturality' := _}}) (X : C), {app := category_theory.limits.is_terminal_equiv_unique._aux_2 F Y t X, naturality' := _}) F Y t X}}, uniq := _}, inv_fun := λ (u : Π (X : C), unique (X ⟶ Y)), {lift := λ (s : category_theory.limits.cone F), inhabited.default, fac' := _, uniq' := _}, left_inv := _, right_inv := _}

source

def category_theory.limits.is_terminal.of_unique {C : Type u₁} [category_theory.category C] (Y : C) [h : Π (X : C), unique (X ⟶ Y)] :

category_theory.limits.is_terminal Y

An object Y is terminal if for every X there is a unique morphism X ⟶ Y (as an instance).

Equations

category_theory.limits.is_terminal.of_unique Y = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), inhabited.default, fac' := _, uniq' := _}

source

def category_theory.limits.is_terminal_top {α : Type u_1} [preorder α] [order_top α] :

category_theory.limits.is_terminal ⊤

If α is a preorder with top, then ⊤ is a terminal object.

Equations

category_theory.limits.is_terminal_top = category_theory.limits.is_terminal.of_unique ⊤

source

def category_theory.limits.is_terminal.of_iso {C : Type u₁} [category_theory.category C] {Y Z : C} (hY : category_theory.limits.is_terminal Y) (i : Y ≅ Z) :

category_theory.limits.is_terminal Z

Transport a term of type is_terminal across an isomorphism.

Equations

hY.of_iso i = category_theory.limits.is_limit.of_iso_limit hY {hom := {hom := i.hom, w' := _}, inv := {hom := i.inv, w' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

def category_theory.limits.is_initial_equiv_unique {C : Type u₁} [category_theory.category C] (F : category_theory.discrete pempty ⥤ C) (X : C) :

category_theory.limits.is_colimit {X := X, ι := {app := category_theory.limits.is_initial_equiv_unique._aux_1 F X, naturality' := _}} ≃ Π (Y : C), unique (X ⟶ Y)

An object X is initial iff for every Y there is a unique morphism X ⟶ Y.

Equations

category_theory.limits.is_initial_equiv_unique F X = {to_fun := λ (t : category_theory.limits.is_colimit {X := X, ι := {app := category_theory.limits.is_initial_equiv_unique._aux_1 F X, naturality' := _}}) (X_1 : C), {to_inhabited := {default := t.desc {X := X_1, ι := id (λ (F : category_theory.discrete pempty ⥤ C) (X : C) (t : category_theory.limits.is_colimit {X := X, ι := {app := category_theory.limits.is_initial_equiv_unique._aux_1 F X, naturality' := _}}) (X_1 : C), {app := category_theory.limits.is_initial_equiv_unique._aux_2 F X t X_1, naturality' := _}) F X t X_1}}, uniq := _}, inv_fun := λ (u : Π (Y : C), unique (X ⟶ Y)), {desc := λ (s : category_theory.limits.cocone F), inhabited.default, fac' := _, uniq' := _}, left_inv := _, right_inv := _}

source

def category_theory.limits.is_initial.of_unique {C : Type u₁} [category_theory.category C] (X : C) [h : Π (Y : C), unique (X ⟶ Y)] :

category_theory.limits.is_initial X

An object X is initial if for every Y there is a unique morphism X ⟶ Y (as an instance).

Equations

category_theory.limits.is_initial.of_unique X = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), inhabited.default, fac' := _, uniq' := _}

source

def category_theory.limits.is_initial_bot {α : Type u_1} [preorder α] [order_bot α] :

category_theory.limits.is_initial ⊥

If α is a preorder with bot, then ⊥ is an initial object.

Equations

category_theory.limits.is_initial_bot = category_theory.limits.is_initial.of_unique ⊥

source

def category_theory.limits.is_initial.of_iso {C : Type u₁} [category_theory.category C] {X Y : C} (hX : category_theory.limits.is_initial X) (i : X ≅ Y) :

category_theory.limits.is_initial Y

Transport a term of type is_initial across an isomorphism.

Equations

hX.of_iso i = category_theory.limits.is_colimit.of_iso_colimit hX {hom := {hom := i.hom, w' := _}, inv := {hom := i.inv, w' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

def category_theory.limits.is_terminal.from {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_terminal X) (Y : C) :

Y ⟶ X

Give the morphism to a terminal object from any other.

Equations

t.from Y = t.lift (category_theory.limits.as_empty_cone Y)

source

theorem category_theory.limits.is_terminal.hom_ext {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_terminal X) (f g : Y ⟶ X) :

f = g

Any two morphisms to a terminal object are equal.

source

@[simp]

theorem category_theory.limits.is_terminal.comp_from {C : Type u₁} [category_theory.category C] {Z : C} (t : category_theory.limits.is_terminal Z) {X Y : C} (f : X ⟶ Y) :

f ≫ t.from Y = t.from X

source

@[simp]

theorem category_theory.limits.is_terminal.from_self {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_terminal X) :

t.from X = 𝟙 X

source

def category_theory.limits.is_initial.to {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_initial X) (Y : C) :

X ⟶ Y

Give the morphism from an initial object to any other.

Equations

t.to Y = t.desc (category_theory.limits.as_empty_cocone Y)

source

theorem category_theory.limits.is_initial.hom_ext {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_initial X) (f g : X ⟶ Y) :

f = g

Any two morphisms from an initial object are equal.

source

@[simp]

theorem category_theory.limits.is_initial.to_comp {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_initial X) {Y Z : C} (f : Y ⟶ Z) :

t.to Y ≫ f = t.to Z

source

@[simp]

theorem category_theory.limits.is_initial.to_self {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_initial X) :

t.to X = 𝟙 X

source

def category_theory.limits.is_terminal.split_mono_from {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_terminal X) (f : X ⟶ Y) :

category_theory.split_mono f

Any morphism from a terminal object is split mono.

Equations

t.split_mono_from f = {retraction := t.from Y, id' := _}

source

def category_theory.limits.is_initial.split_epi_to {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_initial X) (f : Y ⟶ X) :

category_theory.split_epi f

Any morphism to an initial object is split epi.

Equations

t.split_epi_to f = {section_ := t.to Y, id' := _}

source

theorem category_theory.limits.is_terminal.mono_from {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_terminal X) (f : X ⟶ Y) :

category_theory.mono f

Any morphism from a terminal object is mono.

source

theorem category_theory.limits.is_initial.epi_to {C : Type u₁} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_initial X) (f : Y ⟶ X) :

category_theory.epi f

Any morphism to an initial object is epi.

source

@[simp]

theorem category_theory.limits.is_terminal.unique_up_to_iso_inv {C : Type u₁} [category_theory.category C] {T T' : C} (hT : category_theory.limits.is_terminal T) (hT' : category_theory.limits.is_terminal T') :

(hT.unique_up_to_iso hT').inv = hT.from T'

source

@[simp]

theorem category_theory.limits.is_terminal.unique_up_to_iso_hom {C : Type u₁} [category_theory.category C] {T T' : C} (hT : category_theory.limits.is_terminal T) (hT' : category_theory.limits.is_terminal T') :

(hT.unique_up_to_iso hT').hom = hT'.from T

source

def category_theory.limits.is_terminal.unique_up_to_iso {C : Type u₁} [category_theory.category C] {T T' : C} (hT : category_theory.limits.is_terminal T) (hT' : category_theory.limits.is_terminal T') :

T ≅ T'

If T and T' are terminal, they are isomorphic.

Equations

hT.unique_up_to_iso hT' = {hom := hT'.from T, inv := hT.from T', hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.is_initial.unique_up_to_iso_hom {C : Type u₁} [category_theory.category C] {I I' : C} (hI : category_theory.limits.is_initial I) (hI' : category_theory.limits.is_initial I') :

(hI.unique_up_to_iso hI').hom = hI.to I'

source

def category_theory.limits.is_initial.unique_up_to_iso {C : Type u₁} [category_theory.category C] {I I' : C} (hI : category_theory.limits.is_initial I) (hI' : category_theory.limits.is_initial I') :

I ≅ I'

If I and I' are initial, they are isomorphic.

Equations

hI.unique_up_to_iso hI' = {hom := hI.to I', inv := hI'.to I, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.is_initial.unique_up_to_iso_inv {C : Type u₁} [category_theory.category C] {I I' : C} (hI : category_theory.limits.is_initial I) (hI' : category_theory.limits.is_initial I') :

(hI.unique_up_to_iso hI').inv = hI'.to I

source

def category_theory.limits.has_terminal (C : Type u₁) [category_theory.category C] :

Prop

A category has a terminal object if it has a limit over the empty diagram. Use has_terminal_of_unique to construct instances.

source

def category_theory.limits.has_initial (C : Type u₁) [category_theory.category C] :

Prop

A category has an initial object if it has a colimit over the empty diagram. Use has_initial_of_unique to construct instances.

source

def category_theory.limits.is_limit_change_empty_cone (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} {c₁ : category_theory.limits.cone F₁} (hl : category_theory.limits.is_limit c₁) (c₂ : category_theory.limits.cone F₂) (hi : c₁.X ≅ c₂.X) :

category_theory.limits.is_limit c₂

Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.

Equations

category_theory.limits.is_limit_change_empty_cone C hl c₂ hi = {lift := λ (c : category_theory.limits.cone F₂), hl.lift {X := c.X, π := {app := category_theory.limits.is_limit_change_empty_cone._aux_1 C hl c₂ hi c, naturality' := _}} ≫ hi.hom, fac' := _, uniq' := _}

source

def category_theory.limits.is_limit_empty_cone_equiv (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} (c₁ : category_theory.limits.cone F₁) (c₂ : category_theory.limits.cone F₂) (h : c₁.X ≅ c₂.X) :

category_theory.limits.is_limit c₁ ≃ category_theory.limits.is_limit c₂

Replacing an empty cone in is_limit by another with the same cone point is an equivalence.

Equations

category_theory.limits.is_limit_empty_cone_equiv C c₁ c₂ h = {to_fun := λ (hl : category_theory.limits.is_limit c₁), category_theory.limits.is_limit_change_empty_cone C hl c₂ h, inv_fun := λ (hl : category_theory.limits.is_limit c₂), category_theory.limits.is_limit_change_empty_cone C hl c₁ h.symm, left_inv := _, right_inv := _}

source

theorem category_theory.limits.has_terminal_change_diagram (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} (h : category_theory.limits.has_limit F₁) :

category_theory.limits.has_limit F₂

source

theorem category_theory.limits.has_terminal_change_universe (C : Type u₁) [category_theory.category C] [h : category_theory.limits.has_limits_of_shape (category_theory.discrete pempty) C] :

category_theory.limits.has_limits_of_shape (category_theory.discrete pempty) C

source

def category_theory.limits.is_colimit_change_empty_cocone (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} {c₁ : category_theory.limits.cocone F₁} (hl : category_theory.limits.is_colimit c₁) (c₂ : category_theory.limits.cocone F₂) (hi : c₁.X ≅ c₂.X) :

category_theory.limits.is_colimit c₂

Being initial is independent of the empty diagram, its universe, and the cocone over it, as long as the cocone points are isomorphic.

Equations

category_theory.limits.is_colimit_change_empty_cocone C hl c₂ hi = {desc := λ (c : category_theory.limits.cocone F₂), hi.inv ≫ hl.desc {X := c.X, ι := {app := category_theory.limits.is_colimit_change_empty_cocone._aux_1 C hl c₂ hi c, naturality' := _}}, fac' := _, uniq' := _}

source

def category_theory.limits.is_colimit_empty_cocone_equiv (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} (c₁ : category_theory.limits.cocone F₁) (c₂ : category_theory.limits.cocone F₂) (h : c₁.X ≅ c₂.X) :

category_theory.limits.is_colimit c₁ ≃ category_theory.limits.is_colimit c₂

Replacing an empty cocone in is_colimit by another with the same cocone point is an equivalence.

Equations

category_theory.limits.is_colimit_empty_cocone_equiv C c₁ c₂ h = {to_fun := λ (hl : category_theory.limits.is_colimit c₁), category_theory.limits.is_colimit_change_empty_cocone C hl c₂ h, inv_fun := λ (hl : category_theory.limits.is_colimit c₂), category_theory.limits.is_colimit_change_empty_cocone C hl c₁ h.symm, left_inv := _, right_inv := _}

source

theorem category_theory.limits.has_initial_change_diagram (C : Type u₁) [category_theory.category C] {F₁ : category_theory.discrete pempty ⥤ C} {F₂ : category_theory.discrete pempty ⥤ C} (h : category_theory.limits.has_colimit F₁) :

category_theory.limits.has_colimit F₂

source

theorem category_theory.limits.has_initial_change_universe (C : Type u₁) [category_theory.category C] [h : category_theory.limits.has_colimits_of_shape (category_theory.discrete pempty) C] :

category_theory.limits.has_colimits_of_shape (category_theory.discrete pempty) C

source

noncomputable def category_theory.limits.terminal (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] :

C

An arbitrary choice of terminal object, if one exists. You can use the notation ⊤_ C. This object is characterized by having a unique morphism from any object.

source

noncomputable def category_theory.limits.initial (C : Type u₁) [category_theory.category C] [category_theory.limits.has_initial C] :

C

An arbitrary choice of initial object, if one exists. You can use the notation ⊥_ C. This object is characterized by having a unique morphism to any object.

source

theorem category_theory.limits.has_terminal_of_unique {C : Type u₁} [category_theory.category C] (X : C) [h : Π (Y : C), unique (Y ⟶ X)] :

category_theory.limits.has_terminal C

We can more explicitly show that a category has a terminal object by specifying the object, and showing there is a unique morphism to it from any other object.

source

theorem category_theory.limits.has_initial_of_unique {C : Type u₁} [category_theory.category C] (X : C) [h : Π (Y : C), unique (X ⟶ Y)] :

category_theory.limits.has_initial C

We can more explicitly show that a category has an initial object by specifying the object, and showing there is a unique morphism from it to any other object.

source

noncomputable def category_theory.limits.terminal.from {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) :

P ⟶ ⊤_ C

The map from an object to the terminal object.

source

noncomputable def category_theory.limits.initial.to {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] (P : C) :

⊥_ C ⟶ P

The map to an object from the initial object.

source

noncomputable def category_theory.limits.terminal_is_terminal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.limits.is_terminal (⊤_ C)

A terminal object is terminal.

Equations

category_theory.limits.terminal_is_terminal = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), category_theory.limits.terminal.from s.X, fac' := _, uniq' := _}

source

noncomputable def category_theory.limits.initial_is_initial {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] :

category_theory.limits.is_initial (⊥_ C)

An initial object is initial.

Equations

category_theory.limits.initial_is_initial = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), category_theory.limits.initial.to s.X, fac' := _, uniq' := _}

source

@[protected, instance]

noncomputable def category_theory.limits.unique_to_terminal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) :

unique (P ⟶ ⊤_ C)

Equations

category_theory.limits.unique_to_terminal P = ⇑(category_theory.limits.is_terminal_equiv_unique (category_theory.functor.empty C) (⊤_ C)) category_theory.limits.terminal_is_terminal P

source

@[protected, instance]

noncomputable def category_theory.limits.unique_from_initial {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] (P : C) :

unique (⊥_ C ⟶ P)

Equations

category_theory.limits.unique_from_initial P = ⇑(category_theory.limits.is_initial_equiv_unique (category_theory.functor.empty C) (⊥_ C)) category_theory.limits.initial_is_initial P

source

@[simp]

theorem category_theory.limits.terminal.comp_from {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] {P Q : C} (f : P ⟶ Q) :

f ≫ category_theory.limits.terminal.from Q = category_theory.limits.terminal.from P

source

@[simp]

theorem category_theory.limits.initial.to_comp {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] {P Q : C} (f : P ⟶ Q) :

category_theory.limits.initial.to P ≫ f = category_theory.limits.initial.to Q

source

@[simp]

noncomputable def category_theory.limits.initial_iso_is_initial {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] {P : C} (t : category_theory.limits.is_initial P) :

⊥_ C ≅ P

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

Equations

category_theory.limits.initial_iso_is_initial t = category_theory.limits.initial_is_initial.unique_up_to_iso t

source

@[simp]

noncomputable def category_theory.limits.terminal_iso_is_terminal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] {P : C} (t : category_theory.limits.is_terminal P) :

⊤_ C ≅ P

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

Equations

category_theory.limits.terminal_iso_is_terminal t = category_theory.limits.terminal_is_terminal.unique_up_to_iso t

source

@[protected, instance]

noncomputable def category_theory.limits.terminal.split_mono_from {C : Type u₁} [category_theory.category C] {Y : C} [category_theory.limits.has_terminal C] (f : ⊤_ C ⟶ Y) :

category_theory.split_mono f

Any morphism from a terminal object is split mono.

Equations

category_theory.limits.terminal.split_mono_from f = category_theory.limits.terminal_is_terminal.split_mono_from f

source

@[protected, instance]

noncomputable def category_theory.limits.initial.split_epi_to {C : Type u₁} [category_theory.category C] {Y : C} [category_theory.limits.has_initial C] (f : Y ⟶ ⊥_ C) :

category_theory.split_epi f

Any morphism to an initial object is split epi.

Equations

category_theory.limits.initial.split_epi_to f = category_theory.limits.initial_is_initial.split_epi_to f

source

def category_theory.limits.terminal_op_of_initial {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_initial X) :

category_theory.limits.is_terminal (opposite.op X)

An initial object is terminal in the opposite category.

Equations

category_theory.limits.terminal_op_of_initial t = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty Cᵒᵖ)), (t.to (opposite.unop s.X)).op, fac' := _, uniq' := _}

source

def category_theory.limits.terminal_unop_of_initial {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} (t : category_theory.limits.is_initial X) :

category_theory.limits.is_terminal (opposite.unop X)

An initial object in the opposite category is terminal in the original category.

Equations

category_theory.limits.terminal_unop_of_initial t = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), (t.to (opposite.op s.X)).unop, fac' := _, uniq' := _}

source

def category_theory.limits.initial_op_of_terminal {C : Type u₁} [category_theory.category C] {X : C} (t : category_theory.limits.is_terminal X) :

category_theory.limits.is_initial (opposite.op X)

A terminal object is initial in the opposite category.

Equations

category_theory.limits.initial_op_of_terminal t = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty Cᵒᵖ)), (t.from (opposite.unop s.X)).op, fac' := _, uniq' := _}

source

def category_theory.limits.initial_unop_of_terminal {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} (t : category_theory.limits.is_terminal X) :

category_theory.limits.is_initial (opposite.unop X)

A terminal object in the opposite category is initial in the original category.

Equations

category_theory.limits.initial_unop_of_terminal t = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), (t.from (opposite.op s.X)).unop, fac' := _, uniq' := _}

source

@[protected, instance]

def category_theory.limits.obj.has_limit {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.limits.has_limit ((category_theory.functor.const J).obj (⊤_ C))

source

@[simp]

theorem category_theory.limits.limit_const_terminal_hom {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.limits.limit_const_terminal.hom = category_theory.limits.terminal.from (category_theory.limits.limit ((category_theory.functor.const J).obj (⊤_ C)))

source

noncomputable def category_theory.limits.limit_const_terminal {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.limits.limit ((category_theory.functor.const J).obj (⊤_ C)) ≅ ⊤_ C

The limit of the constant ⊤_ C functor is ⊤_ C.

Equations

category_theory.limits.limit_const_terminal = {hom := category_theory.limits.terminal.from (category_theory.limits.limit ((category_theory.functor.const J).obj (⊤_ C))), inv := category_theory.limits.limit.lift ((category_theory.functor.const J).obj (⊤_ C)) {X := ⊤_ C, π := {app := λ (j : J), category_theory.limits.terminal.from (((category_theory.functor.const J).obj (⊤_ C)).obj j), naturality' := _}}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.limit_const_terminal_inv_π {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_terminal C] {j : J} :

category_theory.limits.limit_const_terminal.inv ≫ category_theory.limits.limit.π ((category_theory.functor.const J).obj (⊤_ C)) j = category_theory.limits.terminal.from (⊤_ C)

source

@[simp]

theorem category_theory.limits.limit_const_terminal_inv_π_assoc {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_terminal C] {j : J} {X' : C} (f' : ((category_theory.functor.const J).obj (⊤_ C)).obj j ⟶ X') :

category_theory.limits.limit_const_terminal.inv ≫ category_theory.limits.limit.π ((category_theory.functor.const J).obj (⊤_ C)) j ≫ f' = category_theory.limits.terminal.from (⊤_ C) ≫ f'

source

@[protected, instance]

def category_theory.limits.obj.has_colimit {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_initial C] :

category_theory.limits.has_colimit ((category_theory.functor.const J).obj (⊥_ C))

source

@[simp]

theorem category_theory.limits.colimit_const_initial_inv {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_initial C] :

category_theory.limits.colimit_const_initial.inv = category_theory.limits.initial.to (category_theory.limits.colimit ((category_theory.functor.const J).obj (⊥_ C)))

source

noncomputable def category_theory.limits.colimit_const_initial {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_initial C] :

category_theory.limits.colimit ((category_theory.functor.const J).obj (⊥_ C)) ≅ ⊥_ C

The colimit of the constant ⊥_ C functor is ⊥_ C.

Equations

category_theory.limits.colimit_const_initial = {hom := category_theory.limits.colimit.desc ((category_theory.functor.const J).obj (⊥_ C)) {X := ⊥_ C, ι := {app := λ (j : J), category_theory.limits.initial.to (((category_theory.functor.const J).obj (⊥_ C)).obj j), naturality' := _}}, inv := category_theory.limits.initial.to (category_theory.limits.colimit ((category_theory.functor.const J).obj (⊥_ C))), hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.ι_colimit_const_initial_hom {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_initial C] {j : J} :

category_theory.limits.colimit.ι ((category_theory.functor.const J).obj (⊥_ C)) j ≫ category_theory.limits.colimit_const_initial.hom = category_theory.limits.initial.to (⊥_ C)

source

@[simp]

theorem category_theory.limits.ι_colimit_const_initial_hom_assoc {J : Type u_1} [category_theory.category J] {C : Type u_3} [category_theory.category C] [category_theory.limits.has_initial C] {j : J} {X' : C} (f' : ⊥_ C ⟶ X') :

category_theory.limits.colimit.ι ((category_theory.functor.const J).obj (⊥_ C)) j ≫ category_theory.limits.colimit_const_initial.hom ≫ f' = category_theory.limits.initial.to (⊥_ C) ≫ f'

source

@[class]

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

Prop

is_initial_mono_from : ∀ {I : C} (X : C) (hI : category_theory.limits.is_initial I), category_theory.mono (hI.to X)

A category is a initial_mono_class if the canonical morphism of an initial object is a monomorphism. In practice, this is most useful when given an arbitrary morphism out of the chosen initial object, see initial.mono_from. Given a terminal object, this is equivalent to the assumption that the unique morphism from initial to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.

TODO: This is a condition satisfied by categories with zero objects and morphisms.

Instances of this typeclass

source

theorem category_theory.limits.is_initial.mono_from {C : Type u₁} [category_theory.category C] [category_theory.limits.initial_mono_class C] {I X : C} (hI : category_theory.limits.is_initial I) (f : I ⟶ X) :

category_theory.mono f

source

@[protected, instance]

def category_theory.limits.initial.mono_from {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] [category_theory.limits.initial_mono_class C] (X : C) (f : ⊥_ C ⟶ X) :

category_theory.mono f

source

theorem category_theory.limits.initial_mono_class.of_is_initial {C : Type u₁} [category_theory.category C] {I : C} (hI : category_theory.limits.is_initial I) (h : ∀ (X : C), category_theory.mono (hI.to X)) :

category_theory.limits.initial_mono_class C

To show a category is a initial_mono_class it suffices to give an initial object such that every morphism out of it is a monomorphism.

source

theorem category_theory.limits.initial_mono_class.of_initial {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] (h : ∀ (X : C), category_theory.mono (category_theory.limits.initial.to X)) :

category_theory.limits.initial_mono_class C

To show a category is a initial_mono_class it suffices to show every morphism out of the initial object is a monomorphism.

source

theorem category_theory.limits.initial_mono_class.of_is_terminal {C : Type u₁} [category_theory.category C] {I T : C} (hI : category_theory.limits.is_initial I) (hT : category_theory.limits.is_terminal T) (f : category_theory.mono (hI.to T)) :

category_theory.limits.initial_mono_class C

To show a category is a initial_mono_class it suffices to show the unique morphism from an initial object to a terminal object is a monomorphism.

source

theorem category_theory.limits.initial_mono_class.of_terminal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_initial C] [category_theory.limits.has_terminal C] (h : category_theory.mono (category_theory.limits.initial.to (⊤_ C))) :

category_theory.limits.initial_mono_class C

To show a category is a initial_mono_class it suffices to show the unique morphism from the initial object to a terminal object is a monomorphism.

source

noncomputable def category_theory.limits.terminal_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] :

G.obj (⊤_ C) ⟶ ⊤_ D

The comparison morphism from the image of a terminal object to the terminal object in the target category. This is an isomorphism iff G preserves terminal objects, see category_theory.limits.preserves_terminal.of_iso_comparison.

Equations

category_theory.limits.terminal_comparison G = category_theory.limits.terminal.from (G.obj (⊤_ C))

Instances for category_theory.limits.terminal_comparison

category_theory.limits.terminal_comparison.category_theory.is_iso

source

noncomputable def category_theory.limits.initial_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_initial C] [category_theory.limits.has_initial D] :

⊥_ D ⟶ G.obj (⊥_ C)

The comparison morphism from the initial object in the target category to the image of the initial object.

Equations

category_theory.limits.initial_comparison G = category_theory.limits.initial.to (G.obj (⊥_ C))

Instances for category_theory.limits.initial_comparison

category_theory.limits.initial_comparison.category_theory.is_iso

source

def category_theory.limits.cone_of_diagram_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_initial X) (F : J ⥤ C) :

category_theory.limits.cone F

From a functor F : J ⥤ C, given an initial object of J, construct a cone for J. In limit_of_diagram_initial we show it is a limit cone.

Equations

category_theory.limits.cone_of_diagram_initial tX F = {X := F.obj X, π := {app := λ (j : J), F.map (tX.to j), naturality' := _}}

source

@[simp]

theorem category_theory.limits.cone_of_diagram_initial_π_app {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_initial X) (F : J ⥤ C) (j : J) :

(category_theory.limits.cone_of_diagram_initial tX F).π.app j = F.map (tX.to j)

source

@[simp]

theorem category_theory.limits.cone_of_diagram_initial_X {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_initial X) (F : J ⥤ C) :

(category_theory.limits.cone_of_diagram_initial tX F).X = F.obj X

source

def category_theory.limits.limit_of_diagram_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_initial X) (F : J ⥤ C) :

category_theory.limits.is_limit (category_theory.limits.cone_of_diagram_initial tX F)

From a functor F : J ⥤ C, given an initial object of J, show the cone cone_of_diagram_initial is a limit.

Equations

category_theory.limits.limit_of_diagram_initial tX F = {lift := λ (s : category_theory.limits.cone F), s.π.app X, fac' := _, uniq' := _}

source

noncomputable def category_theory.limits.limit_of_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] (F : J ⥤ C) [category_theory.limits.has_initial J] [category_theory.limits.has_limit F] :

category_theory.limits.limit F ≅ F.obj (⊥_ J)

For a functor F : J ⥤ C, if J has an initial object then the image of it is isomorphic to the limit of F.

Equations

category_theory.limits.limit_of_initial F = (category_theory.limits.limit.is_limit F).cone_point_unique_up_to_iso (category_theory.limits.limit_of_diagram_initial category_theory.limits.initial_is_initial F)

source

@[simp]

theorem category_theory.limits.cone_of_diagram_terminal_X {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_terminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

(category_theory.limits.cone_of_diagram_terminal hX F).X = F.obj X

source

noncomputable def category_theory.limits.cone_of_diagram_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_terminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.cone F

From a functor F : J ⥤ C, given a terminal object of J, construct a cone for J, provided that the morphisms in the diagram are isomorphisms. In limit_of_diagram_terminal we show it is a limit cone.

Equations

category_theory.limits.cone_of_diagram_terminal hX F = {X := F.obj X, π := {app := λ (i : J), category_theory.inv (F.map (hX.from i)), naturality' := _}}

source

@[simp]

theorem category_theory.limits.cone_of_diagram_terminal_π_app {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_terminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] (i : J) :

(category_theory.limits.cone_of_diagram_terminal hX F).π.app i = category_theory.inv (F.map (hX.from i))

source

def category_theory.limits.limit_of_diagram_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_terminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.is_limit (category_theory.limits.cone_of_diagram_terminal hX F)

From a functor F : J ⥤ C, given a terminal object of J and that the morphisms in the diagram are isomorphisms, show the cone cone_of_diagram_terminal is a limit.

Equations

category_theory.limits.limit_of_diagram_terminal hX F = {lift := λ (S : category_theory.limits.cone F), S.π.app X, fac' := _, uniq' := _}

source

noncomputable def category_theory.limits.limit_of_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] (F : J ⥤ C) [category_theory.limits.has_terminal J] [category_theory.limits.has_limit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.limit F ≅ F.obj (⊤_ J)

For a functor F : J ⥤ C, if J has a terminal object and all the morphisms in the diagram are isomorphisms, then the image of the terminal object is isomorphic to the limit of F.

Equations

category_theory.limits.limit_of_terminal F = (category_theory.limits.limit.is_limit F).cone_point_unique_up_to_iso (category_theory.limits.limit_of_diagram_terminal category_theory.limits.terminal_is_terminal F)

source

@[simp]

theorem category_theory.limits.cocone_of_diagram_terminal_ι_app {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_terminal X) (F : J ⥤ C) (j : J) :

(category_theory.limits.cocone_of_diagram_terminal tX F).ι.app j = F.map (tX.from j)

source

def category_theory.limits.cocone_of_diagram_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_terminal X) (F : J ⥤ C) :

category_theory.limits.cocone F

From a functor F : J ⥤ C, given a terminal object of J, construct a cocone for J. In colimit_of_diagram_terminal we show it is a colimit cocone.

Equations

category_theory.limits.cocone_of_diagram_terminal tX F = {X := F.obj X, ι := {app := λ (j : J), F.map (tX.from j), naturality' := _}}

source

@[simp]

theorem category_theory.limits.cocone_of_diagram_terminal_X {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_terminal X) (F : J ⥤ C) :

(category_theory.limits.cocone_of_diagram_terminal tX F).X = F.obj X

source

def category_theory.limits.colimit_of_diagram_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (tX : category_theory.limits.is_terminal X) (F : J ⥤ C) :

category_theory.limits.is_colimit (category_theory.limits.cocone_of_diagram_terminal tX F)

From a functor F : J ⥤ C, given a terminal object of J, show the cocone cocone_of_diagram_terminal is a colimit.

Equations

category_theory.limits.colimit_of_diagram_terminal tX F = {desc := λ (s : category_theory.limits.cocone F), s.ι.app X, fac' := _, uniq' := _}

source

noncomputable def category_theory.limits.colimit_of_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] (F : J ⥤ C) [category_theory.limits.has_terminal J] [category_theory.limits.has_colimit F] :

category_theory.limits.colimit F ≅ F.obj (⊤_ J)

For a functor F : J ⥤ C, if J has a terminal object then the image of it is isomorphic to the colimit of F.

Equations

category_theory.limits.colimit_of_terminal F = (category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.colimit_of_diagram_terminal category_theory.limits.terminal_is_terminal F)

source

@[simp]

theorem category_theory.limits.cocone_of_diagram_initial_X {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_initial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

(category_theory.limits.cocone_of_diagram_initial hX F).X = F.obj X

source

noncomputable def category_theory.limits.cocone_of_diagram_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_initial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.cocone F

From a functor F : J ⥤ C, given an initial object of J, construct a cocone for J, provided that the morphisms in the diagram are isomorphisms. In colimit_of_diagram_initial we show it is a colimit cocone.

Equations

category_theory.limits.cocone_of_diagram_initial hX F = {X := F.obj X, ι := {app := λ (i : J), category_theory.inv (F.map (hX.to i)), naturality' := _}}

source

@[simp]

theorem category_theory.limits.cocone_of_diagram_initial_ι_app {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_initial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] (i : J) :

(category_theory.limits.cocone_of_diagram_initial hX F).ι.app i = category_theory.inv (F.map (hX.to i))

source

def category_theory.limits.colimit_of_diagram_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {X : J} (hX : category_theory.limits.is_initial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.is_colimit (category_theory.limits.cocone_of_diagram_initial hX F)

From a functor F : J ⥤ C, given an initial object of J and that the morphisms in the diagram are isomorphisms, show the cone cocone_of_diagram_initial is a colimit.

Equations

category_theory.limits.colimit_of_diagram_initial hX F = {desc := λ (S : category_theory.limits.cocone F), S.ι.app X, fac' := _, uniq' := _}

source

noncomputable def category_theory.limits.colimit_of_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] (F : J ⥤ C) [category_theory.limits.has_initial J] [category_theory.limits.has_colimit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.limits.colimit F ≅ F.obj (⊥_ J)

For a functor F : J ⥤ C, if J has an initial object and all the morphisms in the diagram are isomorphisms, then the image of the initial object is isomorphic to the colimit of F.

Equations

category_theory.limits.colimit_of_initial F = (category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.colimit_of_diagram_initial category_theory.limits.initial_is_initial F)

source

theorem category_theory.limits.is_iso_π_of_is_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {j : J} (I : category_theory.limits.is_initial j) (F : J ⥤ C) [category_theory.limits.has_limit F] :

category_theory.is_iso (category_theory.limits.limit.π F j)

If j is initial in the index category, then the map limit.π F j is an isomorphism.

source

@[protected, instance]

def category_theory.limits.is_iso_π_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] [category_theory.limits.has_initial J] (F : J ⥤ C) [category_theory.limits.has_limit F] :

category_theory.is_iso (category_theory.limits.limit.π F (⊥_ J))

source

theorem category_theory.limits.is_iso_π_of_is_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {j : J} (I : category_theory.limits.is_terminal j) (F : J ⥤ C) [category_theory.limits.has_limit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.is_iso (category_theory.limits.limit.π F j)

source

@[protected, instance]

def category_theory.limits.is_iso_π_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] [category_theory.limits.has_terminal J] (F : J ⥤ C) [category_theory.limits.has_limit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.is_iso (category_theory.limits.limit.π F (⊤_ J))

source

theorem category_theory.limits.is_iso_ι_of_is_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {j : J} (I : category_theory.limits.is_terminal j) (F : J ⥤ C) [category_theory.limits.has_colimit F] :

category_theory.is_iso (category_theory.limits.colimit.ι F j)

If j is terminal in the index category, then the map colimit.ι F j is an isomorphism.

source

@[protected, instance]

def category_theory.limits.is_iso_ι_terminal {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] [category_theory.limits.has_terminal J] (F : J ⥤ C) [category_theory.limits.has_colimit F] :

category_theory.is_iso (category_theory.limits.colimit.ι F (⊤_ J))

source

theorem category_theory.limits.is_iso_ι_of_is_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] {j : J} (I : category_theory.limits.is_initial j) (F : J ⥤ C) [category_theory.limits.has_colimit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.is_iso (category_theory.limits.colimit.ι F j)

source

@[protected, instance]

def category_theory.limits.is_iso_ι_initial {C : Type u₁} [category_theory.category C] {J : Type u} [category_theory.category J] [category_theory.limits.has_initial J] (F : J ⥤ C) [category_theory.limits.has_colimit F] [∀ (i j : J) (f : i ⟶ j), category_theory.is_iso (F.map f)] :

category_theory.is_iso (category_theory.limits.colimit.ι F (⊥_ J))

mathlib documentation

Initial and terminal objects in a category. #

References #