# Cones and cocones #

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

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

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

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

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

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

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

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

@[simp]
theorem CategoryTheory.Functor.cones_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : Cᵒᵖ) :
F.cones.obj X = (.obj F)
@[simp]
theorem CategoryTheory.Functor.cones_map_app {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : Cᵒᵖ} (f : X Y) (a : (CategoryTheory.yoneda.obj F).obj (.op.obj X)) (X_1 : J), (F.cones.map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)
def CategoryTheory.Functor.cones {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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 = .op.comp (CategoryTheory.yoneda.obj F)
Instances For
@[simp]
theorem CategoryTheory.Functor.cocones_map_app {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : C} (f : X Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F)).obj (.obj X)) (X_1 : J), (F.cocones.map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f
@[simp]
theorem CategoryTheory.Functor.cocones_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : C) :
F.cocones.obj X = (F .obj X)
def CategoryTheory.Functor.cocones {J : Type u₁} [] {C : Type u₃} [] (F : ) :
CategoryTheory.Functor C (Type (max u₁ v₃))

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

Equations
• F.cocones = .comp (CategoryTheory.coyoneda.obj (Opposite.op F))
Instances For
@[simp]
theorem CategoryTheory.cones_map_app_app (J : Type u₁) [] (C : Type u₃) [] :
∀ {X Y : } (f : X Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj (.op.obj X_1)) (X_2 : J), ((.map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (a.app X_2) (f.app X_2)
@[simp]
theorem CategoryTheory.cones_obj_map_app (J : Type u₁) [] (C : Type u₃) [] (F : ) :
∀ {X Y : Cᵒᵖ} (f : X Y) (a : (CategoryTheory.yoneda.obj F).obj (.op.obj X)) (X_1 : J), ((.obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)
@[simp]
theorem CategoryTheory.cones_obj_obj (J : Type u₁) [] (C : Type u₃) [] (F : ) (X : Cᵒᵖ) :
(.obj F).obj X = (.obj F)
def CategoryTheory.cones (J : Type u₁) [] (C : Type u₃) [] :

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.
Instances For
@[simp]
theorem CategoryTheory.cocones_map_app_app (J : Type u₁) [] (C : Type u₃) [] :
∀ {X Y : ᵒᵖ} (f : X Y) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj (.obj X_1)) (X_2 : J), ((.map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (f.unop.app X_2) (a.app X_2)
@[simp]
theorem CategoryTheory.cocones_obj_obj (J : Type u₁) [] (C : Type u₃) [] (F : ᵒᵖ) (X : C) :
(.obj F).obj X = ( .obj X)
@[simp]
theorem CategoryTheory.cocones_obj_map_app (J : Type u₁) [] (C : Type u₃) [] (F : ᵒᵖ) :
∀ {X Y : C} (f : X Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op )).obj (.obj X)) (X_1 : J), ((.obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f
def CategoryTheory.cocones (J : Type u₁) [] (C : Type u₃) [] :

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.
Instances For
structure CategoryTheory.Limits.Cone {J : Type u₁} [] {C : Type u₃} [] (F : ) :
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

• π : .obj self.pt F

A natural transformation from the constant functor at X to F

Instances For
instance CategoryTheory.Limits.inhabitedCone {C : Type u₃} [] (F : ) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Limits.Cone.w_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') {Z : C} (h : F.obj j' Z) :
@[simp]
theorem CategoryTheory.Limits.Cone.w {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') :
CategoryTheory.CategoryStruct.comp (c.app j) (F.map f) = c.app j'
structure CategoryTheory.Limits.Cocone {J : Type u₁} [] {C : Type u₃} [] (F : ) :
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 .obj self.pt

A natural transformation from F to the constant functor at pt

Instances For
instance CategoryTheory.Limits.inhabitedCocone {C : Type u₃} [] (F : ) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Limits.Cocone.w_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') {Z : C} (h : (.obj c.pt).obj j' Z) :
theorem CategoryTheory.Limits.Cocone.w {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {j : J} {j' : J} (f : j j') :
CategoryTheory.CategoryStruct.comp (F.map f) (c.app j') = c.app j
@[simp]
theorem CategoryTheory.Limits.Cone.equiv_inv_π {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : (X : Cᵒᵖ) × F.cones.obj X) :
(.inv c) = c.snd
@[simp]
theorem CategoryTheory.Limits.Cone.equiv_inv_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : (X : Cᵒᵖ) × F.cones.obj X) :
(.inv c).pt = Opposite.unop c.fst
@[simp]
theorem CategoryTheory.Limits.Cone.equiv_hom_snd {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.hom c).snd = c
@[simp]
theorem CategoryTheory.Limits.Cone.equiv_hom_fst {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.hom c).fst = Opposite.op c.pt
def CategoryTheory.Limits.Cone.equiv {J : Type u₁} [] {C : Type u₃} [] (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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.extensions_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : Cᵒᵖ) (f : ((CategoryTheory.yoneda.obj c.pt).comp CategoryTheory.uliftFunctor.{u₁, v₃} ).obj X) :
c.extensions.app X f = CategoryTheory.CategoryStruct.comp (.map f.down) c
def CategoryTheory.Limits.Cone.extensions {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
(CategoryTheory.yoneda.obj c.pt).comp CategoryTheory.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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.extend_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {X : C} (f : X c.pt) :
(c.extend f) = c.extensions.app (Opposite.op X) { down := f }
@[simp]
theorem CategoryTheory.Limits.Cone.extend_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {X : C} (f : X c.pt) :
(c.extend f).pt = X
def CategoryTheory.Limits.Cone.extend {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {X : C} (f : X c.pt) :

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

Equations
• c.extend f = { pt := X, π := c.extensions.app (Opposite.op X) { down := f } }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.whisker_pt {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
.pt = c.pt
@[simp]
theorem CategoryTheory.Limits.Cone.whisker_π {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
def CategoryTheory.Limits.Cone.whisker {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :

Whisker a cone by precomposition of a functor.

Equations
• = { pt := c.pt, π := }
Instances For
def CategoryTheory.Limits.Cocone.equiv {J : Type u₁} [] {C : Type u₃} [] (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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.extensions_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : C) (f : ((CategoryTheory.coyoneda.obj (Opposite.op c.pt)).comp CategoryTheory.uliftFunctor.{u₁, v₃} ).obj X) :
c.extensions.app X f = CategoryTheory.CategoryStruct.comp c (.map f.down)
def CategoryTheory.Limits.Cocone.extensions {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
(CategoryTheory.coyoneda.obj (Opposite.op c.pt)).comp CategoryTheory.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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.extend_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {Y : C} (f : c.pt Y) :
(c.extend f) = c.extensions.app Y { down := f }
@[simp]
theorem CategoryTheory.Limits.Cocone.extend_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {Y : C} (f : c.pt Y) :
(c.extend f).pt = Y
def CategoryTheory.Limits.Cocone.extend {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) {Y : C} (f : c.pt Y) :

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

Equations
• c.extend f = { pt := Y, ι := c.extensions.app Y { down := f } }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.whisker_ι {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
@[simp]
theorem CategoryTheory.Limits.Cocone.whisker_pt {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
.pt = c.pt
def CategoryTheory.Limits.Cocone.whisker {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :

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

Equations
• = { pt := c.pt, ι := }
Instances For
structure CategoryTheory.Limits.ConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } (A : ) (B : ) :
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), CategoryTheory.CategoryStruct.comp self.hom (B.app j) = A.app j

The triangle consisting of the two natural transformations and hom commutes

Instances For
@[simp]
theorem CategoryTheory.Limits.ConeMorphism.w {J : Type u₁} [] {C : Type u₃} [] {F : } {A : } {B : } (self : ) (j : J) :
CategoryTheory.CategoryStruct.comp self.hom (B.app j) = A.app j

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.ConeMorphism.w_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {A : } {B : } (self : ) (j : J) {Z : C} (h : F.obj j Z) :
instance CategoryTheory.Limits.inhabitedConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } (A : ) :
Equations
• = { default := { hom := , w := } }
@[simp]
theorem CategoryTheory.Limits.Cone.category_id_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (B : ) :
@[simp]
theorem CategoryTheory.Limits.Cone.category_comp_hom {J : Type u₁} [] {C : Type u₃} [] {F : } :
∀ {X Y Z : } (f : X Y) (g : Y Z), .hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance CategoryTheory.Limits.Cone.category {J : Type u₁} [] {C : Type u₃} [] {F : } :

The category of cones on a given diagram.

Equations
• CategoryTheory.Limits.Cone.category =
theorem CategoryTheory.Limits.ConeMorphism.ext_iff {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } {f : c c'} {g : c c'} :
f = g f.hom = g.hom
theorem CategoryTheory.Limits.ConeMorphism.ext {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (f : c c') (g : c c') (w : f.hom = g.hom) :
f = g
@[simp]
theorem CategoryTheory.Limits.Cones.ext_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j)) _auto✝) :
.inv.hom = φ.inv
@[simp]
theorem CategoryTheory.Limits.Cones.ext_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j)) _auto✝) :
.hom.hom = φ.hom
def CategoryTheory.Limits.Cones.ext {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), c.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.app j)) _auto✝) :
c c'

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

Equations
• = { hom := { hom := φ.hom, w := }, inv := { hom := φ.inv, w := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.eta_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
.hom.hom =
@[simp]
theorem CategoryTheory.Limits.Cones.eta_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
.inv.hom =
def CategoryTheory.Limits.Cones.eta {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c { pt := c.pt, π := c }

Eta rule for cones.

Equations
Instances For
theorem CategoryTheory.Limits.Cones.cone_iso_of_hom_iso {J : Type u₁} [] {C : Type u₃} [] {K : } {c : } {d : } (f : c d) [i : CategoryTheory.IsIso f.hom] :

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

@[simp]
theorem CategoryTheory.Limits.Cones.extend_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : X s.pt) :
.hom = f
def CategoryTheory.Limits.Cones.extend {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : X s.pt) :
s.extend f s

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

Equations
• = { hom := f, w := }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.extendId_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
@[simp]
theorem CategoryTheory.Limits.Cones.extendId_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
def CategoryTheory.Limits.Cones.extendId {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
s.extend s

Extending a cone by the identity does nothing.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.extendComp_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : X Y) (g : Y s.pt) :
.inv.hom =
@[simp]
theorem CategoryTheory.Limits.Cones.extendComp_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : X Y) (g : Y s.pt) :
.hom.hom =
def CategoryTheory.Limits.Cones.extendComp {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : X Y) (g : Y s.pt) :
s.extend (s.extend g).extend f

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.extendIso_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : X s.pt) :
.inv.hom = f.inv
@[simp]
theorem CategoryTheory.Limits.Cones.extendIso_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : X s.pt) :
.hom.hom = f.hom
def CategoryTheory.Limits.Cones.extendIso {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : X s.pt) :
s.extend f.hom s

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

Equations
• = { hom := { hom := f.hom, w := }, inv := { hom := f.inv, w := }, hom_inv_id := , inv_hom_id := }
Instances For
instance CategoryTheory.Limits.Cones.instIsIsoConeExtend {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (f : X s.pt) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.Cones.postcompose_obj_π {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :
( c) =
@[simp]
theorem CategoryTheory.Limits.Cones.postcompose_map_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) :
∀ {X Y : } (f : X Y), ( f).hom = f.hom
@[simp]
theorem CategoryTheory.Limits.Cones.postcompose_obj_pt {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :
( c).pt = c.pt
def CategoryTheory.Limits.Cones.postcompose {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F 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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeComp_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {H : } (α : F G) (β : G H) (X : ) :
(.app X).hom =
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeComp_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {H : } (α : F G) (β : G H) (X : ) :
(.app X).hom =
def CategoryTheory.Limits.Cones.postcomposeComp {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {H : } (α : F G) (β : G H) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeId_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (X : ) :
(CategoryTheory.Limits.Cones.postcomposeId.inv.app X).hom =
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeId_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (X : ) :
(CategoryTheory.Limits.Cones.postcomposeId.hom.app X).hom =

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_inverse {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) :
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_unitIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) :
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_functor {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) :
@[simp]
theorem CategoryTheory.Limits.Cones.postcomposeEquivalence_counitIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (s : ) => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((.comp ).obj s).pt) )
def CategoryTheory.Limits.Cones.postcomposeEquivalence {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F 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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.whiskering_obj {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
@[simp]
theorem CategoryTheory.Limits.Cones.whiskering_map_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) :
∀ {X Y : } (f : X Y), ( f).hom = f.hom
def CategoryTheory.Limits.Cones.whiskering {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
@[simp]
theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
@[simp]
theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_functor {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
=
@[simp]
theorem CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
def CategoryTheory.Limits.Cones.whiskeringEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
CategoryTheory.Limits.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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :
.inverse = .comp ((CategoryTheory.Limits.Cones.whiskering e.inverse).comp (CategoryTheory.Limits.Cones.postcompose (e.invFunIdAssoc F).hom))
@[simp]
theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_functor {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :
.functor = (CategoryTheory.Limits.Cones.whiskering e.functor).comp
@[simp]
theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :
@[simp]
theorem CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :
def CategoryTheory.Limits.Cones.equivalenceOfReindexing {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.forget_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), f = f.hom
@[simp]
theorem CategoryTheory.Limits.Cones.forget_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (t : ) :
t = t.pt
def CategoryTheory.Limits.Cones.forget {J : Type u₁} [] {C : Type u₃} [] (F : ) :

Forget the cone structure and obtain just the cone point.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cones.functoriality_map_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) :
∀ {X Y : } (f : X Y), ( f).hom = G.map f.hom
@[simp]
theorem CategoryTheory.Limits.Cones.functoriality_obj_π_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (A : ) (j : J) :
( A).app j = G.map (A.app j)
@[simp]
theorem CategoryTheory.Limits.Cones.functoriality_obj_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (A : ) :
( A).pt = G.obj A.pt
def CategoryTheory.Limits.Cones.functoriality {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (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.
Instances For
instance CategoryTheory.Limits.Cones.functoriality_full {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) [G.Full] [G.Faithful] :
.Full
Equations
• =
instance CategoryTheory.Limits.Cones.functoriality_faithful {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) [G.Faithful] :
.Faithful
Equations
• =
@[simp]
theorem CategoryTheory.Limits.Cones.functorialityEquivalence_functor {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.functor =
@[simp]
theorem CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cone (F.comp e.functor)) => CategoryTheory.Limits.Cones.ext (e.counitIso.app c.pt) )
@[simp]
theorem CategoryTheory.Limits.Cones.functorialityEquivalence_inverse {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.inverse = (CategoryTheory.Limits.Cones.functoriality (F.comp e.functor) e.inverse).comp (CategoryTheory.Limits.Cones.postcomposeEquivalence (F.associator e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ F.rightUnitor)).functor
@[simp]
theorem CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (c : ) => CategoryTheory.Limits.Cones.ext (e.unitIso.app ( c).1) )
def CategoryTheory.Limits.Cones.functorialityEquivalence {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
CategoryTheory.Limits.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.
Instances For
instance CategoryTheory.Limits.Cones.reflects_cone_isomorphism {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) [F.ReflectsIsomorphisms] (K : ) :
.ReflectsIsomorphisms

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

Equations
• =
structure CategoryTheory.Limits.CoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } (A : ) (B : ) :
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), CategoryTheory.CategoryStruct.comp (A.app j) self.hom = B.app j

The triangle made from the two natural transformations and hom commutes

Instances For
@[simp]
theorem CategoryTheory.Limits.CoconeMorphism.w {J : Type u₁} [] {C : Type u₃} [] {F : } {A : } {B : } (self : ) (j : J) :
CategoryTheory.CategoryStruct.comp (A.app j) self.hom = B.app j

The triangle made from the two natural transformations and hom commutes

instance CategoryTheory.Limits.inhabitedCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } (A : ) :
Equations
• = { default := { hom := , w := } }
@[simp]
theorem CategoryTheory.Limits.CoconeMorphism.w_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {A : } {B : } (self : ) (j : J) {Z : C} (h : B.pt Z) :
@[simp]
theorem CategoryTheory.Limits.Cocone.category_id_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (B : ) :
@[simp]
theorem CategoryTheory.Limits.Cocone.category_comp_hom {J : Type u₁} [] {C : Type u₃} [] {F : } :
∀ {X Y Z : } (f : X Y) (g : Y Z), .hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance CategoryTheory.Limits.Cocone.category {J : Type u₁} [] {C : Type u₃} [] {F : } :
Equations
• CategoryTheory.Limits.Cocone.category =
theorem CategoryTheory.Limits.CoconeMorphism.ext_iff {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } {f : c c'} {g : c c'} :
f = g f.hom = g.hom
theorem CategoryTheory.Limits.CoconeMorphism.ext {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (f : c c') (g : c c') (w : f.hom = g.hom) :
f = g
@[simp]
theorem CategoryTheory.Limits.Cocones.ext_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j) _auto✝) :
.inv.hom = φ.inv
@[simp]
theorem CategoryTheory.Limits.Cocones.ext_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j) _auto✝) :
.hom.hom = φ.hom
def CategoryTheory.Limits.Cocones.ext {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } {c' : } (φ : c.pt c'.pt) (w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.app j) φ.hom = c'.app j) _auto✝) :
c c'

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

Equations
• = { hom := { hom := φ.hom, w := }, inv := { hom := φ.inv, w := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.eta_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
.hom =
@[simp]
theorem CategoryTheory.Limits.Cocones.eta_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
.hom =
def CategoryTheory.Limits.Cocones.eta {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c { pt := c.pt, ι := c }

Eta rule for cocones.

Equations
Instances For
theorem CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso {J : Type u₁} [] {C : Type u₃} [] {K : } {c : } {d : } (f : c d) [i : CategoryTheory.IsIso f.hom] :

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

@[simp]
theorem CategoryTheory.Limits.Cocones.extend_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : s.pt X) :
.hom = f
def CategoryTheory.Limits.Cocones.extend {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : s.pt X) :
s s.extend f

There is a morphism from a cocone to its extension.

Equations
• = { hom := f, w := }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.extendId_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
@[simp]
theorem CategoryTheory.Limits.Cocones.extendId_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
def CategoryTheory.Limits.Cocones.extendId {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) :
s s.extend

Extending a cocone by the identity does nothing.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.extendComp_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : s.pt X) (g : X Y) :
@[simp]
theorem CategoryTheory.Limits.Cocones.extendComp_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : s.pt X) (g : X Y) :
def CategoryTheory.Limits.Cocones.extendComp {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} {Y : C} (f : s.pt X) (g : X Y) :
s.extend (s.extend f).extend g

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.extendIso_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : s.pt X) :
.hom.hom = f.hom
@[simp]
theorem CategoryTheory.Limits.Cocones.extendIso_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : s.pt X) :
.inv.hom = f.inv
def CategoryTheory.Limits.Cocones.extendIso {J : Type u₁} [] {C : Type u₃} [] {F : } (s : ) {X : C} (f : s.pt X) :
s s.extend f.hom

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

