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.pt and a natural transformation c.π from the constant c.pt 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.pt 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 CategoryTheory.Functor.cones_map_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), ((CategoryTheory.Functor.cones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)

@[simp]

theorem CategoryTheory.Functor.cones_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : (CategoryTheory.Functor.cones F).obj X = ((CategoryTheory.Functor.const J).obj X.unop ⟶ F)

def CategoryTheory.Functor.cones {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₃))

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

@[simp]

theorem CategoryTheory.Functor.cocones_map_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : C} (f : X ⟶ Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), ((CategoryTheory.Functor.cocones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f

@[simp]

theorem CategoryTheory.Functor.cocones_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : C) : (CategoryTheory.Functor.cocones F).obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)

def CategoryTheory.Functor.cocones {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor C (Type (max u₁ v₃))

If F : J ⥤ C then F.cocones is the functor assigning to an object (X : C) the type of natural transformations from F to the constant functor with value X. An object corepresenting this functor is a colimit of F.

@[simp]

theorem CategoryTheory.cones_map_app_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : ∀ {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj ((CategoryTheory.Functor.const J).op.obj X_1)) (X_2 : J), (((CategoryTheory.cones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (a.app X_2) (f.app X_2)

@[simp]

theorem CategoryTheory.cones_obj_map_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), (((CategoryTheory.cones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)

@[simp]

theorem CategoryTheory.cones_obj_obj (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ((CategoryTheory.cones J C).obj F).obj X = ((CategoryTheory.Functor.const J).obj X.unop ⟶ F)

def CategoryTheory.cones (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Functor (CategoryTheory.Functor J C) (CategoryTheory.Functor 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.

@[simp]

theorem CategoryTheory.cocones_obj_map_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : (CategoryTheory.Functor J C)ᵒᵖ) : ∀ {X Y : C} (f : X ⟶ Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F.unop)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), (((CategoryTheory.cocones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f

@[simp]

theorem CategoryTheory.cocones_obj_obj (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : (CategoryTheory.Functor J C)ᵒᵖ) (X : C) : ((CategoryTheory.cocones J C).obj F).obj X = (F.unop ⟶ (CategoryTheory.Functor.const J).obj X)

@[simp]

theorem CategoryTheory.cocones_map_app_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : ∀ {X Y : (CategoryTheory.Functor J C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj ((CategoryTheory.Functor.const J).obj X_1)) (X_2 : J), (((CategoryTheory.cocones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (f.unop.app X_2) (a.app X_2)

def CategoryTheory.cocones (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Functor (CategoryTheory.Functor J C)ᵒᵖ (CategoryTheory.Functor 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.

structure CategoryTheory.Limits.Cone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : Type (max (max u₁ u₃) v₃)

• pt : C

  An object of C

• π : (CategoryTheory.Functor.const J).obj s.pt ⟶ F

  A natural transformation from the constant functor at X to F

A c : Cone F is:

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

Example: if J is a category coming from a poset then the data required to make a term of type Cone F is morphisms πⱼ : c.pt ⟶ F j for all j : J and, for all i ≤ j in J, morphisms πᵢⱼ : F i ⟶ F j such that πᵢ ≫ πᵢⱼ = πᵢ.

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

instance CategoryTheory.Limits.inhabitedCone {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1} ) C) : Inhabited (CategoryTheory.Limits.Cone F)

@[simp]

theorem CategoryTheory.Limits.Cone.w_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j : J} {j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.π.app j) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (c.π.app j') h

@[simp]

theorem CategoryTheory.Limits.Cone.w {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (c.π.app j) (F.map f) = c.π.app j'

structure CategoryTheory.Limits.Cocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : Type (max (max u₁ u₃) v₃)

• pt : C

  An object of C

• ι : F ⟶ (CategoryTheory.Functor.const J).obj s.pt

  A natural transformation from F to the constant functor at pt

A c : Cocone F is

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

For example, if the source J of F is a partially ordered set, then to give c : Cocone F is to give a collection of morphisms ιⱼ : F j ⟶ c.pt and, for all j ≤ k in J, morphisms ιⱼₖ : F j ⟶ F k such that Fⱼₖ ≫ Fₖ = Fⱼ for all j ≤ k.

Cocone F is equivalent, via Cone.equiv below, to Σ X, F.cocones.obj X.

instance CategoryTheory.Limits.inhabitedCocone {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1} ) C) : Inhabited (CategoryTheory.Limits.Cocone F)

@[simp]

theorem CategoryTheory.Limits.Cocone.w_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {j : J} {j' : J} (f : j ⟶ j') {Z : C} (h : ((CategoryTheory.Functor.const J).obj c.pt).obj j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (c.ι.app j') h) = CategoryTheory.CategoryStruct.comp (c.ι.app j) h

theorem CategoryTheory.Limits.Cocone.w {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (F.map f) (c.ι.app j') = c.ι.app j

@[simp]

theorem CategoryTheory.Limits.Cone.equiv_hom_snd {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equiv F).hom c).snd = c.π

@[simp]

theorem CategoryTheory.Limits.Cone.equiv_inv_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X) : ((CategoryTheory.Limits.Cone.equiv F).inv c).π = c.snd

@[simp]

theorem CategoryTheory.Limits.Cone.equiv_hom_fst {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equiv F).hom c).fst = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.Cone.equiv_inv_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X) : ((CategoryTheory.Limits.Cone.equiv F).inv c).pt = c.fst.unop

def CategoryTheory.Limits.Cone.equiv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F ≅ (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X

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

@[simp]

theorem CategoryTheory.Limits.Cone.extensions_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : Cᵒᵖ) (f : (CategoryTheory.Functor.comp (CategoryTheory.yoneda.obj c.pt) CategoryTheory.uliftFunctor.{u₁, v₃} ).obj X) : (CategoryTheory.Limits.Cone.extensions c).app X f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down) c.π

def CategoryTheory.Limits.Cone.extensions {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.comp (CategoryTheory.yoneda.obj c.pt) CategoryTheory.uliftFunctor.{u₁, v₃} ⟶ CategoryTheory.Functor.cones F

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

@[simp]

theorem CategoryTheory.Limits.Cone.extend_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (CategoryTheory.Limits.Cone.extend c f).π = (CategoryTheory.Limits.Cone.extensions c).app (Opposite.op X) { down := f }

@[simp]

theorem CategoryTheory.Limits.Cone.extend_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (CategoryTheory.Limits.Cone.extend c f).pt = X

def CategoryTheory.Limits.Cone.extend {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : CategoryTheory.Limits.Cone F

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

@[simp]

theorem CategoryTheory.Limits.Cone.whisker_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whisker E c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.Cone.whisker_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whisker E c).π = CategoryTheory.whiskerLeft E c.π

def CategoryTheory.Limits.Cone.whisker {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp E F)

Whisker a cone by precomposition of a functor.

def CategoryTheory.Limits.Cocone.equiv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F ≅ (X : C) × (CategoryTheory.Functor.cocones F).obj X

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

@[simp]

theorem CategoryTheory.Limits.Cocone.extensions_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : C) (f : (CategoryTheory.Functor.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt)) CategoryTheory.uliftFunctor.{u₁, v₃} ).obj X) : (CategoryTheory.Limits.Cocone.extensions c).app X f = CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f.down)

def CategoryTheory.Limits.Cocone.extensions {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt)) CategoryTheory.uliftFunctor.{u₁, v₃} ⟶ CategoryTheory.Functor.cocones F

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

@[simp]

theorem CategoryTheory.Limits.Cocone.extend_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {Y : C} (f : c.pt ⟶ Y) : (CategoryTheory.Limits.Cocone.extend c f).pt = Y

@[simp]

theorem CategoryTheory.Limits.Cocone.extend_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {Y : C} (f : c.pt ⟶ Y) : (CategoryTheory.Limits.Cocone.extend c f).ι = (CategoryTheory.Limits.Cocone.extensions c).app Y { down := f }

def CategoryTheory.Limits.Cocone.extend {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {Y : C} (f : c.pt ⟶ Y) : CategoryTheory.Limits.Cocone F

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

@[simp]

theorem CategoryTheory.Limits.Cocone.whisker_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.whisker E c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.whisker_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.whisker E c).ι = CategoryTheory.whiskerLeft E c.ι

def CategoryTheory.Limits.Cocone.whisker {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp E F)

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

structure CategoryTheory.Limits.ConeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cone F) (B : CategoryTheory.Limits.Cone F) : Type v₃

• hom : A.pt ⟶ B.pt

  A morphism between the two vertex objects of the cones

• w : ∀ (j : J), CategoryTheory.CategoryStruct.comp s.hom (B.π.app j) = A.π.app j

  The triangle consisting of the two natural transformations and hom commutes

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 CategoryTheory.Limits.ConeMorphism.w_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A : CategoryTheory.Limits.Cone F} {B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π.app j) h) = CategoryTheory.CategoryStruct.comp (A.π.app j) h

instance CategoryTheory.Limits.inhabitedConeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cone F) : Inhabited (CategoryTheory.Limits.ConeMorphism A A)

@[simp]

theorem CategoryTheory.Limits.Cone.category_comp_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : ∀ {X Y Z : CategoryTheory.Limits.Cone F} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.Limits.Cone.category_id_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (B : CategoryTheory.Limits.Cone F) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt

instance CategoryTheory.Limits.Cone.category {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Category.{v₃, max (max u₃ u₁) v₃} (CategoryTheory.Limits.Cone F)

The category of cones on a given diagram.

theorem CategoryTheory.Limits.ConeMorphism.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} {c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') (g : c ⟶ c') (w : f.hom = g.hom) : f = g

@[simp]

theorem CategoryTheory.Limits.Cones.ext_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} {c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝) : (CategoryTheory.Limits.Cones.ext φ).inv.hom = φ.inv

@[simp]

theorem CategoryTheory.Limits.Cones.ext_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} {c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝) : (CategoryTheory.Limits.Cones.ext φ).hom.hom = φ.hom

def CategoryTheory.Limits.Cones.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} {c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝) : c ≅ c'

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

