category_theory.limits.cone_category

@[simp]

theorem category_theory.limits.cone.to_costructured_arrow_obj {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cone F) :

(category_theory.limits.cone.to_costructured_arrow F).obj c = category_theory.costructured_arrow.mk c.π

source

@[simp]

theorem category_theory.limits.cone.to_costructured_arrow_map {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cone F) (f : c ⟶ d) :

(category_theory.limits.cone.to_costructured_arrow F).map f = category_theory.costructured_arrow.hom_mk f.hom _

source

def category_theory.limits.cone.to_costructured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.cone F ⥤ category_theory.costructured_arrow (category_theory.functor.const J) F

Construct an object of the category (Δ ↓ F) from a cone on F. This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations

category_theory.limits.cone.to_costructured_arrow F = {obj := λ (c : category_theory.limits.cone F), category_theory.costructured_arrow.mk c.π, map := λ (c d : category_theory.limits.cone F) (f : c ⟶ d), category_theory.costructured_arrow.hom_mk f.hom _, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.cone.from_costructured_arrow_obj_π {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.from_costructured_arrow F).obj c).π = c.hom

source

@[simp]

theorem category_theory.limits.cone.from_costructured_arrow_obj_X {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.from_costructured_arrow F).obj c).X = c.left

source

@[simp]

theorem category_theory.limits.cone.from_costructured_arrow_map_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.costructured_arrow (category_theory.functor.const J) F) (f : c ⟶ d) :

((category_theory.limits.cone.from_costructured_arrow F).map f).hom = f.left

source

def category_theory.limits.cone.from_costructured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.costructured_arrow (category_theory.functor.const J) F ⥤ category_theory.limits.cone F

Construct a cone on F from an object of the category (Δ ↓ F). This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations

category_theory.limits.cone.from_costructured_arrow F = {obj := λ (c : category_theory.costructured_arrow (category_theory.functor.const J) F), {X := c.left, π := c.hom}, map := λ (c d : category_theory.costructured_arrow (category_theory.functor.const J) F) (f : c ⟶ d), {hom := f.left, w' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_functor_map_right_down_down {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cone F) (f : c ⟶ d) :

_ = _

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_inv_app_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).counit_iso.inv.app X).right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_functor_obj_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cone F) :

((category_theory.limits.cone.equiv_costructured_arrow F).functor.obj c).left = c.X

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).counit_iso.hom.app X).left = 𝟙 X.left

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_unit_iso_hom_app_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.limits.cone F) :

((category_theory.limits.cone.equiv_costructured_arrow F).unit_iso.hom.app X).hom = 𝟙 X.X

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_functor_obj_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cone F) :

((category_theory.limits.cone.equiv_costructured_arrow F).functor.obj c).hom = c.π

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_π {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).inverse.obj c).π = c.hom

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_functor_map_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cone F) (f : c ⟶ d) :

((category_theory.limits.cone.equiv_costructured_arrow F).functor.map f).left = f.hom

source

def category_theory.limits.cone.equiv_costructured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.cone F ≌ category_theory.costructured_arrow (category_theory.functor.const J) F

The category of cones on F is just the comma category (Δ ↓ F), where Δ is the constant functor.

Equations

category_theory.limits.cone.equiv_costructured_arrow F = category_theory.equivalence.mk (category_theory.limits.cone.to_costructured_arrow F) (category_theory.limits.cone.from_costructured_arrow F) (category_theory.nat_iso.of_components category_theory.limits.cones.eta _) (category_theory.nat_iso.of_components (λ (c : category_theory.costructured_arrow (category_theory.functor.const J) F), c.eta.symm) _)

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_map_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.costructured_arrow (category_theory.functor.const J) F) (f : c ⟶ d) :

((category_theory.limits.cone.equiv_costructured_arrow F).inverse.map f).hom = f.left

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_X {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).inverse.obj c).X = c.left

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_inv_app_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).counit_iso.inv.app X).left = 𝟙 X.left

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.costructured_arrow (category_theory.functor.const J) F) :