Equations
• = { hom := { hom := f.hom, w := }, inv := { hom := f.inv, w := }, hom_inv_id := , inv_hom_id := }
Instances For
instance CategoryTheory.Limits.Cocones.instIsIsoCoconeExtend {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (f : s.pt X) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.Cocones.precompose_obj_pt {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) (c : ) :
( c).pt = c.pt
@[simp]
theorem CategoryTheory.Limits.Cocones.precompose_map_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :
∀ {X Y : } (f : X Y), ( f).hom = f.hom
@[simp]
theorem CategoryTheory.Limits.Cocones.precompose_obj_ι {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) (c : ) :
( c) =
def CategoryTheory.Limits.Cocones.precompose {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :

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.
Instances For
def CategoryTheory.Limits.Cocones.precomposeComp {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {H : } (α : F G) (β : G H) :

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.
Instances For

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_counitIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :
@[simp]
theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_unitIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :
@[simp]
theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_inverse {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :
@[simp]
theorem CategoryTheory.Limits.Cocones.precomposeEquivalence_functor {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :
def CategoryTheory.Limits.Cocones.precomposeEquivalence {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : G F) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.whiskering_map_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) :
∀ {X Y : } (f : X Y), ( f).hom = f.hom
@[simp]
theorem CategoryTheory.Limits.Cocones.whiskering_obj {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) (c : ) :
def CategoryTheory.Limits.Cocones.whiskering {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (E : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
@[simp]
theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_functor {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
@[simp]
theorem CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
def CategoryTheory.Limits.Cocones.whiskeringEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } (e : K J) :
CategoryTheory.Limits.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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.equivalenceOfReindexing_functor_obj {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) (X : ) :
.functor.obj X = .obj (CategoryTheory.Limits.Cocone.whisker e.functor X)
def CategoryTheory.Limits.Cocones.equivalenceOfReindexing {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {G : } (e : K J) (α : e.functor.comp F G) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.forget_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (t : ) :
t = t.pt
@[simp]
theorem CategoryTheory.Limits.Cocones.forget_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), f = f.hom
def CategoryTheory.Limits.Cocones.forget {J : Type u₁} [] {C : Type u₃} [] (F : ) :

Forget the cocone structure and obtain just the cocone point.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocones.functoriality_obj_ι_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (A : ) (j : J) :
( A).app j = G.map (A.app j)
@[simp]
theorem CategoryTheory.Limits.Cocones.functoriality_map_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) :
∀ {X Y : } (f : X Y), ( f).hom = G.map f.hom
@[simp]
theorem CategoryTheory.Limits.Cocones.functoriality_obj_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) (A : ) :
( A).pt = G.obj A.pt
def CategoryTheory.Limits.Cocones.functoriality {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (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.
Instances For
instance CategoryTheory.Limits.Cocones.functoriality_full {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) [G.Full] [G.Faithful] :
.Full
Equations
• =
instance CategoryTheory.Limits.Cocones.functoriality_faithful {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (G : ) [G.Faithful] :
.Faithful
Equations
• =
@[simp]
theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cocone (F.comp e.functor)) => CategoryTheory.Limits.Cocones.ext (e.counitIso.app c.pt) )
@[simp]
theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (c : ) => CategoryTheory.Limits.Cocones.ext (e.unitIso.app ( c).1) )
@[simp]
theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.inverse = (CategoryTheory.Limits.Cocones.functoriality (F.comp e.functor) e.inverse).comp (CategoryTheory.Limits.Cocones.precomposeEquivalence (F.associator e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ F.rightUnitor).symm).functor
@[simp]
theorem CategoryTheory.Limits.Cocones.functorialityEquivalence_functor {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
.functor =
def CategoryTheory.Limits.Cocones.functorialityEquivalence {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) (e : C D) :
CategoryTheory.Limits.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.
Instances For
instance CategoryTheory.Limits.Cocones.reflects_cocone_isomorphism {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) [F.ReflectsIsomorphisms] (K : ) :
.ReflectsIsomorphisms

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

Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapCone_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) :
(H.mapCone c).pt = H.obj c.pt
@[simp]
theorem CategoryTheory.Functor.mapCone_π_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) (j : J) :
(H.mapCone c).app j = H.map (c.app j)
def CategoryTheory.Functor.mapCone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) :

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

Equations
• H.mapCone c = c
Instances For
@[simp]
theorem CategoryTheory.Functor.mapCocone_ι_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) (j : J) :
(H.mapCocone c).app j = H.map (c.app j)
@[simp]
theorem CategoryTheory.Functor.mapCocone_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) :
(H.mapCocone c).pt = H.obj c.pt
def CategoryTheory.Functor.mapCocone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } (c : ) :

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

