# mathlibdocumentation

category_theory.limits.cones

# Cones and cocones #

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₁} {C : Type u₃} (F : J C) (_x _x_1 : Cᵒᵖ) (f : _x _x_1) (ᾰ : _x)) (X : J) :
(F.cones.map f ᾰ).app X = f.unop ᾰ.app X
def category_theory.functor.cones {J : Type u₁} {C : Type u₃} (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.cones_obj {J : Type u₁} {C : Type u₃} (F : J C) (X : Cᵒᵖ) :
F.cones.obj X = F)
@[simp]
theorem category_theory.functor.cocones_map_app {J : Type u₁} {C : Type u₃} (F : J C) (_x _x_1 : C) (f : _x _x_1) (ᾰ : _x)) (X : J) :
(F.cocones.map f ᾰ).app X = ᾰ.app X f
def category_theory.functor.cocones {J : Type u₁} {C : Type u₃} (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]
theorem category_theory.functor.cocones_obj {J : Type u₁} {C : Type u₃} (F : J C) (X : C) :
F.cocones.obj X = (F
@[simp]
theorem category_theory.cones_map (J : Type u₁) (C : Type u₃) (F G : J C) (f : F G) :
@[simp]
theorem category_theory.cones_obj (J : Type u₁) (C : Type u₃) (F : J C) :
.obj F = F.cones
def category_theory.cones (J : Type u₁) (C : Type u₃)  :
(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
@[simp]
theorem category_theory.cocones_map (J : Type u₁) (C : Type u₃) (F G : (J C)ᵒᵖ) (f : F G) :
@[simp]
theorem category_theory.cocones_obj (J : Type u₁) (C : Type u₃) (F : (J C)ᵒᵖ) :
def category_theory.cocones (J : Type u₁) (C : Type u₃)  :
(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₁} {C : Type u₃} (F : J C) :
Type (max u₁ u₃ v₃)
• X : C
• π : self.X F

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]
def category_theory.limits.inhabited_cone {C : Type u₃}  :
Equations
• = {default := {X := F.obj {as := punit.star}, π := {app := λ (_x : , category_theory.limits.inhabited_cone._match_1 F _x, naturality' := _}}}
• category_theory.limits.inhabited_cone._match_1 F {as := punit.star} = 𝟙 (F.obj {as := punit.star})).obj {as := punit.star})
@[simp]
theorem category_theory.limits.cone.w {J : Type u₁} {C : Type u₃} {F : J C} {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₁} {C : Type u₃} {F : J C} {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₁} {C : Type u₃} (F : J C) :
Type (max u₁ u₃ v₃)
• X : C
• ι : F self.X

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]
def category_theory.limits.inhabited_cocone {C : Type u₃}  :
Equations
• = {default := {X := F.obj {as := punit.star}, ι := {app := λ (_x : , category_theory.limits.inhabited_cocone._match_1 F _x, naturality' := _}}}
• category_theory.limits.inhabited_cocone._match_1 F {as := punit.star} = 𝟙 (F.obj {as := punit.star})
@[simp]
theorem category_theory.limits.cocone.w {J : Type u₁} {C : Type u₃} {F : J C} {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₁} {C : Type u₃} {F : J C} {j j' : J} (f : j j') {X' : C} (f' : c.X).obj j' X') :
F.map f c.ι.app j' f' = c.ι.app j f'
@[simp]
theorem category_theory.limits.cone.equiv_hom_snd {J : Type u₁} {C : Type u₃} (F : J C)  :
.snd = c.π
@[simp]
theorem category_theory.limits.cone.equiv_inv_X {J : Type u₁} {C : Type u₃} (F : J C) (c : Σ (X : Cᵒᵖ), F.cones.obj X) :
@[simp]
theorem category_theory.limits.cone.equiv_hom_fst {J : Type u₁} {C : Type u₃} (F : J C)  :
.fst =
def category_theory.limits.cone.equiv {J : Type u₁} {C : Type u₃} (F : J C) :
Σ (X : Cᵒᵖ), F.cones.obj X

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

Equations
@[simp]
theorem category_theory.limits.cone.equiv_inv_π {J : Type u₁} {C : Type u₃} (F : J C) (c : Σ (X : Cᵒᵖ), F.cones.obj X) :
.π = c.snd
@[simp]
theorem category_theory.limits.cone.extensions_app {J : Type u₁} {C : Type u₃} {F : J C} (X : Cᵒᵖ) (f : X) :
def category_theory.limits.cone.extensions {J : Type u₁} {C : Type u₃} {F : J C}  :

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

Equations
@[simp]
theorem category_theory.limits.cone.extend_X {J : Type u₁} {C : Type u₃} {F : J C} {X : C} (f : X c.X) :
(c.extend f).X = X
@[simp]
theorem category_theory.limits.cone.extend_π {J : Type u₁} {C : Type u₃} {F : J C} {X : C} (f : X c.X) :
(c.extend f).π = c.extensions.app (opposite.op X) {down := f}
def category_theory.limits.cone.extend {J : Type u₁} {C : Type u₃} {F : J C} {X : C} (f : X c.X) :

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

Equations
@[simp]
theorem category_theory.limits.cone.whisker_X {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
@[simp]
theorem category_theory.limits.cone.whisker_π {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
def category_theory.limits.cone.whisker {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :

Whisker a cone by precomposition of a functor.

Equations
def category_theory.limits.cocone.equiv {J : Type u₁} {C : Type u₃} (F : J C) :
Σ (X : C), F.cocones.obj X

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

Equations
def category_theory.limits.cocone.extensions {J : Type u₁} {C : Type u₃} {F : J C}  :

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

Equations
@[simp]
theorem category_theory.limits.cocone.extensions_app {J : Type u₁} {C : Type u₃} {F : J C} (X : C) (f : X) :
c.extensions.app X f = c.ι
@[simp]
theorem category_theory.limits.cocone.extend_ι {J : Type u₁} {C : Type u₃} {F : J C} {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₁} {C : Type u₃} {F : J C} {X : C} (f : c.X X) :
(c.extend f).X = X
def category_theory.limits.cocone.extend {J : Type u₁} {C : Type u₃} {F : J C} {X : C} (f : c.X X) :

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

Equations
@[simp]
theorem category_theory.limits.cocone.whisker_ι {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
def category_theory.limits.cocone.whisker {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :

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

Equations
@[simp]
theorem category_theory.limits.cocone.whisker_X {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
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 : B) (h : x.hom = y.hom) :
x = y
theorem category_theory.limits.cone_morphism.ext_iff {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 : B) :
x = y x.hom = y.hom
@[ext]
structure category_theory.limits.cone_morphism {J : Type u₁} {C : Type u₃} {F : J C} (A B : category_theory.limits.cone F) :
Type v₃

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 {J : Type u₁} {C : Type u₃} {F : J C} {A B : category_theory.limits.cone F} (self : B) (j : J) :
self.hom B.π.app j = A.π.app j
@[simp]
theorem category_theory.limits.cone_morphism.w_assoc {J : Type u₁} {C : Type u₃} {F : J C} {A B : category_theory.limits.cone F} (self : B) (j : J) {X' : C} (f' : F.obj j X') :
self.hom B.π.app j f' = A.π.app j f'
@[protected, instance]
def category_theory.limits.inhabited_cone_morphism {J : Type u₁} {C : Type u₃} {F : J C}  :
Equations
@[simp]
theorem category_theory.limits.cone.category_comp_hom {J : Type u₁} {C : Type u₃} {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]
def category_theory.limits.cone.category {J : Type u₁} {C : Type u₃} {F : J C} :

The category of cones on a given diagram.

Equations
@[simp]
theorem category_theory.limits.cone.category_id_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
(𝟙 B).hom = 𝟙 B.X
@[simp]
theorem category_theory.limits.cone.category_hom {J : Type u₁} {C : Type u₃} {F : J C} (A B : category_theory.limits.cone F) :
(A B) =
@[simp]
theorem category_theory.limits.cones.ext_inv_hom {J : Type u₁} {C : Type u₃} {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₁} {C : Type u₃} {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₁} {C : Type u₃} {F : J C} {c c' : category_theory.limits.cone F} (φ : c.X c'.X) (w : ∀ (j : J), c.π.app j = φ.hom c'.π.app j) :
@[simp]
theorem category_theory.limits.cones.eta_inv_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
@[simp]
theorem category_theory.limits.cones.eta_hom_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
def category_theory.limits.cones.eta {J : Type u₁} {C : Type u₃} {F : J C}  :
c {X := c.X, π := c.π}

Eta rule for cones.

Equations
theorem category_theory.limits.cones.cone_iso_of_hom_iso {J : Type u₁} {C : Type u₃} {K : J C} {c d : category_theory.limits.cone K} (f : c d) [i : category_theory.is_iso f.hom] :

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

@[simp]
theorem category_theory.limits.cones.postcompose_obj_X {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G)  :
= c.X
@[simp]
theorem category_theory.limits.cones.postcompose_obj_π {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G)  :
= c.π α
def category_theory.limits.cones.postcompose {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :

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

Equations
@[simp]
theorem category_theory.limits.cones.postcompose_map_hom {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) (c₁ c₂ : category_theory.limits.cone F) (f : c₁ c₂) :
def category_theory.limits.cones.postcompose_comp {J : Type u₁} {C : Type u₃} {F G H : J C} (α : F G) (β : G H) :

Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as postcomposing by `α` and then by `β`.

Equations
@[simp]
theorem category_theory.limits.cones.postcompose_comp_hom_app_hom {J : Type u₁} {C : Type u₃} {F G H : J C} (α : F G) (β : G H)  :
= 𝟙 X.X
@[simp]
theorem category_theory.limits.cones.postcompose_comp_inv_app_hom {J : Type u₁} {C : Type u₃} {F G H : J C} (α : F G) (β : G H)  :
= 𝟙 X.X
@[simp]
theorem category_theory.limits.cones.postcompose_id_hom_app_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
@[simp]
theorem category_theory.limits.cones.postcompose_id_inv_app_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
def category_theory.limits.cones.postcompose_id {J : Type u₁} {C : Type u₃} {F : J C} :

Postcomposing by the identity does not change the cone up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_functor {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :
@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_unit_iso {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :
@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_inverse {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :
def category_theory.limits.cones.postcompose_equivalence {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :

If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of cones.

Equations
@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_counit_iso {J : Type u₁} {C : Type u₃} {F G : J C} (α : F G) :
@[simp]
theorem category_theory.limits.cones.whiskering_map_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J) (c c' : category_theory.limits.cone F) (f : c c') :
def category_theory.limits.cones.whiskering {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J) :

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

Equations
@[simp]
theorem category_theory.limits.cones.whiskering_obj {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_counit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_inverse {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_unit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
def category_theory.limits.cones.whiskering_equivalence {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :

Whiskering by an equivalence gives an equivalence between categories of cones.

Equations
@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_functor {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cones.equivalence_of_reindexing_functor {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :
def category_theory.limits.cones.equivalence_of_reindexing {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :

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
@[simp]
theorem category_theory.limits.cones.equivalence_of_reindexing_counit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :
@[simp]
theorem category_theory.limits.cones.equivalence_of_reindexing_unit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :
@[simp]
theorem category_theory.limits.cones.equivalence_of_reindexing_inverse {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :
@[simp]
theorem category_theory.limits.cones.forget_map {J : Type u₁} {C : Type u₃} (F : J C) (s t : category_theory.limits.cone F) (f : s t) :
@[simp]
theorem category_theory.limits.cones.forget_obj {J : Type u₁} {C : Type u₃} (F : J C)  :
def category_theory.limits.cones.forget {J : Type u₁} {C : Type u₃} (F : J C) :

Forget the cone structure and obtain just the cone point.

Equations
def category_theory.limits.cones.functoriality {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) :

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

Equations
Instances for `category_theory.limits.cones.functoriality`
@[simp]
theorem category_theory.limits.cones.functoriality_obj_X {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
.X = G.obj A.X
@[simp]
theorem category_theory.limits.cones.functoriality_map_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) (X Y : category_theory.limits.cone F) (f : X Y) :
.hom = G.map f.hom
@[simp]
theorem category_theory.limits.cones.functoriality_obj_π_app {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) (j : J) :
.π.app j = G.map (A.π.app j)
@[protected, instance]
def category_theory.limits.cones.functoriality_full {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
Equations
@[protected, instance]
def category_theory.limits.cones.functoriality_faithful {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_inverse {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_unit_iso {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
def category_theory.limits.cones.functoriality_equivalence {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :

If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an equivalence between cones over `F` and cones over `F ⋙ e.functor`.

Equations
@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_counit_iso {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_functor {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[protected, instance]
def category_theory.limits.cones.reflects_cone_isomorphism {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : C D) (K : J C) :

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

theorem category_theory.limits.cocone_morphism.ext_iff {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.cocone F} (x y : B) :
x = y x.hom = y.hom
@[ext]
structure category_theory.limits.cocone_morphism {J : Type u₁} {C : Type u₃} {F : J C} (A B : category_theory.limits.cocone F) :
Type v₃

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`
theorem category_theory.limits.cocone_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.cocone F} (x y : B) (h : x.hom = y.hom) :
x = y
@[protected, instance]
def category_theory.limits.inhabited_cocone_morphism {J : Type u₁} {C : Type u₃} {F : J C}  :
Equations
@[simp]
theorem category_theory.limits.cocone_morphism.w {J : Type u₁} {C : Type u₃} {F : J C} {A B : category_theory.limits.cocone F} (self : B) (j : J) :
A.ι.app j self.hom = B.ι.app j
@[simp]
theorem category_theory.limits.cocone_morphism.w_assoc {J : Type u₁} {C : Type u₃} {F : J C} {A B : category_theory.limits.cocone F} (self : 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₁} {C : Type u₃} {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.cocone.category_hom {J : Type u₁} {C : Type u₃} {F : J C} (A B : category_theory.limits.cocone F) :
(A B) =
@[protected, instance]
def category_theory.limits.cocone.category {J : Type u₁} {C : Type u₃} {F : J C} :
Equations
@[simp]
theorem category_theory.limits.cocone.category_id_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
(𝟙 B).hom = 𝟙 B.X
@[simp]
theorem category_theory.limits.cocones.ext_inv_hom {J : Type u₁} {C : Type u₃} {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₁} {C : Type u₃} {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₁} {C : Type u₃} {F : J C} {c c' : category_theory.limits.cocone F} (φ : c.X c'.X) (w : ∀ (j : J), c.ι.app j φ.hom = c'.ι.app j) :
@[simp]
theorem category_theory.limits.cocones.eta_hom_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
def category_theory.limits.cocones.eta {J : Type u₁} {C : Type u₃} {F : J C}  :
c {X := c.X, ι := c.ι}

Eta rule for cocones.

Equations
@[simp]
theorem category_theory.limits.cocones.eta_inv_hom {J : Type u₁} {C : Type u₃} {F : J C}  :
theorem category_theory.limits.cocones.cocone_iso_of_hom_iso {J : Type u₁} {C : Type u₃} {K : J C} {c d : category_theory.limits.cocone K} (f : c d) [i : category_theory.is_iso f.hom] :

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

def category_theory.limits.cocones.precompose {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :

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

Equations
@[simp]
theorem category_theory.limits.cocones.precompose_obj_ι {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F)  :
= α c.ι
@[simp]
theorem category_theory.limits.cocones.precompose_map_hom {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) (c₁ c₂ : category_theory.limits.cocone F) (f : c₁ c₂) :
@[simp]
theorem category_theory.limits.cocones.precompose_obj_X {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F)  :
= c.X
def category_theory.limits.cocones.precompose_comp {J : Type u₁} {C : Type u₃} {F G H : J C} (α : F G) (β : G H) :

Precomposing a cocone by the composite natural transformation `α ≫ β` is the same as precomposing by `β` and then by `α`.

Equations
def category_theory.limits.cocones.precompose_id {J : Type u₁} {C : Type u₃} {F : J C} :

Precomposing by the identity does not change the cocone up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_functor {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :
@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_inverse {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :
def category_theory.limits.cocones.precompose_equivalence {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :

If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of cocones.

Equations
@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_counit_iso {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :
@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_unit_iso {J : Type u₁} {C : Type u₃} {F G : J C} (α : G F) :
def category_theory.limits.cocones.whiskering {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J) :

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

Equations
@[simp]
theorem category_theory.limits.cocones.whiskering_map_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J) (c c' : category_theory.limits.cocone F) (f : c c') :
@[simp]
theorem category_theory.limits.cocones.whiskering_obj {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (E : K J)  :
def category_theory.limits.cocones.whiskering_equivalence {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :

Whiskering by an equivalence gives an equivalence between categories of cones.

Equations
@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_inverse {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_unit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_functor {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_counit_iso {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} (e : K J) :
@[simp]
theorem category_theory.limits.cocones.equivalence_of_reindexing_functor_obj {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G)  :
def category_theory.limits.cocones.equivalence_of_reindexing {J : Type u₁} {K : Type u₂} {C : Type u₃} {F : J C} {G : K C} (e : K J) (α : e.functor F G) :

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
def category_theory.limits.cocones.forget {J : Type u₁} {C : Type u₃} (F : J C) :

Forget the cocone structure and obtain just the cocone point.

Equations
@[simp]
theorem category_theory.limits.cocones.forget_map {J : Type u₁} {C : Type u₃} (F : J C) (s t : category_theory.limits.cocone F) (f : s t) :
@[simp]
theorem category_theory.limits.cocones.forget_obj {J : Type u₁} {C : Type u₃} (F : J C)  :
def category_theory.limits.cocones.functoriality {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) :

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

Equations
Instances for `category_theory.limits.cocones.functoriality`
@[simp]
theorem category_theory.limits.cocones.functoriality_map_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) (_x _x_1 : category_theory.limits.cocone F) (f : _x _x_1) :
= G.map f.hom
@[simp]
theorem category_theory.limits.cocones.functoriality_obj_ι_app {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D) (j : J) :
.ι.app j = G.map (A.ι.app j)
@[simp]
theorem category_theory.limits.cocones.functoriality_obj_X {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
.X = G.obj A.X
@[protected, instance]
def category_theory.limits.cocones.functoriality_full {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
Equations
@[protected, instance]
def category_theory.limits.cocones.functoriality_faithful {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (G : C D)  :
@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_inverse {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_functor {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
def category_theory.limits.cocones.functoriality_equivalence {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :

If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an equivalence between cocones over `F` and cocones over `F ⋙ e.functor`.

Equations
@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_counit_iso {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_unit_iso {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : J C) (e : C D) :
@[protected, instance]
def category_theory.limits.cocones.reflects_cocone_isomorphism {J : Type u₁} {C : Type u₃} {D : Type u₄} (F : C D) (K : J C) :

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

@[simp]
theorem category_theory.functor.map_cone_π_app {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) (j : J) :
(H.map_cone c).π.app j = H.map (c.π.app j)
def category_theory.functor.map_cone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D)  :

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₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D)  :
(H.map_cone c).X = H.obj c.X
@[simp]
theorem category_theory.functor.map_cocone_ι_app {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) (j : J) :
(H.map_cocone c).ι.app j = H.map (c.ι.app j)
@[simp]
theorem category_theory.functor.map_cocone_X {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D)  :
(H.map_cocone c).X = H.obj c.X
def category_theory.functor.map_cocone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D)  :

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

Equations
def category_theory.functor.map_cone_morphism {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {c c' : category_theory.limits.cone F} (f : c 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 u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {c c' : category_theory.limits.cocone F} (f : c c') :

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

Equations
def category_theory.functor.map_cone_inv {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) (c : category_theory.limits.cone (F H)) :

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

Equations
def category_theory.functor.map_cone_map_cone_inv {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J D} (H : D C) (c : category_theory.limits.cone (F H)) :

`map_cone` is the left inverse to `map_cone_inv`.

Equations
def category_theory.functor.map_cone_inv_map_cone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J D} (H : D C)  :

`map_cone` is the right inverse to `map_cone_inv`.

Equations
def category_theory.functor.map_cocone_inv {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) (c : category_theory.limits.cocone (F H)) :

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

Equations
def category_theory.functor.map_cocone_map_cocone_inv {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J D} (H : D C) (c : category_theory.limits.cocone (F H)) :

`map_cocone` is the left inverse to `map_cocone_inv`.

Equations
def category_theory.functor.map_cocone_inv_map_cocone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J D} (H : D C)  :

`map_cocone` is the right inverse to `map_cocone_inv`.

Equations
@[simp]
theorem category_theory.functor.functoriality_comp_postcompose_inv_app_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
@[simp]
theorem category_theory.functor.functoriality_comp_postcompose_hom_app_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
def category_theory.functor.functoriality_comp_postcompose {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H') :

`functoriality F _ ⋙ postcompose (whisker_left F _)` simplifies to `functoriality F _`.

Equations
@[simp]
theorem category_theory.functor.postcompose_whisker_left_map_cone_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
@[simp]
theorem category_theory.functor.postcompose_whisker_left_map_cone_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
def category_theory.functor.postcompose_whisker_left_map_cone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :

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
def category_theory.functor.map_cone_postcompose {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :

`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
@[simp]
theorem category_theory.functor.map_cone_postcompose_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
@[simp]
theorem category_theory.functor.map_cone_postcompose_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
@[simp]
theorem category_theory.functor.map_cone_postcompose_equivalence_functor_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
def category_theory.functor.map_cone_postcompose_equivalence_functor {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :

`map_cone` commutes with `postcompose_equivalence`

Equations
@[simp]
theorem category_theory.functor.map_cone_postcompose_equivalence_functor_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
def category_theory.functor.functoriality_comp_precompose {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H') :

`functoriality F _ ⋙ precompose (whisker_left F _)` simplifies to `functoriality F _`.

Equations
@[simp]
theorem category_theory.functor.functoriality_comp_precompose_inv_app_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
@[simp]
theorem category_theory.functor.functoriality_comp_precompose_hom_app_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
def category_theory.functor.precompose_whisker_left_map_cocone {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :

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
@[simp]
theorem category_theory.functor.precompose_whisker_left_map_cocone_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
@[simp]
theorem category_theory.functor.precompose_whisker_left_map_cocone_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F : J C} {H H' : C D} (α : H H')  :
@[simp]
theorem category_theory.functor.map_cocone_precompose_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
@[simp]
theorem category_theory.functor.map_cocone_precompose_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
def category_theory.functor.map_cocone_precompose {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :

`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
@[simp]
theorem category_theory.functor.map_cocone_precompose_equivalence_functor_hom_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
@[simp]
theorem category_theory.functor.map_cocone_precompose_equivalence_functor_inv_hom {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :
def category_theory.functor.map_cocone_precompose_equivalence_functor {J : Type u₁} {C : Type u₃} {D : Type u₄} {F G : J C} (H : C D) {α : F G}  :

`map_cocone` commutes with `precompose_equivalence`

Equations
def category_theory.functor.map_cone_whisker {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :

`map_cone` commutes with `whisker`

Equations
@[simp]
theorem category_theory.functor.map_cone_whisker_hom_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :
@[simp]
theorem category_theory.functor.map_cone_whisker_inv_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :
@[simp]
theorem category_theory.functor.map_cocone_whisker_inv_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :
def category_theory.functor.map_cocone_whisker {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :

`map_cocone` commutes with `whisker`

Equations
@[simp]
theorem category_theory.functor.map_cocone_whisker_hom_hom {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} (H : C D) {E : K J}  :
@[simp]
theorem category_theory.limits.cocone.op_X {J : Type u₁} {C : Type u₃} {F : J C}  :
c.op.X =
@[simp]
theorem category_theory.limits.cocone.op_π {J : Type u₁} {C : Type u₃} {F : J C}  :
def category_theory.limits.cocone.op {J : Type u₁} {C : Type u₃} {F : J C}  :

Change a `cocone F` into a `cone F.op`.

Equations
def category_theory.limits.cone.op {J : Type u₁} {C : Type u₃} {F : J C}  :

Change a `cone F` into a `cocone F.op`.

Equations
@[simp]
theorem category_theory.limits.cone.op_ι {J : Type u₁} {C : Type u₃} {F : J C}  :
@[simp]
theorem category_theory.limits.cone.op_X {J : Type u₁} {C : Type u₃} {F : J C}  :
c.op.X =
@[simp]
theorem category_theory.limits.cocone.unop_π {J : Type u₁} {C : Type u₃} {F : J C}  :
@[simp]
theorem category_theory.limits.cocone.unop_X {J : Type u₁} {C : Type u₃} {F : J C}  :
c.unop.X =
def category_theory.limits.cocone.unop {J : Type u₁} {C : Type u₃} {F : J C}  :

Change a `cocone F.op` into a `cone F`.

Equations
def category_theory.limits.cone.unop {J : Type u₁} {C : Type u₃} {F : J C}  :

Change a `cone F.op` into a `cocone F`.

Equations
@[simp]
theorem category_theory.limits.cone.unop_ι {J : Type u₁} {C : Type u₃} {F : J C}  :
@[simp]
theorem category_theory.limits.cone.unop_X {J : Type u₁} {C : Type u₃} {F : J C}  :
c.unop.X =
def category_theory.limits.cocone_equivalence_op_cone_op {J : Type u₁} {C : Type u₃} (F : J C) :

The category of cocones on `F` is equivalent to the opposite category of the category of cones on the opposite of `F`.

Equations
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_functor_obj {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_inverse_obj {J : Type u₁} {C : Type u₃} (F : J C) (c : ᵒᵖ) :
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_counit_iso {J : Type u₁} {C : Type u₃} (F : J C) :
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_inverse_map_hom {J : Type u₁} {C : Type u₃} (F : J C) (X Y : ᵒᵖ) (f : X Y) :
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_functor_map {J : Type u₁} {C : Type u₃} (F : J C) (X Y : category_theory.limits.cocone F) (f : X Y) :
= quiver.hom.op {hom := f.hom.op, w' := _}
@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_unit_iso {J : Type u₁} {C : Type u₃} (F : J C) :
def