@[simp]

theorem CategoryTheory.Limits.Cones.eta_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.eta c).inv.hom = CategoryTheory.CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.Cones.eta_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.eta c).hom.hom = CategoryTheory.CategoryStruct.id c.pt

def CategoryTheory.Limits.Cones.eta {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c ≅ { pt := c.pt, π := c.π }

Eta rule for cones.

theorem CategoryTheory.Limits.Cones.cone_iso_of_hom_iso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone K} {d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f

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

@[simp]

theorem CategoryTheory.Limits.Cones.postcompose_obj_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.postcompose α).obj c).π = CategoryTheory.CategoryStruct.comp c.π α

@[simp]

theorem CategoryTheory.Limits.Cones.postcompose_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.postcompose α).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.Cones.postcompose_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.postcompose α).obj c).pt = c.pt

def CategoryTheory.Limits.Cones.postcompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)

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

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeComp_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.postcomposeComp α β).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeComp_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.postcomposeComp α β).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt

def CategoryTheory.Limits.Cones.postcomposeComp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Limits.Cones.postcompose (CategoryTheory.CategoryStruct.comp α β) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.postcompose α) (CategoryTheory.Limits.Cones.postcompose β)

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

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeId_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.postcomposeId.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeId_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.postcomposeId.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt

def CategoryTheory.Limits.Cones.postcomposeId {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.Cones.postcompose (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)

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

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cones.postcomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.postcompose α.inv) (CategoryTheory.Limits.Cones.postcompose α.hom)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cones.postcomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cones.postcomposeEquivalence α).functor = CategoryTheory.Limits.Cones.postcompose α.hom

