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.

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

Equations

• F.cones = (CategoryTheory.Functor.const J).op.comp (CategoryTheory.yoneda.obj F)

@[simp]

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

@[simp]

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

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

Equations

• F.cocones = (CategoryTheory.Functor.const J).comp (CategoryTheory.coyoneda.obj (Opposite.op F))

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

• pt : C

  An object of C

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

  A natural transformation from the constant functor at X to F

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

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.

• pt : C

  An object of C

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

  A natural transformation from F to the constant functor at pt

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

• c.extend f = { pt := X, π := CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f) c.π }

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

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

Equations

• c.extend f = { pt := X, ι := CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f) }

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.extend_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) {X : C} (f : c.pt ⟶ X) : (c.extend f).ι = CategoryStruct.comp c.ι ((Functor.const J).map f)

@[simp]

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

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

Whisker a cone by precomposition of a functor.

Equations

• CategoryTheory.Limits.Cone.whisker E c = { pt := c.pt, π := E.whiskerLeft c.π }

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

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

Equations

• CategoryTheory.Limits.Cocone.whisker E c = { pt := c.pt, ι := E.whiskerLeft c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

• hom : A.pt ⟶ B.pt

  A morphism between the two vertex objects of the cones

• w (j : J) : CategoryStruct.comp self.hom (B.π.app j) = A.π.app j

  The triangle consisting of the two natural transformations and hom commutes

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

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

• hom : A.pt ⟶ B.pt

  A morphism between the (co)vertex objects in C

• w (j : J) : CategoryStruct.comp (A.ι.app j) self.hom = B.ι.app j

  The triangle made from the two natural transformations and hom commutes

@[simp]

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

The triangle made from the two natural transformations and hom commutes

@[simp]

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

The triangle consisting of the two natural transformations and hom commutes

@[implicit_reducible]

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

Equations

• CategoryTheory.Limits.inhabitedConeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }

@[implicit_reducible]

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

Equations

• CategoryTheory.Limits.inhabitedCoconeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }

@[implicit_reducible]

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

The category of cones on a given diagram.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

The category of cocones on a given diagram.

Equations

• CategoryTheory.Limits.Cocone.category = CategoryTheory.Category.mk' ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.category_comp_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {x✝ x✝¹ x✝² : Cocone F} (x✝³ : CoconeMorphism x✝ x✝¹) (x✝⁴ : CoconeMorphism x✝¹ x✝²) : (CategoryStruct.comp x✝³ x✝⁴).hom = CategoryStruct.comp x✝³.hom x✝⁴.hom

@[simp]

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

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

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

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

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

@[simp]

theorem CategoryTheory.Limits.ConeMorphism.hom_inv_id {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) : CategoryStruct.comp f.hom.hom f.inv.hom = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.CoconeMorphism.hom_inv_id {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) : CategoryStruct.comp f.hom.hom f.inv.hom = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.CoconeMorphism.hom_inv_id_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp f.hom.hom (CategoryStruct.comp f.inv.hom h) = h

@[simp]

theorem CategoryTheory.Limits.ConeMorphism.hom_inv_id_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp f.hom.hom (CategoryStruct.comp f.inv.hom h) = h

@[simp]

theorem CategoryTheory.Limits.ConeMorphism.inv_hom_id {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) : CategoryStruct.comp f.inv.hom f.hom.hom = CategoryStruct.id d.pt

@[simp]

theorem CategoryTheory.Limits.CoconeMorphism.inv_hom_id {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) : CategoryStruct.comp f.inv.hom f.hom.hom = CategoryStruct.id d.pt

@[simp]

theorem CategoryTheory.Limits.CoconeMorphism.inv_hom_id_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp f.inv.hom (CategoryStruct.comp f.hom.hom h) = h

@[simp]

theorem CategoryTheory.Limits.ConeMorphism.inv_hom_id_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp f.inv.hom (CategoryStruct.comp f.hom.hom h) = h

instance CategoryTheory.Limits.instIsIsoHomHomCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) : IsIso f.hom.hom

instance CategoryTheory.Limits.instIsIsoHomHomCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) : IsIso f.inv.hom

instance CategoryTheory.Limits.instIsIsoHomInvCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cone F} (f : c ≅ d) : IsIso f.inv.hom