((category_theory.limits.cone.equiv_costructured_arrow F).counit_iso.hom.app X).right = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.limits.cone.equiv_costructured_arrow_unit_iso_inv_app_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.limits.cone F) :

((category_theory.limits.cone.equiv_costructured_arrow F).unit_iso.inv.app X).hom = 𝟙 X.X

source

def category_theory.limits.cone.is_limit_equiv_is_terminal {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} (c : category_theory.limits.cone F) :

category_theory.limits.is_limit c ≃ category_theory.limits.is_terminal c

A cone is a limit cone iff it is terminal.

Equations

c.is_limit_equiv_is_terminal = category_theory.limits.is_limit.iso_unique_cone_morphism.to_equiv.trans {to_fun := λ (h : Π (s : category_theory.limits.cone F), unique (s ⟶ c)), category_theory.limits.is_terminal.of_unique c, inv_fun := λ (h : category_theory.limits.is_terminal c) (s : category_theory.limits.cone F), {to_inhabited := {default := h.from s}, uniq := _}, left_inv := _, right_inv := _}

source

theorem category_theory.limits.has_limit_iff_has_terminal_cone {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.has_limit F ↔ category_theory.limits.has_terminal (category_theory.limits.cone F)

source

theorem category_theory.limits.has_limits_of_shape_iff_is_left_adjoint_const {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] :

category_theory.limits.has_limits_of_shape J C ↔ nonempty (category_theory.is_left_adjoint (category_theory.functor.const J))

source

theorem category_theory.limits.is_limit.lift_cone_morphism_eq_is_terminal_from {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} {c : category_theory.limits.cone F} (hc : category_theory.limits.is_limit c) (s : category_theory.limits.cone F) :

hc.lift_cone_morphism s = (⇑(c.is_limit_equiv_is_terminal) hc).from s

source

theorem category_theory.limits.is_terminal.from_eq_lift_cone_morphism {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} {c : category_theory.limits.cone F} (hc : category_theory.limits.is_terminal c) (s : category_theory.limits.cone F) :

hc.from s = (⇑(c.is_limit_equiv_is_terminal.symm) hc).lift_cone_morphism s

source

def category_theory.limits.is_limit.of_preserves_cone_terminal {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F : J ⥤ C} {F' : K ⥤ D} (G : category_theory.limits.cone F ⥤ category_theory.limits.cone F') [category_theory.limits.preserves_limit (category_theory.functor.empty (category_theory.limits.cone F)) G] {c : category_theory.limits.cone F} (hc : category_theory.limits.is_limit c) :

category_theory.limits.is_limit (G.obj c)

If G : cone F ⥤ cone F' preserves terminal objects, it preserves limit cones.

Equations

category_theory.limits.is_limit.of_preserves_cone_terminal G hc = ⇑((G.obj c).is_limit_equiv_is_terminal.symm) (category_theory.limits.is_terminal.is_terminal_obj G c (⇑(c.is_limit_equiv_is_terminal) hc))

source

def category_theory.limits.is_limit.of_reflects_cone_terminal {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F : J ⥤ C} {F' : K ⥤ D} (G : category_theory.limits.cone F ⥤ category_theory.limits.cone F') [category_theory.limits.reflects_limit (category_theory.functor.empty (category_theory.limits.cone F)) G] {c : category_theory.limits.cone F} (hc : category_theory.limits.is_limit (G.obj c)) :

category_theory.limits.is_limit c

If G : cone F ⥤ cone F' reflects terminal objects, it reflects limit cones.

Equations

category_theory.limits.is_limit.of_reflects_cone_terminal G hc = ⇑(c.is_limit_equiv_is_terminal.symm) (category_theory.limits.is_terminal.is_terminal_of_obj G c (⇑((G.obj c).is_limit_equiv_is_terminal) hc))

source

@[simp]

theorem category_theory.limits.cocone.to_structured_arrow_obj {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cocone F) :

(category_theory.limits.cocone.to_structured_arrow F).obj c = category_theory.structured_arrow.mk c.ι

source

def category_theory.limits.cocone.to_structured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.cocone F ⥤ category_theory.structured_arrow F (category_theory.functor.const J)

Construct an object of the category (F ↓ Δ) from a cocone on F. This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations

category_theory.limits.cocone.to_structured_arrow F = {obj := λ (c : category_theory.limits.cocone F), category_theory.structured_arrow.mk c.ι, map := λ (c d : category_theory.limits.cocone F) (f : c ⟶ d), category_theory.structured_arrow.hom_mk f.hom _, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.cocone.to_structured_arrow_map {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cocone F) (f : c ⟶ d) :

(category_theory.limits.cocone.to_structured_arrow F).map f = category_theory.structured_arrow.hom_mk f.hom _

source

@[simp]

theorem category_theory.limits.cocone.from_structured_arrow_map_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.structured_arrow F (category_theory.functor.const J)) (f : c ⟶ d) :

((category_theory.limits.cocone.from_structured_arrow F).map f).hom = f.right

source

def category_theory.limits.cocone.from_structured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.structured_arrow F (category_theory.functor.const J) ⥤ category_theory.limits.cocone F

Construct a cocone on F from an object of the category (F ↓ Δ). This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations

category_theory.limits.cocone.from_structured_arrow F = {obj := λ (c : category_theory.structured_arrow F (category_theory.functor.const J)), {X := c.right, ι := c.hom}, map := λ (c d : category_theory.structured_arrow F (category_theory.functor.const J)) (f : c ⟶ d), {hom := f.right, w' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.cocone.from_structured_arrow_obj_ι {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.from_structured_arrow F).obj c).ι = c.hom

source

@[simp]

theorem category_theory.limits.cocone.from_structured_arrow_obj_X {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.from_structured_arrow F).obj c).X = c.right

source

def category_theory.limits.cocone.equiv_structured_arrow {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.cocone F ≌ category_theory.structured_arrow F (category_theory.functor.const J)

The category of cocones on F is just the comma category (F ↓ Δ), where Δ is the constant functor.

Equations

category_theory.limits.cocone.equiv_structured_arrow F = category_theory.equivalence.mk (category_theory.limits.cocone.to_structured_arrow F) (category_theory.limits.cocone.from_structured_arrow F) (category_theory.nat_iso.of_components category_theory.limits.cocones.eta _) (category_theory.nat_iso.of_components (λ (c : category_theory.structured_arrow F (category_theory.functor.const J)), c.eta.symm) _)

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).counit_iso.inv.app X).right = 𝟙 X.right

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_unit_iso_hom_app_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.limits.cocone F) :

