mathlib documentation

category_theory.limits.cones

def category_theory.functor.cones {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] :
J CCᵒᵖ Type v

F.cones is the functor assigning to an object X the type of natural transformations from the constant functor with value X to F. An object representing this functor is a limit of F.

Equations
@[simp]
theorem category_theory.functor.cones_map_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] (F : J C) {X₁ X₂ : Cᵒᵖ} (f : X₁ X₂) (t : F.cones.obj X₁) (j : J) :
(F.cones.map f t).app j = f.unop t.app j

def category_theory.functor.cocones {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] :
J CC Type v

F.cocones is the functor assigning to an object X the type of natural transformations from F to the constant functor with value X. An object corepresenting this functor is a colimit of F.

Equations
@[simp]
theorem category_theory.functor.cocones_map_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] (F : J C) {X₁ X₂ : C} (f : X₁ X₂) (t : F.cocones.obj X₁) (j : J) :
(F.cocones.map f t).app j = t.app j f

@[simp]

def category_theory.cones (J : Type v) [category_theory.small_category J] (C : Type u) [category_theory.category C] :
(J C) Cᵒᵖ Type v

Functorially associated to each functor J ⥤ C, we have the C-presheaf consisting of cones with a given cone point.

Equations
def category_theory.cocones (J : Type v) [category_theory.small_category J] (C : Type u) [category_theory.category C] :
(J C)ᵒᵖ C Type v

Contravariantly associated to each functor J ⥤ C, we have the C-copresheaf consisting of cocones with a given cocone point.

Equations
structure category_theory.limits.cone {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] :
J CType (max u v)

A c : cone F is:

  • an object c.X and
  • a natural transformation c.π : c.X ⟶ F from the constant c.X functor to F.

cone F is equivalent, via cone.equiv below, to Σ X, F.cones.obj X.

@[instance]