instance CategoryTheory.Limits.instIsIsoHomInvCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c d : Cocone F} (f : c ≅ d) : IsIso f.hom.hom

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.Cone.ext φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Limits.Cocone.ext_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.ι.app j = CategoryStruct.comp (c'.ι.app j) φ.inv := by cat_disch) : c ≅ c'

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

Equations

• CategoryTheory.Limits.Cocone.ext_inv φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.ext_inv_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.ι.app j = CategoryStruct.comp (c'.ι.app j) φ.inv := by cat_disch) : (ext_inv φ w).hom.hom = φ.hom

@[simp]

theorem CategoryTheory.Limits.Cocone.ext_inv_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.ι.app j = CategoryStruct.comp (c'.ι.app j) φ.inv := by cat_disch) : (ext_inv φ w).inv.hom = φ.inv

@[simp]

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

def CategoryTheory.Limits.Cone.ext_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : c ≅ c'

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

Equations

• CategoryTheory.Limits.Cone.ext_inv φ w = CategoryTheory.Limits.Cone.ext φ ⋯

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

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

Equations

• CategoryTheory.Limits.Cocone.ext φ w = CategoryTheory.Limits.Cocone.ext_inv φ ⋯

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cone.ext_inv_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : (ext_inv φ w).inv.hom = φ.inv

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cone.ext_inv_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : (ext_inv φ w).hom.hom = φ.hom

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

Eta rule for cones.

Equations

• c.eta = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl c.pt) ⋯

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

Eta rule for cocones.

Equations

• c.eta = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl c.pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

There is a morphism from an extended cone to the original cone.

Equations

• s.extendHom f = { hom := f, w := ⋯ }

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

There is a morphism from a cocone to its extension.

Equations

• s.extendHom f = { hom := f, w := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.extendHom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X : C} (f : s.pt ⟶ X) : (s.extendHom f).hom = f

def CategoryTheory.Limits.Cone.extendId {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) : s.extend (CategoryStruct.id s.pt) ≅ s

Extending a cone by the identity does nothing.

Equations

• s.extendId = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.id s.pt)).pt) ⋯

def CategoryTheory.Limits.Cocone.extendId {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) : s.extend (CategoryStruct.id s.pt) ≅ s

Extending a cocone by the identity does nothing.

Equations

• s.extendId = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.id s.pt)).pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cone.extendComp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : s.extend (CategoryStruct.comp f g) ≅ (s.extend g).extend f

Extending a cone by a composition is the same as extending the cone twice.

Equations

• s.extendComp f g = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.comp f g)).pt) ⋯

def CategoryTheory.Limits.Cocone.extendComp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X) : s.extend (CategoryStruct.comp g f) ≅ (s.extend g).extend f

Extending a cocone by a composition is the same as extending the cone twice.

Equations

• x✝⁴.extendComp x✝¹ x✝ = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl (x✝⁴.extend (CategoryTheory.CategoryStruct.comp x✝¹ x✝)).pt) ⋯

@[simp]

theorem CategoryTheory.Limits.Cocone.extendComp_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X) : (s.extendComp g f).hom.hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.Cone.extendComp_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : (s.extendComp f g).hom.hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.Cone.extendComp_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : (s.extendComp f g).inv.hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.Cocone.extendComp_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X) : (s.extendComp g f).inv.hom = CategoryStruct.id X

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

A cone extended by an isomorphism is isomorphic to the original cone.

Equations

• s.extendIso f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Limits.Cocone.extendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.hom

A cocone extended by an isomorphism is isomorphic to the original cone.

Equations

• s.extendIso f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Cocone.extendIso_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).inv.hom = f.inv

@[simp]

theorem CategoryTheory.Limits.Cocone.extendIso_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).hom.hom = f.hom

@[simp]

theorem CategoryTheory.Limits.Cone.extendIso_hom_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).hom.hom = f.hom

@[simp]

theorem CategoryTheory.Limits.Cone.extendIso_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).inv.hom = f.inv

instance CategoryTheory.Limits.Cone.instIsIsoExtendHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cone F} {X : C} (f : X ⟶ s.pt) [IsIso f] : IsIso (s.extendHom f)

instance CategoryTheory.Limits.Cocone.instIsIsoExtendHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cocone F} {X : C} (f : s.pt ⟶ X) [IsIso f] : IsIso (s.extendHom f)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Limits.Cone.equivalenceOfReindexing e α = (CategoryTheory.Limits.Cone.whiskeringEquivalence e).trans (CategoryTheory.Limits.Cone.postcomposeEquivalence α)

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

Equations

• CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α = (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).trans (CategoryTheory.Limits.Cocone.precomposeEquivalence α)