@[simp]

theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cones.postcomposeEquivalence α).inverse = CategoryTheory.Limits.Cones.postcompose α.inv

def CategoryTheory.Limits.Cones.postcomposeEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G

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

@[simp]

theorem CategoryTheory.Limits.Cones.whiskering_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.whiskering E).obj c = CategoryTheory.Limits.Cone.whisker E c

@[simp]

theorem CategoryTheory.Limits.Cones.whiskering_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.whiskering E).map f).hom = f.hom

def CategoryTheory.Limits.Cones.whiskering {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp E F))

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

@[simp]

theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cones.whiskeringEquivalence e).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse) (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom)

@[simp]

theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cones.whiskeringEquivalence e).unitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cones.whiskeringEquivalence e).counitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse) (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom)) (CategoryTheory.Limits.Cones.whiskering e.functor)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cones.whiskering e.functor

def CategoryTheory.Limits.Cones.whiskeringEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp e.functor F)

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

@[simp]

theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : (CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).functor = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.functor) (CategoryTheory.Limits.Cones.postcompose α.hom)

@[simp]

theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : (CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).unitIso = (CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt)) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.whiskering e.functor) (CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt)) (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse) (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom)))

@[simp]

theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : (CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.postcompose α.inv) (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse) (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom))

@[simp]

theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : (CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).counitIso = CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.postcompose α.inv) (CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt)) (CategoryTheory.Limits.Cones.postcompose α.hom)) ≪≫ CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt)

def CategoryTheory.Limits.Cones.equivalenceOfReindexing {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone 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).

@[simp]

theorem CategoryTheory.Limits.Cones.forget_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cones.forget F).map f = f.hom

@[simp]

theorem CategoryTheory.Limits.Cones.forget_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.forget F).obj t = t.pt

def CategoryTheory.Limits.Cones.forget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) C

Forget the cone structure and obtain just the cone point.

@[simp]

theorem CategoryTheory.Limits.Cones.functoriality_obj_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) (j : J) : ((CategoryTheory.Limits.Cones.functoriality F G).obj A).π.app j = G.map (A.π.app j)

@[simp]

theorem CategoryTheory.Limits.Cones.functoriality_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cones.functoriality F G).obj A).pt = G.obj A.pt

@[simp]

