mathlib3 documentation

category_theory.limits.cones

Cones and cocones #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define cone F, a cone over a functor F, and F.cones : Cᵒᵖ ⥤ Type, the functor associating to X the cones over F with cone point X.

A cone c is defined by specifying its cone point c.X and a natural transformation c.π from the constant c.X valued functor to F.

We provide c.w f : c.π.app j ≫ F.map f = c.π.app j' for any f : j ⟶ j' as a wrapper for c.π.naturality f avoiding unneeded identity morphisms.

We define c.extend f, where c : cone F and f : Y ⟶ c.X for some other Y, which replaces the cone point by Y and inserts f into each of the components of the cone. Similarly we have c.whisker F producing a cone (E ⋙ F)

We define morphisms of cones, and the category of cones.

We define cone.postcompose α : cone F ⥤ cone G for α a natural transformation F ⟶ G.

And, of course, we dualise all this to cocones as well.

For more results about the category of cones, see cone_category.lean.

@[simp]
theorem category_theory.functor.cones_map_app {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) (_x _x_1 : Cᵒᵖ) (f : _x _x_1) (ᾰ : (category_theory.yoneda.obj F).obj ((category_theory.functor.const J).op.obj _x)) (X : J) :
(F.cones.map f ᾰ).app X = f.unop ᾰ.app X
def category_theory.functor.cones {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) :
Cᵒᵖ Type (max u₁ 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.cocones_map_app {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) (_x _x_1 : C) (f : _x _x_1) (ᾰ : (category_theory.coyoneda.obj (opposite.op F)).obj ((category_theory.functor.const J).obj _x)) (X : J) :
(F.cocones.map f ᾰ).app X = ᾰ.app X f
def category_theory.functor.cocones {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) :
C Type (max u₁ 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]
def category_theory.cones (J : Type u₁) [category_theory.category J] (C : Type u₃) [category_theory.category C] :
(J C) Cᵒᵖ Type (max u₁ 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 u₁) [category_theory.category J] (C : Type u₃) [category_theory.category C] :
(J C)ᵒᵖ C Type (max u₁ 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 u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) :
Type (max u₁ 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.

Instances for category_theory.limits.cone
@[protected, instance]
Equations
@[simp]
theorem category_theory.limits.cone.w {J : Type u₁} [category_theory.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 u₁} [category_theory.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 u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] (F : J C) :
Type (max u₁ 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.

Instances for category_theory.limits.cocone
@[protected, instance]
Equations
@[simp]
theorem category_theory.limits.cocone.w {J : Type u₁} [category_theory.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 u₁} [category_theory.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]
theorem category_theory.limits.cone.extend_X {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {X : C} (f : X c.X) :
(c.extend f).X = X
@[simp]
theorem category_theory.limits.cone.extend_π {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {X : C} (f : X c.X) :
(c.extend f).π = c.extensions.app (opposite.op X) {down := f}

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

Equations

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]
theorem category_theory.limits.cocone.extend_ι {J : Type u₁} [category_theory.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 {down := f}
@[simp]
theorem category_theory.limits.cocone.extend_X {J : Type u₁} [category_theory.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).X = X

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

Equations

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

Equations
theorem category_theory.limits.cone_morphism.ext {J : Type u₁} {_inst_1 : category_theory.category J} {C : Type u₃} {_inst_3 : category_theory.category C} {F : J C} {A B : category_theory.limits.cone F} (x y : category_theory.limits.cone_morphism A B) (h : x.hom = y.hom) :
x = 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.

Instances for category_theory.limits.cone_morphism
@[simp]
theorem category_theory.limits.cone_morphism.w_assoc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {A B : category_theory.limits.cone F} (self : category_theory.limits.cone_morphism A B) (j : J) {X' : C} (f' : F.obj j X') :
self.hom B.π.app j f' = A.π.app j f'
@[simp]
theorem category_theory.limits.cone.category_comp_hom {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (X Y Z : category_theory.limits.cone F) (f : X Y) (g : Y Z) :
(f g).hom = f.hom g.hom
@[protected, instance]

The category of cones on a given diagram.

Equations
@[simp]
theorem category_theory.limits.cones.ext_inv_hom {J : Type u₁} [category_theory.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 u₁} [category_theory.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) :
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 u₁} [category_theory.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.

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
Instances for category_theory.limits.cones.functoriality
@[protected, instance]

If F reflects isomorphisms, then cones.functoriality F reflects isomorphisms as well.

@[ext]

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

Instances for category_theory.limits.cocone_morphism
@[simp]
theorem category_theory.limits.cocone_morphism.w_assoc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {A B : category_theory.limits.cocone F} (self : category_theory.limits.cocone_morphism A B) (j : J) {X' : C} (f' : B.X X') :
A.ι.app j self.hom f' = B.ι.app j f'
@[simp]
theorem category_theory.limits.cocone.category_comp_hom {J : Type u₁} [category_theory.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 u₁} [category_theory.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 u₁} [category_theory.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) :
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 u₁} [category_theory.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.

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

Equations

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
Instances for category_theory.limits.cocones.functoriality
@[protected, instance]

If F reflects isomorphisms, then cocones.functoriality F reflects isomorphisms as well.

@[simp]
theorem category_theory.functor.map_cone_π_app {J : Type u₁} [category_theory.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)

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

Equations
@[simp]
theorem category_theory.functor.map_cone_X {J : Type u₁} [category_theory.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_ι_app {J : Type u₁} [category_theory.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)
@[simp]

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

Equations

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

Equations

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

Equations

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

For F : J ⥤ C, given a cone c : cone F, and a natural isomorphism α : H ≅ H' for functors H H' : C ⥤ D, the postcomposition of the cone H.map_cone using the isomorphism α is isomorphic to the cone H'.map_cone.

Equations

map_cone commutes with postcompose. In particular, for F : J ⥤ C, given a cone c : cone F, a natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious ways of producing a cone over G ⋙ H, and they are both isomorphic.

Equations

For F : J ⥤ C, given a cocone c : cocone F, and a natural isomorphism α : H ≅ H' for functors H H' : C ⥤ D, the precomposition of the cocone H.map_cocone using the isomorphism α is isomorphic to the cocone H'.map_cocone.

Equations

map_cocone commutes with precompose. In particular, for F : J ⥤ C, given a cocone c : cocone F, a natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious ways of producing a cocone over G ⋙ H, and they are both isomorphic.

Equations

Change a cocone F into a cone F.op.

Equations

Change a cone F into a cocone F.op.

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