@[simp]

theorem CategoryTheory.Limits.Cocone.equivalenceOfReindexing_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {G : Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G) : (equivalenceOfReindexing e α).counitIso = (((precompose α.hom).comp ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv))).associator (whiskering e.functor) (precompose α.inv)).symm ≪≫ Functor.isoWhiskerRight ((precompose α.hom).associator ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv)) (whiskering e.functor)) (precompose α.inv) ≪≫ Functor.isoWhiskerRight ((precompose α.hom).isoWhiskerLeft (NatIso.ofComponents' (fun (s : Cocone (e.functor.comp F)) => ext_inv (Iso.refl s.pt) ⋯) ⋯)) (precompose α.inv) ≪≫ Functor.isoWhiskerRight (precompose α.hom).rightUnitor (precompose α.inv) ≪≫ NatIso.ofComponents' (fun (s : Cocone G) => ext_inv (Iso.refl s.pt) ⋯) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.equivalenceOfReindexing_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {G : Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G) : (equivalenceOfReindexing e α).unitIso = NatIso.ofComponents' (fun (s : Cocone F) => ext_inv (Iso.refl s.pt) ⋯) ⋯ ≪≫ Functor.isoWhiskerRight (whiskering e.functor).rightUnitor.symm ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv)) ≪≫ Functor.isoWhiskerRight ((whiskering e.functor).isoWhiskerLeft (NatIso.ofComponents' (fun (s : Cocone (e.functor.comp F)) => ext_inv (Iso.refl s.pt) ⋯) ⋯)) ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv)) ≪≫ Functor.isoWhiskerRight ((whiskering e.functor).associator (precompose α.inv) (precompose α.hom)).symm ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv)) ≪≫ ((whiskering e.functor).comp (precompose α.inv)).associator (precompose α.hom) ((whiskering e.inverse).comp (precompose (e.invFunIdAssoc F).inv))

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

Forget the cone structure and obtain just the cone point.

Equations