theorem CategoryTheory.Limits.Cones.functoriality_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.functoriality F G).map f).hom = G.map f.hom

def CategoryTheory.Limits.Cones.functoriality {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F G))

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

instance CategoryTheory.Limits.Cones.functorialityFull {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.Full G] [CategoryTheory.Faithful G] : CategoryTheory.Full (CategoryTheory.Limits.Cones.functoriality F G)

instance CategoryTheory.Limits.Cones.functorialityFaithful {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.Faithful G] : CategoryTheory.Faithful (CategoryTheory.Limits.Cones.functoriality F G)

@[simp]

theorem CategoryTheory.Limits.Cones.functorialityEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cones.functoriality F e.functor

@[simp]

theorem CategoryTheory.Limits.Cones.functorialityEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cones.functorialityEquivalence F e).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.functoriality (CategoryTheory.Functor.comp F e.functor) e.inverse) (CategoryTheory.Limits.Cones.postcomposeEquivalence (CategoryTheory.Functor.associator F e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ CategoryTheory.Functor.rightUnitor F)).functor

@[simp]

theorem CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents fun c => CategoryTheory.Limits.Cones.ext (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj c).1)

@[simp]

theorem CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents fun c => CategoryTheory.Limits.Cones.ext (e.counitIso.app c.pt)

def CategoryTheory.Limits.Cones.functorialityEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F e.functor)

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.

instance CategoryTheory.Limits.Cones.reflects_cone_isomorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms F] (K : CategoryTheory.Functor J C) : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Limits.Cones.functoriality K F)

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

structure CategoryTheory.Limits.CoconeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cocone F) (B : CategoryTheory.Limits.Cocone F) : Type v₃

• hom : A.pt ⟶ B.pt

  A morphism between the (co)vertex objects in C

• w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) s.hom = B.ι.app j

  The triangle made from the two natural transformations and hom commutes

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

instance CategoryTheory.Limits.inhabitedCoconeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cocone F) : Inhabited (CategoryTheory.Limits.CoconeMorphism A A)

@[simp]

theorem CategoryTheory.Limits.CoconeMorphism.w_assoc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A : CategoryTheory.Limits.Cocone F} {B : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.CoconeMorphism A B) (j : J) {Z : C} (h : B.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.ι.app j) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (B.ι.app j) h

@[simp]

theorem CategoryTheory.Limits.Cocone.category_id_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (B : CategoryTheory.Limits.Cocone F) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.category_comp_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : ∀ {X Y Z : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

instance CategoryTheory.Limits.Cocone.category {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Category.{v₃, max (max u₃ u₁) v₃} (CategoryTheory.Limits.Cocone F)

theorem CategoryTheory.Limits.CoconeMorphism.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {c' : CategoryTheory.Limits.Cocone F} (f : c ⟶ c') (g : c ⟶ c') (w : f.hom = g.hom) : f = g

@[simp]

theorem CategoryTheory.Limits.Cocones.ext_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝) : (CategoryTheory.Limits.Cocones.ext φ).hom.hom = φ.hom

@[simp]

theorem CategoryTheory.Limits.Cocones.ext_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝) : (CategoryTheory.Limits.Cocones.ext φ).inv.hom = φ.inv

def CategoryTheory.Limits.Cocones.ext {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝) : c ≅ c'

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

@[simp]

theorem CategoryTheory.Limits.Cocones.eta_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.eta c).inv.hom = CategoryTheory.CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.Cocones.eta_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.eta c).hom.hom = CategoryTheory.CategoryStruct.id c.pt

def CategoryTheory.Limits.Cocones.eta {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : c ≅ { pt := c.pt, ι := c.ι }

Eta rule for cocones.

theorem CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone K} {d : CategoryTheory.Limits.Cocone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f

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

@[simp]

theorem CategoryTheory.Limits.Cocones.precompose_obj_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocones.precompose α).obj c).ι = CategoryTheory.CategoryStruct.comp α c.ι

@[simp]

theorem CategoryTheory.Limits.Cocones.precompose_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocones.precompose α).obj c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.Cocones.precompose_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ⟶ F) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.precompose α).map f).hom = f.hom

def CategoryTheory.Limits.Cocones.precompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ⟶ F) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone G)

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

def CategoryTheory.Limits.Cocones.precomposeComp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Limits.Cocones.precompose (CategoryTheory.CategoryStruct.comp α β) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.precompose β) (CategoryTheory.Limits.Cocones.precompose α)

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

def CategoryTheory.Limits.Cocones.precomposeId {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.Cocones.precompose (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)

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

@[simp]

theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ≅ F) : (CategoryTheory.Limits.Cocones.precomposeEquivalence α).inverse = CategoryTheory.Limits.Cocones.precompose α.inv

@[simp]

theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ≅ F) : (CategoryTheory.Limits.Cocones.precomposeEquivalence α).functor = CategoryTheory.Limits.Cocones.precompose α.hom

@[simp]

theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ≅ F) : (CategoryTheory.Limits.Cocones.precomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ≅ F) : (CategoryTheory.Limits.Cocones.precomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.precompose α.inv) (CategoryTheory.Limits.Cocones.precompose α.hom)).obj s).pt)

def CategoryTheory.Limits.Cocones.precomposeEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : G ≅ F) : CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone G

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

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskering_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.whiskering E).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskering_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.whiskering E).obj c = CategoryTheory.Limits.Cocone.whisker E c

def CategoryTheory.Limits.Cocones.whiskering {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp E F))

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

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cocones.whiskeringEquivalence e).counitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.whiskering e.inverse) (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.counitIso.inv F) (CategoryTheory.Functor.associator e.inverse e.functor F).inv)))) (CategoryTheory.Limits.Cocones.whiskering e.functor)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cocones.whiskeringEquivalence e).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.whiskering e.inverse) (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.counitIso.inv F) (CategoryTheory.Functor.associator e.inverse e.functor F).inv)))

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cocones.whiskeringEquivalence e).unitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt)

@[simp]

theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cocones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cocones.whiskering e.functor

def CategoryTheory.Limits.Cocones.whiskeringEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp e.functor F)

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

@[simp]

theorem CategoryTheory.Limits.Cocones.equivalenceOfReindexing_functor_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) (X : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.equivalenceOfReindexing e α).functor.obj X = (CategoryTheory.Limits.Cocones.precompose α.inv).obj (CategoryTheory.Limits.Cocone.whisker e.functor X)

def CategoryTheory.Limits.Cocones.equivalenceOfReindexing {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : CategoryTheory.Functor.comp e.functor F ≅ G) : CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone 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).

@[simp]

theorem CategoryTheory.Limits.Cocones.forget_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.forget F).obj t = t.pt

@[simp]

theorem CategoryTheory.Limits.Cocones.forget_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cocones.forget F).map f = f.hom

def CategoryTheory.Limits.Cocones.forget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) C

Forget the cocone structure and obtain just the cocone point.

@[simp]

theorem CategoryTheory.Limits.Cocones.functoriality_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocones.functoriality F G).obj A).pt = G.obj A.pt

@[simp]

theorem CategoryTheory.Limits.Cocones.functoriality_obj_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cocone F) (j : J) : ((CategoryTheory.Limits.Cocones.functoriality F G).obj A).ι.app j = G.map (A.ι.app j)

@[simp]

theorem CategoryTheory.Limits.Cocones.functoriality_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.functoriality F G).map f).hom = G.map f.hom

def CategoryTheory.Limits.Cocones.functoriality {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F G))

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

instance CategoryTheory.Limits.Cocones.functorialityFull {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.Full G] [CategoryTheory.Faithful G] : CategoryTheory.Full (CategoryTheory.Limits.Cocones.functoriality F G)

instance CategoryTheory.Limits.Cocones.functoriality_faithful {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.Faithful G] : CategoryTheory.Faithful (CategoryTheory.Limits.Cocones.functoriality F G)

@[simp]

theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents fun c => CategoryTheory.Limits.Cocones.ext (e.counitIso.app c.pt)

@[simp]

theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocones.functorialityEquivalence F e).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.functoriality (CategoryTheory.Functor.comp F e.functor) e.inverse) (CategoryTheory.Limits.Cocones.precomposeEquivalence (CategoryTheory.Functor.associator F e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ CategoryTheory.Functor.rightUnitor F).symm).functor

@[simp]

theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents fun c => CategoryTheory.Limits.Cocones.ext (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).1)

@[simp]

theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_functor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cocones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cocones.functoriality F e.functor

def CategoryTheory.Limits.Cocones.functorialityEquivalence {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F e.functor)

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.

instance CategoryTheory.Limits.Cocones.reflects_cocone_isomorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms F] (K : CategoryTheory.Functor J C) : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Limits.Cocones.functoriality K F)

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

@[simp]

theorem CategoryTheory.Functor.mapCone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (H.mapCone c).pt = H.obj c.pt

@[simp]

theorem CategoryTheory.Functor.mapCone_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J) : (H.mapCone c).π.app j = H.map (c.π.app j)

def CategoryTheory.Functor.mapCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F H)

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

@[simp]

theorem CategoryTheory.Functor.mapCocone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (H.mapCocone c).pt = H.obj c.pt

@[simp]

theorem CategoryTheory.Functor.mapCocone_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J) : (H.mapCocone c).ι.app j = H.map (c.ι.app j)

