mathlibdocumentation

category_theory.limits.cones

def category_theory.functor.cones {J : Type v} {C : Type u}  :
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
theorem category_theory.functor.cones_obj {J : Type v} {C : Type u} (F : J C) (X : Cᵒᵖ) :
F.cones.obj X = F)

@[simp]
theorem category_theory.functor.cones_map_app {J : Type v} {C : Type u} (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} {C : Type u}  :
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
theorem category_theory.functor.cocones_obj {J : Type v} {C : Type u} (F : J C) (X : C) :
F.cocones.obj X = (F

@[simp]
theorem category_theory.functor.cocones_map_app {J : Type v} {C : Type u} (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]
theorem category_theory.cones_map (J : Type v) (C : Type u) (F G : J C) (f : F G) :

@[simp]
theorem category_theory.cones_obj (J : Type v) (C : Type u) (F : J C) :
.obj F = F.cones

def category_theory.cones (J : Type v) (C : Type u)  :
(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
@[simp]
theorem category_theory.cocones_map (J : Type v) (C : Type u) (F G : (J C)ᵒᵖ) (f : F G) :

@[simp]
theorem category_theory.cocones_obj (J : Type v) (C : Type u) (F : (J C)ᵒᵖ) :

def category_theory.cocones (J : Type v) (C : Type u)  :
(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} {C : Type u}  :
J CType (max u v)
• X : C
• π : 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`.

@[instance]

Equations
@[simp]
theorem category_theory.limits.cone.w {J : Type v} {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 v} {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 v} {C : Type u}  :
J CType (max u v)
• X : C
• ι : F

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} {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 v} {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'

def category_theory.limits.cone.equiv {J : Type v} {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]
def category_theory.limits.cone.extensions {J : Type v} {C : Type u} {F : J C}  :

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

Equations
@[simp]
def category_theory.limits.cone.extend {J : Type v} {C : Type u} {F : J C} {X : C} :
(X c.X)

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

Equations
@[simp]
theorem category_theory.limits.cone.extend_π {J : Type v} {C : Type u} {F : J C} {X : Cᵒᵖ} (f : c.X) :
(c.extend f).π = c.extensions.app X f

@[simp]
theorem category_theory.limits.cone.whisker_X {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

@[simp]
theorem category_theory.limits.cone.whisker_π {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

def category_theory.limits.cone.whisker {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J) :

Whisker a cone by precomposition of a functor.

Equations
def category_theory.limits.cocone.equiv {J : Type v} {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
@[simp]
def category_theory.limits.cocone.extensions {J : Type v} {C : Type u} {F : J C}  :

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

Equations
@[simp]
def category_theory.limits.cocone.extend {J : Type v} {C : Type u} {F : J C} {X : C} :
(c.X X)

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

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

@[simp]
theorem category_theory.limits.cocone.whisker_ι {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

def category_theory.limits.cocone.whisker {J : Type v} {C : Type u} {F : J C} {K : Type v} (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 v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

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 : B) :
x.hom = y.homx = y

theorem category_theory.limits.cone_morphism.ext_iff {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 : B) :
x = y x.hom = y.hom

@[ext]
structure category_theory.limits.cone_morphism {J : Type v} {C : Type u} {F : J C} :
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.

@[simp]
theorem category_theory.limits.cone_morphism.w {J : Type v} {C : Type u} {F : J C} {A B : category_theory.limits.cone F} (j : J) :
c.hom B.π.app j = A.π.app j

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

@[instance]
def category_theory.limits.inhabited_cone_morphism {J : Type v} {C : Type u} {F : J C}  :

Equations
@[simp]
theorem category_theory.limits.cone.category_to_category_struct_comp_hom {J : Type v} {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

@[simp]

@[simp]
theorem category_theory.limits.cone.category_to_category_struct_id_hom {J : Type v} {C : Type u} {F : J C}  :
(𝟙 B).hom = 𝟙 B.X

@[instance]
def category_theory.limits.cone.category {J : Type v} {C : Type u} {F : J C} :

The category of cones on a given diagram.

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

def category_theory.limits.cones.cone_iso_of_hom_iso {J : Type v} {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.

Equations
@[simp]
theorem category_theory.limits.cones.postcompose_obj_X {J : Type v} {C : Type u} {F G : J C} (α : F G)  :
= c.X

@[simp]
theorem category_theory.limits.cones.postcompose_obj_π {J : Type v} {C : Type u} {F G : J C} (α : F G)  :
= c.π α

def category_theory.limits.cones.postcompose {J : Type v} {C : Type u} {F G : J C} :

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 v} {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 v} {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
def category_theory.limits.cones.postcompose_id {J : Type v} {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 v} {C : Type u} {F G : J C} (α : F G) :

@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_unit_iso {J : Type v} {C : Type u} {F G : J C} (α : F G) :

@[simp]
theorem category_theory.limits.cones.postcompose_equivalence_inverse {J : Type v} {C : Type u} {F G : J C} (α : F G) :

def category_theory.limits.cones.postcompose_equivalence {J : Type v} {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 v} {C : Type u} {F G : J C} (α : F G) :

@[simp]
theorem category_theory.limits.cones.whiskering_map_hom {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J) (c c' : category_theory.limits.cone F) (f : c c') :

def category_theory.limits.cones.whiskering {J : Type v} {C : Type u} {F : J C} {K : Type v} (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 v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_counit_iso {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_inverse {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

@[simp]
theorem category_theory.limits.cones.whiskering_equivalence_unit_iso {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

def category_theory.limits.cones.whiskering_equivalence {J : Type v} {C : Type u} {F : J C} {K : Type v} (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 v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

def category_theory.limits.cones.equivalence_of_reindexing {J : Type v} {C : Type u} {F : J C} {K : Type v} {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_functor_obj {J : Type v} {C : Type u} {F : J C} {K : Type v} {G : K C} (e : K J) (α : e.functor F G)  :

@[simp]
theorem category_theory.limits.cones.forget_map {J : Type v} {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 v} {C : Type u} (F : J C)  :

def category_theory.limits.cones.forget {J : Type v} {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 v} {C : Type u} (F : J C) {D : Type u'} (G : C D) :

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

Equations
@[simp]
theorem category_theory.limits.cones.functoriality_obj_X {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :
.X = G.obj A.X

@[simp]
theorem category_theory.limits.cones.functoriality_map_hom {J : Type v} {C : Type u} (F : J C) {D : Type u'} (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 v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) :
.π.app j = G.map (A.π.app j)

@[instance]
def category_theory.limits.cones.functoriality_full {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

Equations
@[instance]
def category_theory.limits.cones.functoriality_faithful {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_inverse {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_unit_iso {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

def category_theory.limits.cones.functoriality_equivalence {J : Type v} {C : Type u} (F : J C) {D : Type u'} (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 v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[simp]
theorem category_theory.limits.cones.functoriality_equivalence_functor {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[instance]
def category_theory.limits.cones.reflects_cone_isomorphism {J : Type v} {C : Type u} {D : Type u'} (F : C D) (K : J C) :

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

Equations
theorem category_theory.limits.cocone_morphism.ext_iff {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 : B) :
x = y x.hom = y.hom

@[ext]
structure category_theory.limits.cocone_morphism {J : Type v} {C : Type u} {F : J C} :

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 : B) :
x.hom = y.homx = y

@[instance]
def category_theory.limits.inhabited_cocone_morphism {J : Type v} {C : Type u} {F : J C}  :

Equations
@[simp]
theorem category_theory.limits.cocone_morphism.w {J : Type v} {C : Type u} {F : J C} {A B : category_theory.limits.cocone F} (j : J) :
A.ι.app j c.hom = B.ι.app j

@[simp]
theorem category_theory.limits.cocone_morphism.w_assoc {J : Type v} {C : Type u} {F : J C} {A B : category_theory.limits.cocone F} (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} {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]

@[simp]
theorem category_theory.limits.cocone.category_to_category_struct_id_hom {J : Type v} {C : Type u} {F : J C}  :
(𝟙 B).hom = 𝟙 B.X

@[instance]
def category_theory.limits.cocone.category {J : Type v} {C : Type u} {F : J C} :

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

def category_theory.limits.cocones.cocone_iso_of_hom_iso {J : Type v} {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.

Equations
def category_theory.limits.cocones.precompose {J : Type v} {C : Type u} {F G : J C} :

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 v} {C : Type u} {F G : J C} (α : G F)  :
= α c.ι

@[simp]
theorem category_theory.limits.cocones.precompose_map_hom {J : Type v} {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 v} {C : Type u} {F G : J C} (α : G F)  :
= c.X

def category_theory.limits.cocones.precompose_comp {J : Type v} {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 v} {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 v} {C : Type u} {F G : J C} (α : G F) :

@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_inverse {J : Type v} {C : Type u} {F G : J C} (α : G F) :

def category_theory.limits.cocones.precompose_equivalence {J : Type v} {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 v} {C : Type u} {F G : J C} (α : G F) :

@[simp]
theorem category_theory.limits.cocones.precompose_equivalence_unit_iso {J : Type v} {C : Type u} {F G : J C} (α : G F) :

def category_theory.limits.cocones.whiskering {J : Type v} {C : Type u} {F : J C} {K : Type v} (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 v} {C : Type u} {F : J C} {K : Type v} (E : K J) (c c' : category_theory.limits.cocone F) (f : c c') :

@[simp]
theorem category_theory.limits.cocones.whiskering_obj {J : Type v} {C : Type u} {F : J C} {K : Type v} (E : K J)  :

def category_theory.limits.cocones.whiskering_equivalence {J : Type v} {C : Type u} {F : J C} {K : Type v} (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 v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_unit_iso {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_functor {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

@[simp]
theorem category_theory.limits.cocones.whiskering_equivalence_counit_iso {J : Type v} {C : Type u} {F : J C} {K : Type v} (e : K J) :

def category_theory.limits.cocones.equivalence_of_reindexing {J : Type v} {C : Type u} {F : J C} {K : Type v} {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
@[simp]
theorem category_theory.limits.cocones.equivalence_of_reindexing_functor_obj {J : Type v} {C : Type u} {F : J C} {K : Type v} {G : K C} (e : K J) (α : e.functor F G)  :

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

def category_theory.limits.cocones.functoriality {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) :

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

Equations
@[simp]
theorem category_theory.limits.cocones.functoriality_map_hom {J : Type v} {C : Type u} (F : J C) {D : Type u'} (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 v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) :
.ι.app j = G.map (A.ι.app j)

@[simp]
theorem category_theory.limits.cocones.functoriality_obj_X {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :
.X = G.obj A.X

@[instance]
def category_theory.limits.cocones.functoriality_full {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

Equations
@[instance]
def category_theory.limits.cocones.functoriality_faithful {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_inverse {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_functor {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

def category_theory.limits.cocones.functoriality_equivalence {J : Type v} {C : Type u} (F : J C) {D : Type u'} (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 v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[simp]
theorem category_theory.limits.cocones.functoriality_equivalence_unit_iso {J : Type v} {C : Type u} (F : J C) {D : Type u'} (e : C D) :

@[instance]
def category_theory.limits.cocones.reflects_cocone_isomorphism {J : Type v} {C : Type u} {D : Type u'} (F : C D) (K : J C) :

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

Equations
def category_theory.functor.map_cone {J : Type v} {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
def category_theory.functor.map_cocone {J : Type v} {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
@[simp]
theorem category_theory.functor.map_cone_X {J : Type v} {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_X {J : Type v} {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_cone_morphism {J : Type v} {C : Type u} {D : Type u'} {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} {C : Type u} {D : Type u'} {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} {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)

@[simp]
theorem category_theory.functor.map_cocone_ι {J : Type v} {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)

def category_theory.functor.map_cone_inv {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D)  :

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 v} {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 v} {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 v} {C : Type u} {D : Type u'} {F : J C} (H : C D)  :

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 v} {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 v} {C : Type u} {D : Type u'} {F : J D} (H : D C)  :

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

Equations
def category_theory.functor.map_cone_postcompose {J : Type v} {C : Type u} {D : Type u'} {F G : J C} (H : C D) {α : F G}  :

`map_cone` commutes with `postcompose`

Equations
@[simp]
theorem category_theory.functor.map_cone_postcompose_hom_hom {J : Type v} {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 v} {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 v} {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 v} {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 v} {C : Type u} {D : Type u'} {F G : J C} (H : C D) {α : F G}  :

@[simp]
theorem category_theory.functor.map_cocone_precompose_inv_hom {J : Type v} {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 v} {C : Type u} {D : Type u'} {F G : J C} (H : C D) {α : F G}  :

def category_theory.functor.map_cocone_precompose {J : Type v} {C : Type u} {D : Type u'} {F G : J C} (H : C D) {α : F G}  :

`map_cocone` commutes with `precompose`

Equations
@[simp]
theorem category_theory.functor.map_cocone_precompose_equivalence_functor_hom_hom {J : Type v} {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 v} {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 v} {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 v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

`map_cone` commutes with `whisker`

Equations
@[simp]
theorem category_theory.functor.map_cone_whisker_hom_hom {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

@[simp]
theorem category_theory.functor.map_cone_whisker_inv_hom {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

@[simp]
theorem category_theory.functor.map_cocone_whisker_inv_hom {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

def category_theory.functor.map_cocone_whisker {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

`map_cocone` commutes with `whisker`

Equations
@[simp]
theorem category_theory.functor.map_cocone_whisker_hom_hom {J : Type v} {C : Type u} {D : Type u'} {F : J C} (H : C D) {K : Type v} {E : K J}  :

@[simp]
theorem category_theory.limits.cocone.op_X {J : Type v} {C : Type u} {F : J C}  :
c.op.X =

def category_theory.limits.cocone.op {J : Type v} {C : Type u} {F : J C} :

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

Equations
@[simp]
theorem category_theory.limits.cocone.op_π_app {J : Type v} {C : Type u} {F : J C} (j : Jᵒᵖ) :
c.op.π.app j = (c.ι.app (opposite.unop j)).op

@[simp]
theorem category_theory.limits.cone.op_ι_app {J : Type v} {C : Type u} {F : J C} (j : Jᵒᵖ) :
c.op.ι.app j = (c.π.app (opposite.unop j)).op

def category_theory.limits.cone.op {J : Type v} {C : Type u} {F : J C} :

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

Equations
@[simp]
theorem category_theory.limits.cone.op_X {J : Type v} {C : Type u} {F : J C}  :
c.op.X =

@[simp]
theorem category_theory.limits.cocone.unop_π_app {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.cocone.unop_X {J : Type v} {C : Type u} {F : J C}  :
c.unop.X =

def category_theory.limits.cocone.unop {J : Type v} {C : Type u} {F : J C} :

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

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

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

Equations
@[simp]
theorem category_theory.limits.cone.unop_X {J : Type v} {C : Type u} {F : J C}  :
c.unop.X =

@[simp]
theorem category_theory.limits.cone.unop_ι_app {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_functor_obj {J : Type v} {C : Type u} (F : J C)  :

@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_inverse_obj {J : Type v} {C : Type u} (F : J C) (c : ᵒᵖ) :

@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_counit_iso {J : Type v} {C : Type u} (F : J C) :

@[simp]
theorem category_theory.limits.cocone_equivalence_op_cone_op_inverse_map_hom {J : Type v} {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 v} {C : Type u} (F : J C) (X Y : category_theory.limits.cocone F) (f : X Y) :

def category_theory.limits.cocone_equivalence_op_cone_op {J : Type v} {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_unit_iso {J : Type v} {C : Type u} (F : J C) :

def category_theory.limits.cone_of_cocone_left_op {J : Type v} {C : Type u} {F : J Cᵒᵖ} :

Change a cocone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`.

Equations
@[simp]
theorem category_theory.limits.cone_of_cocone_left_op_X {J : Type v} {C : Type u} {F : J Cᵒᵖ}  :

@[simp]
theorem category_theory.limits.cone_of_cocone_left_op_π_app {J : Type v} {C : Type u} {F : J Cᵒᵖ} (j : J) :
= (c.ι.app (opposite.op j)).op

@[simp]
theorem category_theory.limits.cocone_left_op_of_cone_X {J : Type v} {C : Type u} {F : J Cᵒᵖ}  :

def category_theory.limits.cocone_left_op_of_cone {J : Type v} {C : Type u} {F : J Cᵒᵖ} :

Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.left_op : Jᵒᵖ ⥤ C`.

Equations
@[simp]
theorem category_theory.limits.cocone_left_op_of_cone_ι_app {J : Type v} {C : Type u} {F : J Cᵒᵖ} (j : Jᵒᵖ) :

@[simp]
theorem category_theory.limits.cocone_of_cone_left_op_X {J : Type v} {C : Type u} {F : J Cᵒᵖ}  :

def category_theory.limits.cocone_of_cone_left_op {J : Type v} {C : Type u} {F : J Cᵒᵖ} :

Change a cone on `F.left_op : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`.

Equations
@[simp]
theorem category_theory.limits.cocone_of_cone_left_op_ι_app {J : Type v} {C : Type u} {F : J Cᵒᵖ} (j : J) :
= (c.π.app (opposite.op j)).op

@[simp]
theorem category_theory.limits.cone_left_op_of_cocone_X {J : Type v} {C : Type u} {F : J Cᵒᵖ}  :

def category_theory.limits.cone_left_op_of_cocone {J : Type v} {C : Type u} {F : J Cᵒᵖ} :

Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.left_op : Jᵒᵖ ⥤ C`.

Equations
@[simp]
theorem category_theory.limits.cone_left_op_of_cocone_π_app {J : Type v} {C : Type u} {F : J Cᵒᵖ} (j : Jᵒᵖ) :

def category_theory.functor.map_cone_op {J : Type v} {C : Type u} {F : J C} {D : Type u'} (G : C D)  :

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

Equations
def category_theory.functor.map_cocone_op {J : Type v} {C : Type u} {F : J C} {D : Type u'} (G : C D)  :

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

Equations