Equations
• H.mapCocone c = c
Instances For
def CategoryTheory.Functor.mapConeMorphism {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {c : } {c' : } (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 = f
Instances For
def CategoryTheory.Functor.mapCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {c : } {c' : } (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 = f
Instances For
noncomputable def CategoryTheory.Functor.mapConeInv {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) :

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

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

mapCone is the left inverse to mapConeInv.

Equations
Instances For
noncomputable def CategoryTheory.Functor.mapConeInvMapCone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } (H : ) [H.IsEquivalence] (c : ) :
H.mapConeInv (H.mapCone c) c

MapCone is the right inverse to mapConeInv.

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

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

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

mapCocone is the left inverse to mapCoconeInv.

Equations
Instances For
noncomputable def CategoryTheory.Functor.mapCoconeInvMapCocone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } (H : ) [H.IsEquivalence] (c : ) :
H.mapCoconeInv (H.mapCocone c) c

mapCocone is the right inverse to mapCoconeInv.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (X : ) :
( X).hom = α.inv.app X.pt
@[simp]
theorem CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (X : ) :
( X).hom = α.hom.app X.pt
def CategoryTheory.Functor.functorialityCompPostcompose {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.hom = α.hom.app c.pt
@[simp]
theorem CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.hom = α.inv.app c.pt
def CategoryTheory.Functor.postcomposeWhiskerLeftMapCone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.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
Instances For
@[simp]
theorem CategoryTheory.Functor.mapConePostcompose_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapConePostcompose.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapConePostcompose_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapConePostcompose.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapConePostcompose {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCone ( c) (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
Instances For
@[simp]
theorem CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapConePostcomposeEquivalenceFunctor.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapConePostcomposeEquivalenceFunctor.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCone (.obj c) .obj (H.mapCone c)

mapCone commutes with postcomposeEquivalence

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (X : ) :
( X).hom = α.hom.app X.pt
@[simp]
theorem CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (X : ) :
( X).hom = α.inv.app X.pt
def CategoryTheory.Functor.functorialityCompPrecompose {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.hom = α.hom.app c.pt
@[simp]
theorem CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.hom = α.inv.app c.pt
def CategoryTheory.Functor.precomposeWhiskerLeftMapCocone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {H : } {H' : } (α : H H') (c : ) :
.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
Instances For
@[simp]
theorem CategoryTheory.Functor.mapCoconePrecompose_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCoconePrecompose.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapCoconePrecompose_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCoconePrecompose.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapCoconePrecompose {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCocone ( c) (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
Instances For
@[simp]
theorem CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCoconePrecomposeEquivalenceFunctor.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCoconePrecomposeEquivalenceFunctor.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {G : } {α : F G} {c : } :
H.mapCocone (.obj c) .obj (H.mapCocone c)

mapCocone commutes with precomposeEquivalence

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapConeWhisker_hom_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapConeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapConeWhisker_inv_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapConeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapConeWhisker {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapCone CategoryTheory.Limits.Cone.whisker E (H.mapCone c)

mapCone commutes with whisker

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapCoconeWhisker_inv_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapCoconeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem CategoryTheory.Functor.mapCoconeWhisker_hom_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapCoconeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def CategoryTheory.Functor.mapCoconeWhisker {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] (H : ) {F : } {E : } {c : } :
H.mapCocone CategoryTheory.Limits.Cocone.whisker E (H.mapCocone c)

mapCocone commutes with whisker

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.op_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.op.pt = Opposite.op c.pt
@[simp]
theorem CategoryTheory.Limits.Cocone.op_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.op =
def CategoryTheory.Limits.Cocone.op {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

Change a Cocone F into a Cone F.op.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.op_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.op =
@[simp]
theorem CategoryTheory.Limits.Cone.op_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.op.pt = Opposite.op c.pt
def CategoryTheory.Limits.Cone.op {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

Change a Cone F into a Cocone F.op.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.unop_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.unop.pt = Opposite.unop c.pt
@[simp]
theorem CategoryTheory.Limits.Cocone.unop_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.unop =
def CategoryTheory.Limits.Cocone.unop {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

Change a Cocone F.op into a Cone F.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.unop_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.unop =
@[simp]
theorem CategoryTheory.Limits.Cone.unop_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.unop.pt = Opposite.unop c.pt
def CategoryTheory.Limits.Cone.unop {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

Change a Cone F.op into a Cocone F.

Equations
Instances For
def CategoryTheory.Limits.coconeEquivalenceOpConeOp {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_unitIso {J : Type u₁} [] {C : Type u₃} [] (F : ) :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (c : ) => )
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_map {J : Type u₁} [] {C : Type u₃} [] (F : ) {X : } {Y : } (f : X Y) :
.functor.map f = Quiver.Hom.op { hom := f.hom.op, w := }
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_map_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) {X : ᵒᵖ} {Y : ᵒᵖ} (f : X Y) :
(.inverse.map f).hom = f.unop.hom.unop
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ᵒᵖ) :
.inverse.obj c = .unop
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
.functor.obj c = Opposite.op c.op
@[simp]
theorem CategoryTheory.Limits.coconeEquivalenceOpConeOp_counitIso {J : Type u₁} [] {C : Type u₃} [] (F : ) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (c : ᵒᵖ) => Opposite.rec' (fun (X : ) => .op) c)
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeLeftOp_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.leftOp) :
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeLeftOp_π_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.leftOp) (X : J) :
.app X = (c.app (Opposite.op X)).op
def CategoryTheory.Limits.coneOfCoconeLeftOp {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.leftOp) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeLeftOpOfCone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coconeLeftOpOfCone_ι_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : Jᵒᵖ) :
.app X = (c.app ).unop
def CategoryTheory.Limits.coconeLeftOpOfCone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeOfConeLeftOp_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.leftOp) :
def CategoryTheory.Limits.coconeOfConeLeftOp {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.leftOp) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeOfConeLeftOp_ι_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.leftOp) (j : J) :
.app j = (c.app (Opposite.op j)).op
@[simp]
theorem CategoryTheory.Limits.coneLeftOpOfCocone_π_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : Jᵒᵖ) :
.app X = (c.app ).unop
@[simp]
theorem CategoryTheory.Limits.coneLeftOpOfCocone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coneLeftOpOfCocone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeRightOp_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.rightOp) :
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeRightOp_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.rightOp) :
def CategoryTheory.Limits.coneOfCoconeRightOp {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cocone F.rightOp) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeRightOpOfCone_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coconeRightOpOfCone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coconeRightOpOfCone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeOfConeRightOp_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.rightOp) :
@[simp]
theorem CategoryTheory.Limits.coconeOfConeRightOp_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.rightOp) :
def CategoryTheory.Limits.coconeOfConeRightOp {J : Type u₁} [] {C : Type u₃} [] {F : } (c : CategoryTheory.Limits.Cone F.rightOp) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coneRightOpOfCocone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coneRightOpOfCocone_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coneRightOpOfCocone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeUnop_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coneOfCoconeUnop_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coneOfCoconeUnop {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeUnopOfCone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coconeUnopOfCone_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coconeUnopOfCone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeOfConeUnop_ι {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coconeOfConeUnop_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coconeOfConeUnop {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coneUnopOfCocone_π {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
@[simp]
theorem CategoryTheory.Limits.coneUnopOfCocone_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
def CategoryTheory.Limits.coneUnopOfCocone {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapConeOp_hom_hom {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {F : } (G :