def CategoryTheory.Functor.mapCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F H)

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

def CategoryTheory.Functor.mapConeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} {c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') : H.mapCone c ⟶ H.mapCone c'

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

def CategoryTheory.Functor.mapCoconeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {c' : CategoryTheory.Limits.Cocone F} (f : c ⟶ c') : H.mapCocone c ⟶ H.mapCocone c'

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

def CategoryTheory.Functor.mapConeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F H)) : CategoryTheory.Limits.Cone F

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

def CategoryTheory.Functor.mapConeMapConeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F H)) : H.mapCone (CategoryTheory.Functor.mapConeInv H c) ≅ c

mapCone is the left inverse to mapConeInv.

def CategoryTheory.Functor.mapConeInvMapCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.mapConeInv H (H.mapCone c) ≅ c

MapCone is the right inverse to mapConeInv.

def CategoryTheory.Functor.mapCoconeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F H)) : CategoryTheory.Limits.Cocone F

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

def CategoryTheory.Functor.mapCoconeMapCoconeInv {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F H)) : H.mapCocone (CategoryTheory.Functor.mapCoconeInv H c) ≅ c

mapCocone is the left inverse to mapCoconeInv.

def CategoryTheory.Functor.mapCoconeInvMapCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.mapCoconeInv H (H.mapCocone c) ≅ c

mapCocone is the right inverse to mapCoconeInv.

@[simp]

theorem CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Functor.functorialityCompPostcompose α).inv.app X).hom = α.inv.app X.pt

@[simp]

theorem CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Functor.functorialityCompPostcompose α).hom.app X).hom = α.hom.app X.pt

def CategoryTheory.Functor.functorialityCompPostcompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.functoriality F H) (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerLeft F α.hom)) ≅ CategoryTheory.Limits.Cones.functoriality F H'

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

@[simp]

theorem CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).hom.hom = α.hom.app c.pt

@[simp]

theorem CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).inv.hom = α.inv.app c.pt

def CategoryTheory.Functor.postcomposeWhiskerLeftMapCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerLeft F α.hom)).obj (H.mapCone c) ≅ H'.mapCone c

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.mapCone using the isomorphism α is isomorphic to the cone H'.mapCone.

@[simp]

theorem CategoryTheory.Functor.mapConePostcompose_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConePostcompose H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapConePostcompose_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConePostcompose H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapConePostcompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F} : H.mapCone ((CategoryTheory.Limits.Cones.postcompose α).obj c) ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerRight α H)).obj (H.mapCone c)

mapCone 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.

@[simp]

theorem CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F} : H.mapCone ((CategoryTheory.Limits.Cones.postcomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cones.postcomposeEquivalence (CategoryTheory.isoWhiskerRight α H)).functor.obj (H.mapCone c)

mapCone commutes with postcomposeEquivalence

@[simp]

theorem CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Functor.functorialityCompPrecompose α).inv.app X).hom = α.inv.app X.pt

@[simp]

theorem CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Functor.functorialityCompPrecompose α).hom.app X).hom = α.hom.app X.pt

def CategoryTheory.Functor.functorialityCompPrecompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.functoriality F H) (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerLeft F α.inv)) ≅ CategoryTheory.Limits.Cocones.functoriality F H'

functoriality F _ ⋙ precompose (whiskerLeft F _) simplifies to functoriality F _.

@[simp]

theorem CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).hom.hom = α.hom.app c.pt

@[simp]

theorem CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).inv.hom = α.inv.app c.pt

def CategoryTheory.Functor.precomposeWhiskerLeftMapCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerLeft F α.inv)).obj (H.mapCocone c) ≅ H'.mapCocone c

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.mapCocone using the isomorphism α is isomorphic to the cocone H'.mapCocone.

@[simp]

theorem CategoryTheory.Functor.mapCoconePrecompose_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cocone G} : (CategoryTheory.Functor.mapCoconePrecompose H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapCoconePrecompose_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cocone G} : (CategoryTheory.Functor.mapCoconePrecompose H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapCoconePrecompose {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cocone G} : H.mapCocone ((CategoryTheory.Limits.Cocones.precompose α).obj c) ≅ (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerRight α H)).obj (H.mapCocone c)

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.

@[simp]