• CategoryTheory.Limits.Cone.forget F = { obj := fun (t : CategoryTheory.Limits.Cone F) => t.pt, map := fun {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

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

Forget the cocone structure and obtain just the cocone point.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Functoriality is functorial.

Equations

• One or more equations did not get rendered due to their size.

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

Functoriality is functorial.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

def CategoryTheory.Limits.Cone.functorialityEquivalence {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (F : Functor J C) (e : C ≌ D) : Cone F ≌ Cone (F.comp 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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.Cocone.functorialityEquivalence {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (F : Functor J C) (e : C ≌ D) : Cocone F ≌ Cocone (F.comp 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[deprecated CategoryTheory.Limits.Cone.ext (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.ext.

---

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

Equations

• @CategoryTheory.Limits.Cones.ext = @CategoryTheory.Limits.Cone.ext

@[deprecated CategoryTheory.Limits.Cone.eta (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.eta.

---

Eta rule for cones.

Equations

• @CategoryTheory.Limits.Cones.eta = @CategoryTheory.Limits.Cone.eta

@[deprecated CategoryTheory.Limits.Cone.cone_iso_of_hom_iso (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.cone_iso_of_hom_iso.

---

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

@[deprecated CategoryTheory.Limits.Cone.extendHom (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.extendHom.

---

There is a morphism from an extended cone to the original cone.

Equations

• @CategoryTheory.Limits.Cones.extend = @CategoryTheory.Limits.Cone.extendHom

@[deprecated CategoryTheory.Limits.Cone.extendId (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.extendId.

---

Extending a cone by the identity does nothing.

Equations

• @CategoryTheory.Limits.Cones.extendId = @CategoryTheory.Limits.Cone.extendId

@[deprecated CategoryTheory.Limits.Cone.extendComp (since := "2026-03-06")]

def CategoryTheory.Limits.Cones.extendComp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : s.extend (CategoryStruct.comp f g) ≅ (s.extend g).extend f

Alias of CategoryTheory.Limits.Cone.extendComp.

---

Extending a cone by a composition is the same as extending the cone twice.

Equations

• @CategoryTheory.Limits.Cones.extendComp = @CategoryTheory.Limits.Cone.extendComp

@[deprecated CategoryTheory.Limits.Cone.extendIso (since := "2026-03-06")]

def CategoryTheory.Limits.Cones.extendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.inv

Alias of CategoryTheory.Limits.Cone.extendIso.

---

A cone extended by an isomorphism is isomorphic to the original cone.

Equations

• @CategoryTheory.Limits.Cones.extendIso = @CategoryTheory.Limits.Cone.extendIso

@[deprecated CategoryTheory.Limits.Cone.postcompose (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.postcompose.

---

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

Equations

• @CategoryTheory.Limits.Cones.postcompose = @CategoryTheory.Limits.Cone.postcompose

@[deprecated CategoryTheory.Limits.Cone.postcomposeComp (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.postcomposeComp.

---

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

Equations

• @CategoryTheory.Limits.Cones.postcomposeComp = @CategoryTheory.Limits.Cone.postcomposeComp

@[deprecated CategoryTheory.Limits.Cone.postcomposeId (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.postcomposeId.

---

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

Equations

• @CategoryTheory.Limits.Cones.postcomposeId = @CategoryTheory.Limits.Cone.postcomposeId

@[deprecated CategoryTheory.Limits.Cone.postcomposeEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.postcomposeEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cones.postcomposeEquivalence = @CategoryTheory.Limits.Cone.postcomposeEquivalence

@[deprecated CategoryTheory.Limits.Cone.whiskering (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.whiskering.

---

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

Equations

• @CategoryTheory.Limits.Cones.whiskering = @CategoryTheory.Limits.Cone.whiskering

@[deprecated CategoryTheory.Limits.Cone.whiskeringEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.whiskeringEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cones.whiskeringEquivalence = @CategoryTheory.Limits.Cone.whiskeringEquivalence

@[deprecated CategoryTheory.Limits.Cone.equivalenceOfReindexing (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.equivalenceOfReindexing.

---

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

Equations

• @CategoryTheory.Limits.Cones.equivalenceOfReindexing = @CategoryTheory.Limits.Cone.equivalenceOfReindexing

@[deprecated CategoryTheory.Limits.Cone.forget (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.forget.

---

Forget the cone structure and obtain just the cone point.

Equations

• @CategoryTheory.Limits.Cones.forget = @CategoryTheory.Limits.Cone.forget

@[deprecated CategoryTheory.Limits.Cone.functoriality (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.functoriality.

---

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

Equations

• @CategoryTheory.Limits.Cones.functoriality = @CategoryTheory.Limits.Cone.functoriality

@[deprecated CategoryTheory.Limits.Cone.functorialityCompFunctoriality (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.functorialityCompFunctoriality.

---

Functoriality is functorial.

Equations

• @CategoryTheory.Limits.Cones.functorialityCompFunctoriality = @CategoryTheory.Limits.Cone.functorialityCompFunctoriality

@[deprecated CategoryTheory.Limits.Cone.functoriality_full (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.functoriality_full.

@[deprecated CategoryTheory.Limits.Cone.functoriality_faithful (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.functoriality_faithful.

@[deprecated CategoryTheory.Limits.Cone.functorialityEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.functorialityEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cones.functorialityEquivalence = @CategoryTheory.Limits.Cone.functorialityEquivalence

@[deprecated CategoryTheory.Limits.Cone.reflects_cone_isomorphism (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cone.reflects_cone_isomorphism.

---

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

@[deprecated CategoryTheory.Limits.Cocone.ext (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.ext.

---

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

Equations

• @CategoryTheory.Limits.Cocones.ext = @CategoryTheory.Limits.Cocone.ext

@[deprecated CategoryTheory.Limits.Cocone.eta (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.eta.

---

Eta rule for cocones.

Equations

• @CategoryTheory.Limits.Cocones.eta = @CategoryTheory.Limits.Cocone.eta

@[deprecated CategoryTheory.Limits.Cocone.cocone_iso_of_hom_iso (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.cocone_iso_of_hom_iso.

---

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

@[deprecated CategoryTheory.Limits.Cocone.extendHom (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.extendHom.

---

There is a morphism from a cocone to its extension.

Equations

• @CategoryTheory.Limits.Cocones.extend = @CategoryTheory.Limits.Cocone.extendHom

@[deprecated CategoryTheory.Limits.Cocone.extendId (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.extendId.

---

Extending a cocone by the identity does nothing.

Equations

• @CategoryTheory.Limits.Cocones.extendId = @CategoryTheory.Limits.Cocone.extendId

@[deprecated CategoryTheory.Limits.Cocone.extendComp (since := "2026-03-06")]

def CategoryTheory.Limits.Cocones.extendComp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X) : s.extend (CategoryStruct.comp g f) ≅ (s.extend g).extend f

Alias of CategoryTheory.Limits.Cocone.extendComp.

---

Extending a cocone by a composition is the same as extending the cone twice.

Equations

• @CategoryTheory.Limits.Cocones.extendComp = @CategoryTheory.Limits.Cocone.extendComp

@[deprecated CategoryTheory.Limits.Cocone.extendIso (since := "2026-03-06")]

def CategoryTheory.Limits.Cocones.extendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (s : Cocone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.hom

Alias of CategoryTheory.Limits.Cocone.extendIso.

---

A cocone extended by an isomorphism is isomorphic to the original cone.

Equations

• @CategoryTheory.Limits.Cocones.extendIso = @CategoryTheory.Limits.Cocone.extendIso

@[deprecated CategoryTheory.Limits.Cocone.precompose (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.precompose.

---

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

Equations

• @CategoryTheory.Limits.Cocones.postcompose = @CategoryTheory.Limits.Cocone.precompose

@[deprecated CategoryTheory.Limits.Cocone.precomposeComp (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.precomposeComp.

---

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

Equations

• @CategoryTheory.Limits.Cocones.postcomposeComp = @CategoryTheory.Limits.Cocone.precomposeComp

@[deprecated CategoryTheory.Limits.Cocone.precomposeId (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.precomposeId.

---

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

Equations

• @CategoryTheory.Limits.Cocones.postcomposeId = @CategoryTheory.Limits.Cocone.precomposeId

@[deprecated CategoryTheory.Limits.Cocone.precomposeEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.precomposeEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cocones.postcomposeEquivalence = @CategoryTheory.Limits.Cocone.precomposeEquivalence

@[deprecated CategoryTheory.Limits.Cocone.whiskering (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.whiskering.

---

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

Equations

• @CategoryTheory.Limits.Cocones.whiskering = @CategoryTheory.Limits.Cocone.whiskering

@[deprecated CategoryTheory.Limits.Cocone.whiskeringEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.whiskeringEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cocones.whiskeringEquivalence = @CategoryTheory.Limits.Cocone.whiskeringEquivalence

@[deprecated CategoryTheory.Limits.Cocone.equivalenceOfReindexing (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.equivalenceOfReindexing.

---

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

Equations

• @CategoryTheory.Limits.Cocones.equivalenceOfReindexing = @CategoryTheory.Limits.Cocone.equivalenceOfReindexing

@[deprecated CategoryTheory.Limits.Cocone.forget (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.forget.

---

Forget the cocone structure and obtain just the cocone point.

Equations

• @CategoryTheory.Limits.Cocones.forget = @CategoryTheory.Limits.Cocone.forget

@[deprecated CategoryTheory.Limits.Cocone.functoriality (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.functoriality.

---

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

Equations

• @CategoryTheory.Limits.Cocones.functoriality = @CategoryTheory.Limits.Cocone.functoriality

@[deprecated CategoryTheory.Limits.Cocone.functorialityCompFunctoriality (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.functorialityCompFunctoriality.

---

Functoriality is functorial.

Equations

• @CategoryTheory.Limits.Cocones.functorialityCompFunctoriality = @CategoryTheory.Limits.Cocone.functorialityCompFunctoriality

@[deprecated CategoryTheory.Limits.Cocone.functoriality_full (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.functoriality_full.

@[deprecated CategoryTheory.Limits.Cocone.functoriality_faithful (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.functoriality_faithful.

@[deprecated CategoryTheory.Limits.Cocone.functorialityEquivalence (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.functorialityEquivalence.

---

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

Equations

• @CategoryTheory.Limits.Cocones.functorialityEquivalence = @CategoryTheory.Limits.Cocone.functorialityEquivalence

@[deprecated CategoryTheory.Limits.Cocone.reflects_cocone_isomorphism (since := "2026-03-06")]

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

Alias of CategoryTheory.Limits.Cocone.reflects_cocone_isomorphism.

---

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

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

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

Equations

• H.mapCone c = (CategoryTheory.Limits.Cone.functoriality F H).obj c

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

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

Equations

• H.mapCocone c = (CategoryTheory.Limits.Cocone.functoriality F H).obj c

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The construction mapCone respects functor composition.

Equations

• CategoryTheory.Functor.mapConeMapCone c = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H'.mapCone (H.mapCone c)).pt) ⋯

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

The construction mapCocone respects functor composition.

Equations

• CategoryTheory.Functor.mapCoconeMapCocone c = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl (H'.mapCocone (H.mapCocone c)).pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.mapConeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (H : Functor C D) {F : Functor J C} {c c' : 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.

Equations

• H.mapConeMorphism f = (CategoryTheory.Limits.Cone.functoriality F H).map f

def CategoryTheory.Functor.mapCoconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (H : Functor C D) {F : Functor J C} {c c' : 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.

Equations

• H.mapCoconeMorphism f = (CategoryTheory.Limits.Cocone.functoriality F H).map f

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

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

Equations

• H.mapConeInv c = (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).inverse.obj c

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

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

Equations

• H.mapCoconeInv c = (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).inverse.obj c

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

mapCone is the left inverse to mapConeInv.

Equations

• CategoryTheory.Functor.mapConeMapConeInv H c = (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).counitIso.app c

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

mapCocone is the left inverse to mapCoconeInv.

Equations

• CategoryTheory.Functor.mapCoconeMapCoconeInv H c = (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).counitIso.app c

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

mapCone is the right inverse to mapConeInv.

Equations

• CategoryTheory.Functor.mapConeInvMapCone H c = (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c

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

mapCocone is the right inverse to mapCoconeInv.

Equations

• CategoryTheory.Functor.mapCoconeInvMapCocone H c = (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c

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

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

Equations

• CategoryTheory.Functor.functorialityCompPostcompose α = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cone F) => CategoryTheory.Limits.Cone.ext (α.app c.pt) ⋯) ⋯

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

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

Equations

• CategoryTheory.Functor.functorialityCompPrecompose α = CategoryTheory.NatIso.ofComponents' (fun (c : CategoryTheory.Limits.Cocone F) => CategoryTheory.Limits.Cocone.ext_inv (α.app c.pt) ⋯) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.postcomposeWhiskerLeftMapCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F : Functor J C} {H H' : Functor C D} (α : H ≅ H') (c : Limits.Cone F) : (Limits.Cone.postcompose (F.whiskerLeft α.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.

Equations

• CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c = (CategoryTheory.Functor.functorialityCompPostcompose α).app c

def CategoryTheory.Functor.precomposeWhiskerLeftMapCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {F : Functor J C} {H H' : Functor C D} (α : H ≅ H') (c : Limits.Cocone F) : (Limits.Cocone.precompose (F.whiskerLeft α.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.

Equations

• CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c = (CategoryTheory.Functor.functorialityCompPrecompose α).app c

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.mapConePostcompose {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (H : Functor C D) {F G : Functor J C} {α : F ⟶ G} {c : Limits.Cone F} : H.mapCone ((Limits.Cone.postcompose α).obj c) ≅ (Limits.Cone.postcompose (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.

Equations

• H.mapConePostcompose = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cone.postcompose α).obj c)).pt) ⋯

def CategoryTheory.Functor.mapCoconePrecompose {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (H : Functor C D) {F G : Functor J C} {α : G ⟶ F} {c : Limits.Cocone F} : H.mapCocone ((Limits.Cocone.precompose α).obj c) ≅ (Limits.Cocone.precompose (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.

Equations

• H.mapCoconePrecompose = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocone.precompose α).obj c)).pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

mapCone commutes with postcomposeEquivalence

Equations

• H.mapConePostcomposeEquivalenceFunctor = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor.obj c)).pt) ⋯

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

mapCocone commutes with precomposeEquivalence

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

mapCone commutes with whisker

Equations

• H.mapConeWhisker = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H.mapCone (CategoryTheory.Limits.Cone.whisker E c)).pt) ⋯

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

mapCocone commutes with whisker

Equations

• H.mapCoconeWhisker = CategoryTheory.Limits.Cocone.ext_inv (CategoryTheory.Iso.refl (H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c)).pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Change a Cone F into a Cocone F.op.

Equations

• c.op = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.op c.π }

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

Change a Cocone F into a Cone F.op.

Equations

• c.op = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.op c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Change a Cone F.op into a Cocone F.

Equations

• c.unop = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeOp c.π }

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

Change a Cocone F.op into a Cone F.

Equations

• c.unop = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeOp c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Cones on F : J ⥤ C are equivalent to cocones on F.op : Jᵒᵖ ⥤ Cᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

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

Cocones on F : J ⥤ C are equivalent to cones on F.op : Jᵒᵖ ⥤ Cᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coconeOpEquiv_functor_map_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {x✝ x✝¹ : (Cocone F)ᵒᵖ} (f : x✝ ⟶ x✝¹) : (coconeOpEquiv.functor.map f).hom = f.unop.hom.op

@[simp]

theorem CategoryTheory.Limits.coconeOpEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {x✝ x✝¹ : Cone F.op} (f : x✝ ⟶ x✝¹) : coconeOpEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneOpEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X✝ Y✝ : Cocone F.op} (f : X✝ ⟶ Y✝) : coneOpEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneOpEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} : coneOpEquiv.counitIso = Iso.refl ({ obj := fun (c : Cocone F.op) => Opposite.op c.unop, map := fun {X Y : Cocone F.op} (f : X ⟶ Y) => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cone F)ᵒᵖ) => (Opposite.unop c).op, map := fun {X Y : (Cone F)ᵒᵖ} (f : X ⟶ Y) => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Limits.coneOpEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} : coneOpEquiv.unitIso = Iso.refl (Functor.id (Cone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coconeOpEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} : coconeOpEquiv.unitIso = Iso.refl (Functor.id (Cocone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coconeOpEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} : coconeOpEquiv.counitIso = Iso.refl ({ obj := fun (c : Cone F.op) => Opposite.op c.unop, map := fun {x x_1 : Cone F.op} (f : x ⟶ x_1) => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cocone F)ᵒᵖ) => (Opposite.unop c).op, map := fun {x x_1 : (Cocone F)ᵒᵖ} (f : x ⟶ x_1) => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.coneOfCoconeLeftOp c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeLeftOp c.ι }

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

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

Equations

• CategoryTheory.Limits.coconeOfConeLeftOp c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeLeftOp c.π }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.coconeLeftOpOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.leftOp c.π }

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

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

Equations

• CategoryTheory.Limits.coneLeftOpOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.leftOp c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Cones on F : J ⥤ Cᵒᵖ are equivalent to cocones on F.leftOp : Jᵒᵖ ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

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

Cocones on F : J ⥤ Cᵒᵖ are equivalent to cones on F.leftOp : Jᵒᵖ ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} : coconeLeftOpOfConeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cocone F.leftOp) => Opposite.op (coneOfCoconeLeftOp c), map := fun {X Y : Cocone F.leftOp} (f : X ⟶ Y) => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cone F)ᵒᵖ) => coconeLeftOpOfCone (Opposite.unop c), map := fun {X Y : (Cone F)ᵒᵖ} (f : X ⟶ Y) => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} : coneLeftOpOfCoconeEquiv.unitIso = Iso.refl (Functor.id (Cocone F)ᵒᵖ)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_map_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} {x✝ x✝¹ : (Cocone F)ᵒᵖ} (f : x✝ ⟶ x✝¹) : (coneLeftOpOfCoconeEquiv.functor.map f).hom = f.unop.hom.unop

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} : coneLeftOpOfCoconeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cone F.leftOp) => Opposite.op (coconeOfConeLeftOp c), map := fun {x x_1 : Cone F.leftOp} (f : x ⟶ x_1) => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cocone F)ᵒᵖ) => coneLeftOpOfCocone (Opposite.unop c), map := fun {x x_1 : (Cocone F)ᵒᵖ} (f : x ⟶ x_1) => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coconeLeftOpOfConeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} : coconeLeftOpOfConeEquiv.unitIso = Iso.refl (Functor.id (Cone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} {x✝ x✝¹ : Cone F.leftOp} (f : x✝ ⟶ x✝¹) : coneLeftOpOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J Cᵒᵖ} {X✝ Y✝ : Cocone F.leftOp} (f : X✝ ⟶ Y✝) : coconeLeftOpOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }

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

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

Equations

• CategoryTheory.Limits.coneOfCoconeRightOp c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeRightOp c.ι }

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

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

Equations

• CategoryTheory.Limits.coconeOfConeRightOp c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeRightOp c.π }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.coconeRightOpOfCone c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.rightOp c.π }

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

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

Equations

• CategoryTheory.Limits.coneRightOpOfCocone c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.rightOp c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Cones on F : Jᵒᵖ ⥤ C are equivalent to cocones on F.rightOp : J ⥤ Cᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

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

Cocones on F : Jᵒᵖ ⥤ C are equivalent to cones on F.rightOp : J ⥤ Cᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} {X✝ Y✝ : Cocone F.rightOp} (f : X✝ ⟶ Y✝) : coconeRightOpOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfConeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} : coconeRightOpOfConeEquiv.unitIso = Iso.refl (Functor.id (Cone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} : coconeRightOpOfConeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cocone F.rightOp) => Opposite.op (coneOfCoconeRightOp c), map := fun {X Y : Cocone F.rightOp} (f : X ⟶ Y) => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cone F)ᵒᵖ) => coconeRightOpOfCone (Opposite.unop c), map := fun {X Y : (Cone F)ᵒᵖ} (f : X ⟶ Y) => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} : coneRightOpOfCoconeEquiv.unitIso = Iso.refl (Functor.id (Cocone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} {x✝ x✝¹ : (Cocone F)ᵒᵖ} (f : x✝ ⟶ x✝¹) : (coneRightOpOfCoconeEquiv.functor.map f).hom = f.unop.hom.op

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} (c : (Cone F)ᵒᵖ) : coconeRightOpOfConeEquiv.functor.obj c = coconeRightOpOfCone (Opposite.unop c)

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} (c : (Cocone F)ᵒᵖ) : coneRightOpOfCoconeEquiv.functor.obj c = coneRightOpOfCocone (Opposite.unop c)

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} {x✝ x✝¹ : Cone F.rightOp} (f : x✝ ⟶ x✝¹) : coneRightOpOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} (c : Cone F.rightOp) : coneRightOpOfCoconeEquiv.inverse.obj c = Opposite.op (coconeOfConeRightOp c)

@[simp]

theorem CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} : coneRightOpOfCoconeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cone F.rightOp) => Opposite.op (coconeOfConeRightOp c), map := fun {x x_1 : Cone F.rightOp} (f : x ⟶ x_1) => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cocone F)ᵒᵖ) => coneRightOpOfCocone (Opposite.unop c), map := fun {x x_1 : (Cocone F)ᵒᵖ} (f : x ⟶ x_1) => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ C} (c : Cocone F.rightOp) : coconeRightOpOfConeEquiv.inverse.obj c = Opposite.op (coneOfCoconeRightOp c)

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

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

Equations

• CategoryTheory.Limits.coneOfCoconeUnop c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeUnop c.ι }

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

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

Equations

• CategoryTheory.Limits.coconeOfConeUnop c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeUnop c.π }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.coconeUnopOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.unop c.π }

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

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

Equations

• CategoryTheory.Limits.coneUnopOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.unop c.ι }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Cones on F : Jᵒᵖ ⥤ Cᵒᵖ are equivalent to cocones on F.unop : J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

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

Cocones on F : Jᵒᵖ ⥤ Cᵒᵖ are equivalent to cones on F.unop : J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coconeUnopOfConeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} : coconeUnopOfConeEquiv.unitIso = Iso.refl (Functor.id (Cone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} : coneUnopOfCoconeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cone F.unop) => Opposite.op (coconeOfConeUnop c), map := fun {x x_1 : Cone F.unop} (f : x ⟶ x_1) => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cocone F)ᵒᵖ) => coneUnopOfCocone (Opposite.unop c), map := fun {x x_1 : (Cocone F)ᵒᵖ} (f : x ⟶ x_1) => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCoconeEquiv_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} : coneUnopOfCoconeEquiv.unitIso = Iso.refl (Functor.id (Cocone F)ᵒᵖ)

@[simp]

theorem CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} {X✝ Y✝ : Cocone F.unop} (f : X✝ ⟶ Y✝) : coconeUnopOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} {x✝ x✝¹ : Cone F.unop} (f : x✝ ⟶ x✝¹) : coneUnopOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_map_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} {x✝ x✝¹ : (Cocone F)ᵒᵖ} (f : x✝ ⟶ x✝¹) : (coneUnopOfCoconeEquiv.functor.map f).hom = f.unop.hom.unop

@[simp]

theorem CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor Jᵒᵖ Cᵒᵖ} : coconeUnopOfConeEquiv.counitIso = Iso.refl ({ obj := fun (c : Cocone F.unop) => Opposite.op (coneOfCoconeUnop c), map := fun {X Y : Cocone F.unop} (f : X ⟶ Y) => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (c : (Cone F)ᵒᵖ) => coconeUnopOfCone (Opposite.unop c), map := fun {X Y : (Cone F)ᵒᵖ} (f : X ⟶ Y) => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })

@[simp]

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

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

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

Equations

• CategoryTheory.Functor.mapConeOp G t = CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl (G.mapCone t).op.pt) ⋯

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

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

Equations

• CategoryTheory.Functor.mapCoconeOp G t = CategoryTheory.Limits.Cone.ext_inv (CategoryTheory.Iso.refl (G.mapCocone t).op.pt) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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