Equations
@[simp]
theorem category_theory.limits.cone.w {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {j j' : J} (f : j j') :
c.π.app j F.map f = c.π.app j'

@[simp]
theorem category_theory.limits.cone.w_assoc {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {j j' : J} (f : j j') {X' : C} (f' : F.obj j' X') :
c.π.app j F.map f f' = c.π.app j' f'

structure category_theory.limits.cocone {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] :
J CType (max u v)

A c : cocone F is

  • an object c.X and
  • a natural transformation c.ι : F ⟶ c.X from F to the constant c.X functor.

cocone F is equivalent, via cone.equiv below, to Σ X, F.cocones.obj X.

@[instance]

Equations
@[simp]
theorem category_theory.limits.cocone.w {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (c : category_theory.limits.cocone F) {j j' : J} (f : j j') :
F.map f c.ι.app j' = c.ι.app j

@[simp]
theorem category_theory.limits.cocone.w_assoc {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (c : category_theory.limits.cocone F) {j j' : J} (f : j j') {X' : C} (f' : ((category_theory.functor.const J).obj c.X).obj j' X') :
F.map f c.ι.app j' f' = c.ι.app j f'

The isomorphism between a cone on F and an element of the functor F.cones.

Equations
@[simp]

A map to the vertex of a cone naturally induces a cone by composition.

Equations
@[simp]

A map to the vertex of a cone induces a cone by composition.

Equations
@[simp]

Whisker a cone by precomposition of a functor.

Equations

The isomorphism between a cocone on F and an element of the functor F.cocones.

Equations
@[simp]

A map from the vertex of a cocone naturally induces a cocone by composition.

Equations
@[simp]

A map from the vertex of a cocone induces a cocone by composition.

Equations
@[simp]
theorem category_theory.limits.cocone.extend_ι {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (c : category_theory.limits.cocone F) {X : C} (f : c.X X) :
(c.extend f).ι = c.extensions.app X f

Whisker a cocone by precomposition of a functor. See whiskering for a functorial version.

Equations
theorem category_theory.limits.cone_morphism.ext {J : Type v} {_inst_1 : category_theory.small_category J} {C : Type u} {_inst_2 : category_theory.category C} {F : J C} {A B : category_theory.limits.cone F} (x y : category_theory.limits.cone_morphism A B) :
x.hom = y.homx = y

@[ext]

A cone morphism between two cones for the same diagram is a morphism of the cone points which commutes with the cone legs.

@[simp]
theorem category_theory.limits.cone_morphism.w_assoc {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {A B : category_theory.limits.cone F} (c : category_theory.limits.cone_morphism A B) (j : J) {X' : C} (f' : F.obj j X') :
c.hom B.π.app j f' = A.π.app j f'

@[simp]

@[instance]

The category of cones on a given diagram.

Equations
@[simp]
theorem category_theory.limits.cones.ext_inv_hom {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cone F} (φ : c.X c'.X) (w : ∀ (j : J), c.π.app j = φ.hom c'.π.app j) :

@[ext]
def category_theory.limits.cones.ext {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cone F} (φ : c.X c'.X) :
(∀ (j : J), c.π.app j = φ.hom c'.π.app j)(c c')

To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.

Equations
@[simp]
theorem category_theory.limits.cones.ext_hom_hom {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cone F} (φ : c.X c'.X) (w : ∀ (j : J), c.π.app j = φ.hom c'.π.app j) :

Given a cone morphism whose object part is an isomorphism, produce an isomorphism of cones.

Equations

Functorially postcompose a cone for F by a natural transformation F ⟶ G to give a cone for G.

Equations
@[simp]

Whiskering on the left by E : K ⥤ J gives a functor from cone F to cone (E ⋙ F).

Equations

The categories of cones over F and G are equivalent if F and G are naturally isomorphic (possibly after changing the indexing category by an equivalence).

Equations

Forget the cone structure and obtain just the cone point.

Equations

A functor G : C ⥤ D sends cones over F to cones over F ⋙ G functorially.

Equations
@[ext]

A cocone morphism between two cocones for the same diagram is a morphism of the cocone points which commutes with the cocone legs.

theorem category_theory.limits.cocone_morphism.ext {J : Type v} {_inst_1 : category_theory.small_category J} {C : Type u} {_inst_2 : category_theory.category C} {F : J C} {A B : category_theory.limits.cocone F} (x y : category_theory.limits.cocone_morphism A B) :
x.hom = y.homx = y

@[simp]
theorem category_theory.limits.cocone_morphism.w_assoc {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {A B : category_theory.limits.cocone F} (c : category_theory.limits.cocone_morphism A B) (j : J) {X' : C} (f' : B.X X') :
A.ι.app j c.hom f' = B.ι.app j f'

@[simp]
theorem category_theory.limits.cocone.category_to_category_struct_comp_hom {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} (_x _x_1 _x_2 : category_theory.limits.cocone F) (f : _x _x_1) (g : _x_1 _x_2) :
(f g).hom = f.hom g.hom

@[simp]
theorem category_theory.limits.cocones.ext_inv_hom {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cocone F} (φ : c.X c'.X) (w : ∀ (j : J), c.ι.app j φ.hom = c'.ι.app j) :

@[ext]
def category_theory.limits.cocones.ext {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cocone F} (φ : c.X c'.X) :
(∀ (j : J), c.ι.app j φ.hom = c'.ι.app j)(c c')

To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

Equations
@[simp]
theorem category_theory.limits.cocones.ext_hom_hom {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {F : J C} {c c' : category_theory.limits.cocone F} (φ : c.X c'.X) (w : ∀ (j : J), c.ι.app j φ.hom = c'.ι.app j) :

Given a cocone morphism whose object part is an isomorphism, produce an isomorphism of cocones.

Equations

Functorially precompose a cocone for F by a natural transformation G ⟶ F to give a cocone for G.

Equations
@[simp]

Whiskering on the left by E : K ⥤ J gives a functor from cocone F to cocone (E ⋙ F).

Equations

The categories of cocones over F and G are equivalent if F and G are naturally isomorphic (possibly after changing the indexing category by an equivalence).

Equations

Forget the cocone structure and obtain just the cocone point.

Equations

A functor G : C ⥤ D sends cocones over F to cocones over F ⋙ G functorially.

Equations

The image of a cone in C under a functor G : C ⥤ D is a cone in D.

Equations

The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.

Equations
@[simp]
theorem category_theory.functor.map_cone_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) (c : category_theory.limits.cone F) :
(H.map_cone c).X = H.obj c.X

@[simp]
theorem category_theory.functor.map_cocone_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) (c : category_theory.limits.cocone F) :
(H.map_cocone c).X = H.obj c.X

def category_theory.functor.map_cone_morphism {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) {c c' : category_theory.limits.cone F} :
(c c')(H.map_cone c H.map_cone c')

Given a cone morphism c ⟶ c', construct a cone morphism on the mapped cones functorially.

Equations
def category_theory.functor.map_cocone_morphism {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) {c c' : category_theory.limits.cocone F} :
(c c')(H.map_cocone c H.map_cocone c')

Given a cocone morphism c ⟶ c', construct a cocone morphism on the mapped cocones functorially.

Equations
@[simp]
theorem category_theory.functor.map_cone_π {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) (c : category_theory.limits.cone F) (j : J) :
(H.map_cone c).π.app j = H.map (c.π.app j)

@[simp]
theorem category_theory.functor.map_cocone_ι {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] {F : J C} (H : C D) (c : category_theory.limits.cocone F) (j : J) :
(H.map_cocone c).ι.app j = H.map (c.ι.app j)

If H is an equivalence, we invert H.map_cone and get a cone for F from a cone for F ⋙ H.

Equations

If H is an equivalence, we invert H.map_cone and get a cone for F from a cone for F ⋙ H.

Equations

Change a cocone F into a cone F.op.

Equations

Change a cone F into a cocone F.op.

Equations

Change a cocone F.op into a cone F.

Equations

Change a cone F.op into a cocone F.

Equations

The opposite cocone of the image of a cone is the image of the opposite cocone.

Equations

The opposite cone of the image of a cocone is the image of the opposite cone.

Equations