theorem CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone G} : (CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone G} : (CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone G} : H.mapCocone ((CategoryTheory.Limits.Cocones.precomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cocones.precomposeEquivalence (CategoryTheory.isoWhiskerRight α H)).functor.obj (H.mapCocone c)

mapCocone commutes with precomposeEquivalence

@[simp]

theorem CategoryTheory.Functor.mapConeWhisker_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConeWhisker H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapConeWhisker_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : (CategoryTheory.Functor.mapConeWhisker H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapConeWhisker {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : H.mapCone (CategoryTheory.Limits.Cone.whisker E c) ≅ CategoryTheory.Limits.Cone.whisker E (H.mapCone c)

mapCone commutes with whisker

@[simp]

theorem CategoryTheory.Functor.mapCoconeWhisker_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : (CategoryTheory.Functor.mapCoconeWhisker H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

@[simp]

theorem CategoryTheory.Functor.mapCoconeWhisker_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : (CategoryTheory.Functor.mapCoconeWhisker H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)

def CategoryTheory.Functor.mapCoconeWhisker {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c) ≅ CategoryTheory.Limits.Cocone.whisker E (H.mapCocone c)

mapCocone commutes with whisker

@[simp]

theorem CategoryTheory.Limits.Cocone.op_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.op c).π = CategoryTheory.NatTrans.op c.ι

@[simp]

theorem CategoryTheory.Limits.Cocone.op_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.op c).pt = Opposite.op c.pt

def CategoryTheory.Limits.Cocone.op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.op

Change a Cocone F into a Cone F.op.

@[simp]

theorem CategoryTheory.Limits.Cone.op_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.op c).pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.Cone.op_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.op c).ι = CategoryTheory.NatTrans.op c.π

def CategoryTheory.Limits.Cone.op {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.op

Change a Cone F into a Cocone F.op.

@[simp]

theorem CategoryTheory.Limits.Cocone.unop_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op) : (CategoryTheory.Limits.Cocone.unop c).π = CategoryTheory.NatTrans.removeOp c.ι

@[simp]

theorem CategoryTheory.Limits.Cocone.unop_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op) : (CategoryTheory.Limits.Cocone.unop c).pt = c.pt.unop

def CategoryTheory.Limits.Cocone.unop {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op) : CategoryTheory.Limits.Cone F

Change a Cocone F.op into a Cone F.

@[simp]

theorem CategoryTheory.Limits.Cone.unop_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : (CategoryTheory.Limits.Cone.unop c).pt = c.pt.unop

@[simp]

theorem CategoryTheory.Limits.Cone.unop_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : (CategoryTheory.Limits.Cone.unop c).ι = CategoryTheory.NatTrans.removeOp c.π

def CategoryTheory.Limits.Cone.unop {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : CategoryTheory.Limits.Cocone F

Change a Cone F.op into a Cocone F.

def CategoryTheory.Limits.coconeEquivalenceOpConeOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F ≌ (CategoryTheory.Limits.Cone F.op)ᵒᵖ

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

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coconeEquivalenceOpConeOp F).functor.obj c = Opposite.op (CategoryTheory.Limits.Cocone.op c)

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) {X : (CategoryTheory.Limits.Cone F.op)ᵒᵖ} {Y : (CategoryTheory.Limits.Cone F.op)ᵒᵖ} (f : X ⟶ Y) : ((CategoryTheory.Limits.coconeEquivalenceOpConeOp F).inverse.map f).hom = f.unop.hom.unop

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : (CategoryTheory.Limits.Cone F.op)ᵒᵖ) : (CategoryTheory.Limits.coconeEquivalenceOpConeOp F).inverse.obj c = CategoryTheory.Limits.Cone.unop c.unop

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) {X : CategoryTheory.Limits.Cocone F} {Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y) : (CategoryTheory.Limits.coconeEquivalenceOpConeOp F).functor.map f = (CategoryTheory.Limits.ConeMorphism.mk f.hom.op).op

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_unitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.coconeEquivalenceOpConeOp F).unitIso = CategoryTheory.NatIso.ofComponents fun c => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).pt)

@[simp]

theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_counitIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.coconeEquivalenceOpConeOp F).counitIso = CategoryTheory.NatIso.ofComponents fun c => Opposite.rec' (fun X => CategoryTheory.Iso.op (CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl X.pt))) c

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeLeftOp_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) (X : J) : (CategoryTheory.Limits.coneOfCoconeLeftOp c).π.app X = (c.ι.app (Opposite.op X)).op

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeLeftOp_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.coneOfCoconeLeftOp c).pt = Opposite.op c.pt

def CategoryTheory.Limits.coneOfCoconeLeftOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) : CategoryTheory.Limits.Cone F

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

@[simp]

theorem CategoryTheory.Limits.coconeLeftOpOfCone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeLeftOpOfCone c).pt = c.pt.unop

@[simp]

theorem CategoryTheory.Limits.coconeLeftOpOfCone_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) (X : Jᵒᵖ) : (CategoryTheory.Limits.coconeLeftOpOfCone c).ι.app X = (c.π.app X.unop).unop

def CategoryTheory.Limits.coconeLeftOpOfCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.leftOp

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

@[simp]