((category_theory.limits.cocone.equiv_structured_arrow F).unit_iso.hom.app X).hom = 𝟙 X.X

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_ι {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).inverse.obj c).ι = c.hom

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_functor_map_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cocone F) (f : c ⟶ d) :

((category_theory.limits.cocone.equiv_structured_arrow F).functor.map f).right = f.hom

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_functor_map_left_down_down {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.limits.cocone F) (f : c ⟶ d) :

_ = _

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_functor_obj_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cocone F) :

((category_theory.limits.cocone.equiv_structured_arrow F).functor.obj c).right = c.X

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).counit_iso.hom.app X).left = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_unit_iso_inv_app_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.limits.cocone F) :

((category_theory.limits.cocone.equiv_structured_arrow F).unit_iso.inv.app X).hom = 𝟙 X.X

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_X {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).inverse.obj c).X = c.right

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_right {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).counit_iso.hom.app X).right = 𝟙 X.right

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_functor_obj_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c : category_theory.limits.cocone F) :

((category_theory.limits.cocone.equiv_structured_arrow F).functor.obj c).hom = c.ι

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_left {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (X : category_theory.structured_arrow F (category_theory.functor.const J)) :

((category_theory.limits.cocone.equiv_structured_arrow F).counit_iso.inv.app X).left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1

source

@[simp]

theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_map_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) (c d : category_theory.structured_arrow F (category_theory.functor.const J)) (f : c ⟶ d) :