theorem CategoryTheory.Limits.coconeOfConeLeftOp_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.coconeOfConeLeftOp c).pt = Opposite.op c.pt

def CategoryTheory.Limits.coconeOfConeLeftOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) : CategoryTheory.Limits.Cocone F

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

@[simp]

theorem CategoryTheory.Limits.coconeOfConeLeftOp_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) (j : J) : (CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app j = (c.π.app (Opposite.op j)).op

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCocone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coneLeftOpOfCocone c).pt = c.pt.unop

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCocone_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) (X : Jᵒᵖ) : (CategoryTheory.Limits.coneLeftOpOfCocone c).π.app X = (c.ι.app X.unop).unop

def CategoryTheory.Limits.coneLeftOpOfCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.leftOp

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

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeRightOp_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.coneOfCoconeRightOp c).π = CategoryTheory.NatTrans.removeRightOp c.ι

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeRightOp_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.coneOfCoconeRightOp c).pt = c.pt.unop

def CategoryTheory.Limits.coneOfCoconeRightOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp) : CategoryTheory.Limits.Cone F

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

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfCone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeRightOpOfCone c).pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfCone_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeRightOpOfCone c).ι = CategoryTheory.NatTrans.rightOp c.π

def CategoryTheory.Limits.coconeRightOpOfCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.rightOp

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

@[simp]

theorem CategoryTheory.Limits.coconeOfConeRightOp_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.coconeOfConeRightOp c).pt = c.pt.unop

@[simp]

theorem CategoryTheory.Limits.coconeOfConeRightOp_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.coconeOfConeRightOp c).ι = CategoryTheory.NatTrans.removeRightOp c.π

def CategoryTheory.Limits.coconeOfConeRightOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : CategoryTheory.Limits.Cocone F

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

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCocone_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coneRightOpOfCocone c).π = CategoryTheory.NatTrans.rightOp c.ι

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCocone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coneRightOpOfCocone c).pt = Opposite.op c.pt

def CategoryTheory.Limits.coneRightOpOfCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.rightOp

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

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeUnop_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.coneOfCoconeUnop c).pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.coneOfCoconeUnop_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.coneOfCoconeUnop c).π = CategoryTheory.NatTrans.removeUnop c.ι

def CategoryTheory.Limits.coneOfCoconeUnop {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)) : CategoryTheory.Limits.Cone F

Change a cocone on F.unop : J ⥤ C into a cone on F : Jᵒᵖ ⥤ Cᵒᵖ.

@[simp]

theorem CategoryTheory.Limits.coconeUnopOfCone_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeUnopOfCone c).ι = CategoryTheory.NatTrans.unop c.π

@[simp]

theorem CategoryTheory.Limits.coconeUnopOfCone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeUnopOfCone c).pt = c.pt.unop

def CategoryTheory.Limits.coconeUnopOfCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)

Change a cone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cocone on F.unop : J ⥤ C.

@[simp]

theorem CategoryTheory.Limits.coconeOfConeUnop_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.coconeOfConeUnop c).ι = CategoryTheory.NatTrans.removeUnop c.π

@[simp]

theorem CategoryTheory.Limits.coconeOfConeUnop_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.coconeOfConeUnop c).pt = Opposite.op c.pt

def CategoryTheory.Limits.coconeOfConeUnop {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)) : CategoryTheory.Limits.Cocone F

Change a cone on F.unop : J ⥤ C into a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ.

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCocone_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coneUnopOfCocone c).π = CategoryTheory.NatTrans.unop c.ι

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCocone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.coneUnopOfCocone c).pt = c.pt.unop

def CategoryTheory.Limits.coneUnopOfCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)

Change a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cone on F.unop : J ⥤ C.

@[simp]

theorem CategoryTheory.Functor.mapConeOp_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))

@[simp]

theorem CategoryTheory.Functor.mapConeOp_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))

def CategoryTheory.Functor.mapConeOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone.op (G.mapCone t) ≅ G.op.mapCocone (CategoryTheory.Limits.Cone.op t)

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

@[simp]

theorem CategoryTheory.Functor.mapCoconeOp_inv_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) {t : CategoryTheory.Limits.Cocone F} : (CategoryTheory.Functor.mapCoconeOp G).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))

@[simp]

theorem CategoryTheory.Functor.mapCoconeOp_hom_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) {t : CategoryTheory.Limits.Cocone F} : (CategoryTheory.Functor.mapCoconeOp G).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))

def CategoryTheory.Functor.mapCoconeOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) {t : CategoryTheory.Limits.Cocone F} : CategoryTheory.Limits.Cocone.op (G.mapCocone t) ≅ G.op.mapCone (CategoryTheory.Limits.Cocone.op t)

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