((category_theory.limits.cocone.equiv_structured_arrow F).inverse.map f).hom = f.right

source

def category_theory.limits.cocone.is_colimit_equiv_is_initial {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} (c : category_theory.limits.cocone F) :

category_theory.limits.is_colimit c ≃ category_theory.limits.is_initial c

A cocone is a colimit cocone iff it is initial.

Equations

c.is_colimit_equiv_is_initial = category_theory.limits.is_colimit.iso_unique_cocone_morphism.to_equiv.trans {to_fun := λ (h : Π (s : category_theory.limits.cocone F), unique (c ⟶ s)), category_theory.limits.is_initial.of_unique c, inv_fun := λ (h : category_theory.limits.is_initial c) (s : category_theory.limits.cocone F), {to_inhabited := {default := h.to s}, uniq := _}, left_inv := _, right_inv := _}

source

theorem category_theory.limits.has_colimit_iff_has_initial_cocone {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J ⥤ C) :

category_theory.limits.has_colimit F ↔ category_theory.limits.has_initial (category_theory.limits.cocone F)

source

theorem category_theory.limits.has_colimits_of_shape_iff_is_right_adjoint_const {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] :

category_theory.limits.has_colimits_of_shape J C ↔ nonempty (category_theory.is_right_adjoint (category_theory.functor.const J))

source

theorem category_theory.limits.is_colimit.desc_cocone_morphism_eq_is_initial_to {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} {c : category_theory.limits.cocone F} (hc : category_theory.limits.is_colimit c) (s : category_theory.limits.cocone F) :

hc.desc_cocone_morphism s = (⇑(c.is_colimit_equiv_is_initial) hc).to s

source

theorem category_theory.limits.is_initial.to_eq_desc_cocone_morphism {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J ⥤ C} {c : category_theory.limits.cocone F} (hc : category_theory.limits.is_initial c) (s : category_theory.limits.cocone F) :

hc.to s = (⇑(c.is_colimit_equiv_is_initial.symm) hc).desc_cocone_morphism s

source

def category_theory.limits.is_colimit.of_preserves_cocone_initial {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F : J ⥤ C} {F' : K ⥤ D} (G : category_theory.limits.cocone F ⥤ category_theory.limits.cocone F') [category_theory.limits.preserves_colimit (category_theory.functor.empty (category_theory.limits.cocone F)) G] {c : category_theory.limits.cocone F} (hc : category_theory.limits.is_colimit c) :

category_theory.limits.is_colimit (G.obj c)

If G : cocone F ⥤ cocone F' preserves initial objects, it preserves colimit cocones.

Equations

category_theory.limits.is_colimit.of_preserves_cocone_initial G hc = ⇑((G.obj c).is_colimit_equiv_is_initial.symm) (category_theory.limits.is_initial.is_initial_obj G c (⇑(c.is_colimit_equiv_is_initial) hc))

source

def category_theory.limits.is_colimit.of_reflects_cocone_initial {J : Type u₁} [category_theory.category J] {K : Type u₂} [category_theory.category K] {C : Type u₃} [category_theory.category C] {D : Type u₄} [category_theory.category D] {F : J ⥤ C} {F' : K ⥤ D} (G : category_theory.limits.cocone F ⥤ category_theory.limits.cocone F') [category_theory.limits.reflects_colimit (category_theory.functor.empty (category_theory.limits.cocone F)) G] {c : category_theory.limits.cocone F} (hc : category_theory.limits.is_colimit (G.obj c)) :

category_theory.limits.is_colimit c

If G : cocone F ⥤ cocone F' reflects initial objects, it reflects colimit cocones.

Equations

category_theory.limits.is_colimit.of_reflects_cocone_initial G hc = ⇑(c.is_colimit_equiv_is_initial.symm) (category_theory.limits.is_initial.is_initial_of_obj G c (⇑((G.obj c).is_colimit_equiv_is_initial) hc))

mathlib documentation

Limits and the category of (co)cones #

Main results #