Cones and cocones #
We define Cone F, a cone over a functor F,
and F.cones : Cᵒᵖ ⥤ Type, the functor associating to X the cones over F with cone point X.
A cone c is defined by specifying its cone point c.pt and a natural transformation c.π
from the constant c.pt valued functor to F.
We provide c.w f : c.π.app j ≫ F.map f = c.π.app j' for any f : j ⟶ j'
as a wrapper for c.π.naturality f avoiding unneeded identity morphisms.
We define c.extend f, where c : cone F and f : Y ⟶ c.pt for some other Y,
which replaces the cone point by Y and inserts f into each of the components of the cone.
Similarly we have c.whisker F producing a Cone (E ⋙ F)
We define morphisms of cones, and the category of cones.
We define Cone.postcompose α : cone F ⥤ cone G for α a natural transformation F ⟶ G.
And, of course, we dualise all this to cocones as well.
For more results about the category of cones, see cone_category.lean.
@[simp]
theorem
CategoryTheory.Functor.cones_map_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J),
((CategoryTheory.Functor.cones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)
@[simp]
theorem
CategoryTheory.Functor.cones_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(X : Cᵒᵖ)
:
(CategoryTheory.Functor.cones F).obj X = ((CategoryTheory.Functor.const J).obj X.unop ⟶ F)
def
CategoryTheory.Functor.cones
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₃))
If F : J ⥤ C then F.cones is the functor assigning to an object X : C the
type of natural transformations from the constant functor with value X to F.
An object representing this functor is a limit of F.
Equations
- CategoryTheory.Functor.cones F = CategoryTheory.Functor.comp (CategoryTheory.Functor.const J).op (CategoryTheory.yoneda.obj F)
@[simp]
theorem
CategoryTheory.Functor.cocones_map_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
∀ {X Y : C} (f : X ⟶ Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F)).obj ((CategoryTheory.Functor.const J).obj X))
(X_1 : J), ((CategoryTheory.Functor.cocones F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f
@[simp]
theorem
CategoryTheory.Functor.cocones_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(X : C)
:
(CategoryTheory.Functor.cocones F).obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)
def
CategoryTheory.Functor.cocones
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
CategoryTheory.Functor C (Type (max u₁ v₃))
If F : J ⥤ C then F.cocones is the functor assigning to an object (X : C)
the type of natural transformations from F to the constant functor with value X.
An object corepresenting this functor is a colimit of F.
Equations
- CategoryTheory.Functor.cocones F = CategoryTheory.Functor.comp (CategoryTheory.Functor.const J) (CategoryTheory.coyoneda.obj (Opposite.op F))
@[simp]
theorem
CategoryTheory.cones_map_app_app
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
:
∀ {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y) (X_1 : Cᵒᵖ)
(a : (CategoryTheory.yoneda.obj X).obj ((CategoryTheory.Functor.const J).op.obj X_1)) (X_2 : J),
(((CategoryTheory.cones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (a.app X_2) (f.app X_2)
@[simp]
theorem
CategoryTheory.cones_obj_map_app
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J),
(((CategoryTheory.cones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)
@[simp]
theorem
CategoryTheory.cones_obj_obj
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(X : Cᵒᵖ)
:
((CategoryTheory.cones J C).obj F).obj X = ((CategoryTheory.Functor.const J).obj X.unop ⟶ F)
def
CategoryTheory.cones
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
:
CategoryTheory.Functor (CategoryTheory.Functor J C) (CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₃)))
Functorially associated to each functor J ⥤ C, we have the C-presheaf consisting of
cones with a given cone point.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.cocones_obj_map_app
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
(F : (CategoryTheory.Functor J C)ᵒᵖ)
:
∀ {X Y : C} (f : X ⟶ Y)
(a : (CategoryTheory.coyoneda.obj (Opposite.op F.unop)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J),
(((CategoryTheory.cocones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp (a.app X_1) f
@[simp]
theorem
CategoryTheory.cocones_obj_obj
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
(F : (CategoryTheory.Functor J C)ᵒᵖ)
(X : C)
:
((CategoryTheory.cocones J C).obj F).obj X = (F.unop ⟶ (CategoryTheory.Functor.const J).obj X)
@[simp]
theorem
CategoryTheory.cocones_map_app_app
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
:
∀ {X Y : (CategoryTheory.Functor J C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C)
(a : (CategoryTheory.coyoneda.obj X).obj ((CategoryTheory.Functor.const J).obj X_1)) (X_2 : J),
(((CategoryTheory.cocones J C).map f).app X_1 a).app X_2 = CategoryTheory.CategoryStruct.comp (f.unop.app X_2) (a.app X_2)
def
CategoryTheory.cocones
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
(C : Type u₃)
[CategoryTheory.Category.{v₃, u₃} C]
:
CategoryTheory.Functor (CategoryTheory.Functor J C)ᵒᵖ (CategoryTheory.Functor C (Type (max u₁ v₃)))
Contravariantly associated to each functor J ⥤ C, we have the C-copresheaf consisting of
cocones with a given cocone point.
Equations
- One or more equations did not get rendered due to their size.
structure
CategoryTheory.Limits.Cone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
Type (max (max u₁ u₃) v₃)
A c : Cone F is:
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 - π : (CategoryTheory.Functor.const J).obj self.pt ⟶ F
A natural transformation from the constant functor at
XtoF
instance
CategoryTheory.Limits.inhabitedCone
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1} ) C)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cone.w_assoc
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{j : J}
{j' : J}
(f : j ⟶ j')
{Z : C}
(h : F.obj j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (c.π.app j) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (c.π.app j') h
@[simp]
theorem
CategoryTheory.Limits.Cone.w
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{j : J}
{j' : J}
(f : j ⟶ j')
:
CategoryTheory.CategoryStruct.comp (c.π.app j) (F.map f) = c.π.app j'
structure
CategoryTheory.Limits.Cocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
Type (max (max u₁ u₃) v₃)
A c : Cocone F is
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 ⟶ (CategoryTheory.Functor.const J).obj self.pt
A natural transformation from
Fto the constant functor atpt
instance
CategoryTheory.Limits.inhabitedCocone
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1} ) C)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cocone.w_assoc
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{j : J}
{j' : J}
(f : j ⟶ j')
{Z : C}
(h : ((CategoryTheory.Functor.const J).obj c.pt).obj j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (c.ι.app j') h) = CategoryTheory.CategoryStruct.comp (c.ι.app j) h
theorem
CategoryTheory.Limits.Cocone.w
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{j : J}
{j' : J}
(f : j ⟶ j')
:
CategoryTheory.CategoryStruct.comp (F.map f) (c.ι.app j') = c.ι.app j
@[simp]
theorem
CategoryTheory.Limits.Cone.equiv_hom_snd
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cone.equiv F).hom c).snd = c.π
@[simp]
theorem
CategoryTheory.Limits.Cone.equiv_inv_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X)
:
((CategoryTheory.Limits.Cone.equiv F).inv c).π = c.snd
@[simp]
theorem
CategoryTheory.Limits.Cone.equiv_hom_fst
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cone.equiv F).hom c).fst = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.Cone.equiv_inv_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X)
:
((CategoryTheory.Limits.Cone.equiv F).inv c).pt = c.fst.unop
def
CategoryTheory.Limits.Cone.equiv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
CategoryTheory.Limits.Cone F ≅ (X : Cᵒᵖ) × (CategoryTheory.Functor.cones F).obj X
The isomorphism between a cone on F and an element of the functor F.cones.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cone.extensions_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
(X : Cᵒᵖ)
(f : (CategoryTheory.Functor.comp (CategoryTheory.yoneda.obj c.pt) CategoryTheory.uliftFunctor.{u₁, v₃} ).obj X)
:
(CategoryTheory.Limits.Cone.extensions c).app X f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down) c.π
def
CategoryTheory.Limits.Cone.extensions
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
CategoryTheory.Functor.comp (CategoryTheory.yoneda.obj c.pt) CategoryTheory.uliftFunctor.{u₁, v₃} ⟶ CategoryTheory.Functor.cones F
A map to the vertex of a cone naturally induces a cone by composition.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cone.extend_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ⟶ c.pt)
:
(CategoryTheory.Limits.Cone.extend c f).π = (CategoryTheory.Limits.Cone.extensions c).app (Opposite.op X) { down := f }
@[simp]
theorem
CategoryTheory.Limits.Cone.extend_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ⟶ c.pt)
:
(CategoryTheory.Limits.Cone.extend c f).pt = X
def
CategoryTheory.Limits.Cone.extend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ⟶ c.pt)
:
A map to the vertex of a cone induces a cone by composition.
Equations
- CategoryTheory.Limits.Cone.extend c f = { pt := X, π := (CategoryTheory.Limits.Cone.extensions c).app (Opposite.op X) { down := f } }
@[simp]
theorem
CategoryTheory.Limits.Cone.whisker_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cone.whisker E c).pt = c.pt
@[simp]
theorem
CategoryTheory.Limits.Cone.whisker_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cone.whisker E c).π = CategoryTheory.whiskerLeft E c.π
def
CategoryTheory.Limits.Cone.whisker
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cone F)
:
Whisker a cone by precomposition of a functor.
Equations
- CategoryTheory.Limits.Cone.whisker E c = { pt := c.pt, π := CategoryTheory.whiskerLeft E c.π }
def
CategoryTheory.Limits.Cocone.equiv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
CategoryTheory.Limits.Cocone F ≅ (X : C) × (CategoryTheory.Functor.cocones F).obj X
The isomorphism between a cocone on F and an element of the functor F.cocones.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cocone.extensions_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
(X : C)
(f : (CategoryTheory.Functor.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt)) CategoryTheory.uliftFunctor.{u₁, v₃} ).obj
X)
:
(CategoryTheory.Limits.Cocone.extensions c).app X f = CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f.down)
def
CategoryTheory.Limits.Cocone.extensions
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
CategoryTheory.Functor.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt)) CategoryTheory.uliftFunctor.{u₁, v₃} ⟶ CategoryTheory.Functor.cocones F
A map from the vertex of a cocone naturally induces a cocone by composition.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cocone.extend_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{Y : C}
(f : c.pt ⟶ Y)
:
(CategoryTheory.Limits.Cocone.extend c f).ι = (CategoryTheory.Limits.Cocone.extensions c).app Y { down := f }
@[simp]
theorem
CategoryTheory.Limits.Cocone.extend_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{Y : C}
(f : c.pt ⟶ Y)
:
(CategoryTheory.Limits.Cocone.extend c f).pt = Y
def
CategoryTheory.Limits.Cocone.extend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{Y : C}
(f : c.pt ⟶ Y)
:
A map from the vertex of a cocone induces a cocone by composition.
Equations
- CategoryTheory.Limits.Cocone.extend c f = { pt := Y, ι := (CategoryTheory.Limits.Cocone.extensions c).app Y { down := f } }
@[simp]
theorem
CategoryTheory.Limits.Cocone.whisker_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocone.whisker E c).pt = c.pt
@[simp]
theorem
CategoryTheory.Limits.Cocone.whisker_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocone.whisker E c).ι = CategoryTheory.whiskerLeft E c.ι
def
CategoryTheory.Limits.Cocone.whisker
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cocone F)
:
Whisker a cocone by precomposition of a functor. See whiskering for a functorial
version.
Equations
- CategoryTheory.Limits.Cocone.whisker E c = { pt := c.pt, ι := CategoryTheory.whiskerLeft E c.ι }
structure
CategoryTheory.Limits.ConeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(A : CategoryTheory.Limits.Cone F)
(B : CategoryTheory.Limits.Cone F)
:
Type v₃
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
homcommutes
Instances For
@[simp]
theorem
CategoryTheory.Limits.ConeMorphism.w_assoc
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{A : CategoryTheory.Limits.Cone F}
{B : CategoryTheory.Limits.Cone F}
(self : CategoryTheory.Limits.ConeMorphism A B)
(j : J)
{Z : C}
(h : F.obj j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π.app j) h) = CategoryTheory.CategoryStruct.comp (A.π.app j) h
instance
CategoryTheory.Limits.inhabitedConeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(A : CategoryTheory.Limits.Cone F)
:
Equations
- CategoryTheory.Limits.inhabitedConeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
@[simp]
theorem
CategoryTheory.Limits.Cone.category_id_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(B : CategoryTheory.Limits.Cone F)
:
@[simp]
theorem
CategoryTheory.Limits.Cone.category_comp_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
∀ {X Y Z : CategoryTheory.Limits.Cone F} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance
CategoryTheory.Limits.Cone.category
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
The category of cones on a given diagram.
Equations
- CategoryTheory.Limits.Cone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
CategoryTheory.Limits.ConeMorphism.ext
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone F}
{c' : CategoryTheory.Limits.Cone F}
(f : c ⟶ c')
(g : c ⟶ c')
(w : f.hom = g.hom)
:
f = g
@[simp]
theorem
CategoryTheory.Limits.Cones.ext_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone F}
{c' : CategoryTheory.Limits.Cone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝)
:
(CategoryTheory.Limits.Cones.ext φ w).hom.hom = φ.hom
@[simp]
theorem
CategoryTheory.Limits.Cones.ext_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone F}
{c' : CategoryTheory.Limits.Cone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝)
:
(CategoryTheory.Limits.Cones.ext φ w).inv.hom = φ.inv
def
CategoryTheory.Limits.Cones.ext
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone F}
{c' : CategoryTheory.Limits.Cone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j)) _auto✝)
:
c ≅ c'
To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.
Equations
- CategoryTheory.Limits.Cones.ext φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Cones.eta_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.eta c).hom.hom = CategoryTheory.CategoryStruct.id c.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.eta_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.eta c).inv.hom = CategoryTheory.CategoryStruct.id c.pt
def
CategoryTheory.Limits.Cones.eta
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
c ≅ { pt := c.pt, π := c.π }
Eta rule for cones.
Equations
theorem
CategoryTheory.Limits.Cones.cone_iso_of_hom_iso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{K : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone K}
{d : CategoryTheory.Limits.Cone K}
(f : c ⟶ d)
[i : CategoryTheory.IsIso f.hom]
:
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₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ⟶ s.pt)
:
(CategoryTheory.Limits.Cones.extend s f).hom = f
def
CategoryTheory.Limits.Cones.extend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ⟶ s.pt)
:
There is a morphism from an extended cone to the original cone.
Equations
- CategoryTheory.Limits.Cones.extend s f = { hom := f, w := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Cones.extendId_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.extendId s).inv.hom = CategoryTheory.CategoryStruct.id s.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.extendId_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.extendId s).hom.hom = CategoryTheory.CategoryStruct.id s.pt
def
CategoryTheory.Limits.Cones.extendId
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
:
Extending a cone by the identity does nothing.
@[simp]
theorem
CategoryTheory.Limits.Cones.extendComp_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : Y ⟶ s.pt)
:
(CategoryTheory.Limits.Cones.extendComp s f g).inv.hom = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Limits.Cones.extendComp_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : Y ⟶ s.pt)
:
(CategoryTheory.Limits.Cones.extendComp s f g).hom.hom = CategoryTheory.CategoryStruct.id X
def
CategoryTheory.Limits.Cones.extendComp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : Y ⟶ s.pt)
:
Extending a cone by a composition is the same as extending the cone twice.
@[simp]
theorem
CategoryTheory.Limits.Cones.extendIso_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ≅ s.pt)
:
(CategoryTheory.Limits.Cones.extendIso s f).hom.hom = f.hom
@[simp]
theorem
CategoryTheory.Limits.Cones.extendIso_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ≅ s.pt)
:
(CategoryTheory.Limits.Cones.extendIso s f).inv.hom = f.inv
def
CategoryTheory.Limits.Cones.extendIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cone F)
{X : C}
(f : X ≅ s.pt)
:
CategoryTheory.Limits.Cone.extend s f.hom ≅ s
A cone extended by an isomorphism is isomorphic to the original cone.
Equations
- CategoryTheory.Limits.Cones.extendIso s f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
instance
CategoryTheory.Limits.Cones.instIsIsoConeCategoryExtendExtend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{s : CategoryTheory.Limits.Cone F}
{X : C}
(f : X ⟶ s.pt)
[CategoryTheory.IsIso f]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.postcompose_obj_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
(c : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cones.postcompose α).obj c).π = CategoryTheory.CategoryStruct.comp c.π α
@[simp]
theorem
CategoryTheory.Limits.Cones.postcompose_obj_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
(c : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cones.postcompose α).obj c).pt = c.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.postcompose_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
:
∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.postcompose α).map f).hom = f.hom
def
CategoryTheory.Limits.Cones.postcompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
:
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.
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeComp_hom_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor J C}
(α : F ⟶ G)
(β : G ⟶ H)
(X : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cones.postcomposeComp α β).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeComp_inv_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor J C}
(α : F ⟶ G)
(β : G ⟶ H)
(X : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cones.postcomposeComp α β).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
def
CategoryTheory.Limits.Cones.postcomposeComp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor J C}
(α : F ⟶ G)
(β : G ⟶ H)
:
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.
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeId_hom_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(X : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.postcomposeId.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeId_inv_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(X : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.postcomposeId.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
def
CategoryTheory.Limits.Cones.postcomposeId
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
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.
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ≅ G)
:
(CategoryTheory.Limits.Cones.postcomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone F) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Limits.Cones.postcomposeEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ≅ G)
:
(CategoryTheory.Limits.Cones.postcomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone G) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl
((CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.postcompose α.inv)
(CategoryTheory.Limits.Cones.postcompose α.hom)).obj
s).pt)
⋯)
⋯
def
CategoryTheory.Limits.Cones.postcomposeEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ≅ G)
:
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.
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskering_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cone F)
:
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskering_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
:
∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cones.whiskering E).map f).hom = f.hom
def
CategoryTheory.Limits.Cones.whiskering
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
:
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.
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cones.whiskeringEquivalence e).unitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone F) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskeringEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cones.whiskering e.functor
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cones.whiskeringEquivalence e).counitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp e.functor F)) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl
((CategoryTheory.Functor.comp
(CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse)
(CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom))
(CategoryTheory.Limits.Cones.whiskering e.functor)).obj
s).pt)
⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
def
CategoryTheory.Limits.Cones.whiskeringEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
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.Cones.equivalenceOfReindexing_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
@[simp]
theorem
CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).counitIso = CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.postcompose α.inv)
(CategoryTheory.isoWhiskerRight
(CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp e.functor F)) =>
CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯)
⋯)
(CategoryTheory.Limits.Cones.postcompose α.hom)) ≪≫ CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone G) => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).unitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯ ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Limits.Cones.whiskering e.functor)
(CategoryTheory.isoWhiskerRight
(CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp e.functor F)) =>
CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl s.pt) ⋯)
⋯)
(CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse)
(CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom)))
@[simp]
theorem
CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
(CategoryTheory.Limits.Cones.equivalenceOfReindexing e α).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.postcompose α.inv)
(CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.whiskering e.inverse)
(CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Equivalence.invFunIdAssoc e F).hom))
def
CategoryTheory.Limits.Cones.equivalenceOfReindexing
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
The categories of cones over F and G are equivalent if F and G are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
@[simp]
theorem
CategoryTheory.Limits.Cones.forget_map
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cones.forget F).map f = f.hom
@[simp]
theorem
CategoryTheory.Limits.Cones.forget_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.forget F).obj t = t.pt
def
CategoryTheory.Limits.Cones.forget
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
Forget the cone structure and obtain just the cone point.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cones.functoriality_obj_π_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
(A : CategoryTheory.Limits.Cone F)
(j : J)
:
((CategoryTheory.Limits.Cones.functoriality F G).obj A).π.app j = G.map (A.π.app j)
@[simp]
theorem
CategoryTheory.Limits.Cones.functoriality_obj_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
(A : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Limits.Cones.functoriality F G).obj A).pt = G.obj A.pt
@[simp]
theorem
CategoryTheory.Limits.Cones.functoriality_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
:
∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
((CategoryTheory.Limits.Cones.functoriality F G).map f).hom = G.map f.hom
def
CategoryTheory.Limits.Cones.functoriality
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
:
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.
instance
CategoryTheory.Limits.Cones.functorialityFull
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Full G]
[CategoryTheory.Faithful G]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.Cones.functoriality_faithful
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Faithful G]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.functorialityEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cones.functorialityEquivalence F e).inverse = CategoryTheory.Functor.comp
(CategoryTheory.Limits.Cones.functoriality (CategoryTheory.Functor.comp F e.functor) e.inverse)
(CategoryTheory.Limits.Cones.postcomposeEquivalence
(CategoryTheory.Functor.associator F e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ CategoryTheory.Functor.rightUnitor F)).functor
@[simp]
theorem
CategoryTheory.Limits.Cones.functorialityEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cones.functoriality F e.functor
@[simp]
theorem
CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cone F) =>
CategoryTheory.Limits.Cones.ext
(e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj c).1) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F e.functor)) =>
CategoryTheory.Limits.Cones.ext (e.counitIso.app c.pt) ⋯)
⋯
def
CategoryTheory.Limits.Cones.functorialityEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
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.
instance
CategoryTheory.Limits.Cones.reflects_cone_isomorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.ReflectsIsomorphisms F]
(K : CategoryTheory.Functor J C)
:
If F reflects isomorphisms, then Cones.functoriality F reflects isomorphisms
as well.
Equations
- ⋯ = ⋯
structure
CategoryTheory.Limits.CoconeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(A : CategoryTheory.Limits.Cocone F)
(B : CategoryTheory.Limits.Cocone F)
:
Type v₃
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
homcommutes
Instances For
instance
CategoryTheory.Limits.inhabitedCoconeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(A : CategoryTheory.Limits.Cocone F)
:
Equations
- CategoryTheory.Limits.inhabitedCoconeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
@[simp]
theorem
CategoryTheory.Limits.CoconeMorphism.w_assoc
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{A : CategoryTheory.Limits.Cocone F}
{B : CategoryTheory.Limits.Cocone F}
(self : CategoryTheory.Limits.CoconeMorphism A B)
(j : J)
{Z : C}
(h : B.pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (A.ι.app j) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (B.ι.app j) h
@[simp]
theorem
CategoryTheory.Limits.Cocone.category_id_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(B : CategoryTheory.Limits.Cocone F)
:
@[simp]
theorem
CategoryTheory.Limits.Cocone.category_comp_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
∀ {X Y Z : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance
CategoryTheory.Limits.Cocone.category
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
Equations
- CategoryTheory.Limits.Cocone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
CategoryTheory.Limits.CoconeMorphism.ext
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(f : c ⟶ c')
(g : c ⟶ c')
(w : f.hom = g.hom)
:
f = g
@[simp]
theorem
CategoryTheory.Limits.Cocones.ext_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝)
:
(CategoryTheory.Limits.Cocones.ext φ w).hom.hom = φ.hom
@[simp]
theorem
CategoryTheory.Limits.Cocones.ext_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝)
:
(CategoryTheory.Limits.Cocones.ext φ w).inv.hom = φ.inv
def
CategoryTheory.Limits.Cocones.ext
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(φ : c.pt ≅ c'.pt)
(w : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j) _auto✝)
:
c ≅ c'
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Equations
- CategoryTheory.Limits.Cocones.ext φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Cocones.eta_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.eta c).hom.hom = CategoryTheory.CategoryStruct.id c.pt
@[simp]
theorem
CategoryTheory.Limits.Cocones.eta_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.eta c).inv.hom = CategoryTheory.CategoryStruct.id c.pt
def
CategoryTheory.Limits.Cocones.eta
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
c ≅ { pt := c.pt, ι := c.ι }
Eta rule for cocones.
Equations
theorem
CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{K : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone K}
{d : CategoryTheory.Limits.Cocone K}
(f : c ⟶ d)
[i : CategoryTheory.IsIso f.hom]
:
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₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
(f : s.pt ⟶ X)
:
(CategoryTheory.Limits.Cocones.extend s f).hom = f
def
CategoryTheory.Limits.Cocones.extend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
(f : s.pt ⟶ X)
:
There is a morphism from a cocone to its extension.
Equations
- CategoryTheory.Limits.Cocones.extend s f = { hom := f, w := ⋯ }
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendId_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.extendId s).hom.hom = CategoryTheory.CategoryStruct.id s.pt
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendId_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.extendId s).inv.hom = CategoryTheory.CategoryStruct.id s.pt
def
CategoryTheory.Limits.Cocones.extendId
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
:
Extending a cocone by the identity does nothing.
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendComp_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
{Y : C}
(f : s.pt ⟶ X)
(g : X ⟶ Y)
:
(CategoryTheory.Limits.Cocones.extendComp s f g).inv.hom = CategoryTheory.CategoryStruct.id Y
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendComp_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
{Y : C}
(f : s.pt ⟶ X)
(g : X ⟶ Y)
:
(CategoryTheory.Limits.Cocones.extendComp s f g).hom.hom = CategoryTheory.CategoryStruct.id Y
def
CategoryTheory.Limits.Cocones.extendComp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
{Y : C}
(f : s.pt ⟶ X)
(g : X ⟶ Y)
:
Extending a cocone by a composition is the same as extending the cone twice.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendIso_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
(f : s.pt ≅ X)
:
(CategoryTheory.Limits.Cocones.extendIso s f).inv.hom = f.inv
@[simp]
theorem
CategoryTheory.Limits.Cocones.extendIso_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
(f : s.pt ≅ X)
:
(CategoryTheory.Limits.Cocones.extendIso s f).hom.hom = f.hom
def
CategoryTheory.Limits.Cocones.extendIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(s : CategoryTheory.Limits.Cocone F)
{X : C}
(f : s.pt ≅ X)
:
s ≅ CategoryTheory.Limits.Cocone.extend s f.hom
A cocone extended by an isomorphism is isomorphic to the original cone.
Equations
- CategoryTheory.Limits.Cocones.extendIso s f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
instance
CategoryTheory.Limits.Cocones.instIsIsoCoconeCategoryExtendExtend
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{s : CategoryTheory.Limits.Cocone F}
{X : C}
(f : s.pt ⟶ X)
[CategoryTheory.IsIso f]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.precompose_obj_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ⟶ F)
(c : CategoryTheory.Limits.Cocone F)
:
((CategoryTheory.Limits.Cocones.precompose α).obj c).ι = CategoryTheory.CategoryStruct.comp α c.ι
@[simp]
theorem
CategoryTheory.Limits.Cocones.precompose_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ⟶ F)
:
∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.precompose α).map f).hom = f.hom
@[simp]
theorem
CategoryTheory.Limits.Cocones.precompose_obj_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ⟶ F)
(c : CategoryTheory.Limits.Cocone F)
:
((CategoryTheory.Limits.Cocones.precompose α).obj c).pt = c.pt
def
CategoryTheory.Limits.Cocones.precompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ⟶ F)
:
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.
def
CategoryTheory.Limits.Cocones.precomposeComp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor J C}
(α : F ⟶ G)
(β : G ⟶ H)
:
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.
def
CategoryTheory.Limits.Cocones.precomposeId
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
:
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.Cocones.precomposeEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ≅ F)
:
@[simp]
theorem
CategoryTheory.Limits.Cocones.precomposeEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ≅ F)
:
(CategoryTheory.Limits.Cocones.precomposeEquivalence α).unitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cocone F) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.precomposeEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ≅ F)
:
@[simp]
theorem
CategoryTheory.Limits.Cocones.precomposeEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ≅ F)
:
(CategoryTheory.Limits.Cocones.precomposeEquivalence α).counitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cocone G) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl
((CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.precompose α.inv)
(CategoryTheory.Limits.Cocones.precompose α.hom)).obj
s).pt)
⋯)
⋯
def
CategoryTheory.Limits.Cocones.precomposeEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : G ≅ F)
:
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.Cocones.whiskering_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
(c : CategoryTheory.Limits.Cocone F)
:
@[simp]
theorem
CategoryTheory.Limits.Cocones.whiskering_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
:
∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocones.whiskering E).map f).hom = f.hom
def
CategoryTheory.Limits.Cocones.whiskering
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(E : CategoryTheory.Functor K J)
:
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.Cocones.whiskeringEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cocones.whiskeringEquivalence e).inverse = CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.whiskering e.inverse)
(CategoryTheory.Limits.Cocones.precompose
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.counitIso.inv F)
(CategoryTheory.Functor.associator e.inverse e.functor F).inv)))
@[simp]
theorem
CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cocones.whiskeringEquivalence e).counitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp e.functor F)) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl
((CategoryTheory.Functor.comp
(CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.whiskering e.inverse)
(CategoryTheory.Limits.Cocones.precompose
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.counitIso.inv F)
(CategoryTheory.Functor.associator e.inverse e.functor F).inv))))
(CategoryTheory.Limits.Cocones.whiskering e.functor)).obj
s).pt)
⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.whiskeringEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cocones.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cocones.whiskering e.functor
@[simp]
theorem
CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
(CategoryTheory.Limits.Cocones.whiskeringEquivalence e).unitIso = CategoryTheory.NatIso.ofComponents
(fun (s : CategoryTheory.Limits.Cocone F) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
⋯
def
CategoryTheory.Limits.Cocones.whiskeringEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(e : K ≌ J)
:
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.Cocones.equivalenceOfReindexing_functor_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
(X : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.equivalenceOfReindexing e α).functor.obj X = (CategoryTheory.Limits.Cocones.precompose α.inv).obj (CategoryTheory.Limits.Cocone.whisker e.functor X)
def
CategoryTheory.Limits.Cocones.equivalenceOfReindexing
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor K C}
(e : K ≌ J)
(α : CategoryTheory.Functor.comp e.functor F ≅ G)
:
The categories of cocones over F and G are equivalent if F and G are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
@[simp]
theorem
CategoryTheory.Limits.Cocones.forget_map
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cocones.forget F).map f = f.hom
@[simp]
theorem
CategoryTheory.Limits.Cocones.forget_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(t : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.forget F).obj t = t.pt
def
CategoryTheory.Limits.Cocones.forget
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
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.Cocones.functoriality_obj_ι_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
(A : CategoryTheory.Limits.Cocone F)
(j : J)
:
((CategoryTheory.Limits.Cocones.functoriality F G).obj A).ι.app j = G.map (A.ι.app j)
@[simp]
theorem
CategoryTheory.Limits.Cocones.functoriality_obj_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
(A : CategoryTheory.Limits.Cocone F)
:
((CategoryTheory.Limits.Cocones.functoriality F G).obj A).pt = G.obj A.pt
@[simp]
theorem
CategoryTheory.Limits.Cocones.functoriality_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
:
∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y),
((CategoryTheory.Limits.Cocones.functoriality F G).map f).hom = G.map f.hom
def
CategoryTheory.Limits.Cocones.functoriality
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
:
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.
instance
CategoryTheory.Limits.Cocones.functorialityFull
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Full G]
[CategoryTheory.Faithful G]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.Cocones.functoriality_faithful
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Faithful G]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).counitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F e.functor)) =>
CategoryTheory.Limits.Cocones.ext (e.counitIso.app c.pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.functorialityEquivalence_functor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cocones.functoriality F e.functor
@[simp]
theorem
CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).unitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cocone F) =>
CategoryTheory.Limits.Cocones.ext
(e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).1) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
(CategoryTheory.Limits.Cocones.functorialityEquivalence F e).inverse = CategoryTheory.Functor.comp
(CategoryTheory.Limits.Cocones.functoriality (CategoryTheory.Functor.comp F e.functor) e.inverse)
(CategoryTheory.Limits.Cocones.precomposeEquivalence
(CategoryTheory.Functor.associator F e.functor e.inverse ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso.symm ≪≫ CategoryTheory.Functor.rightUnitor F).symm).functor
def
CategoryTheory.Limits.Cocones.functorialityEquivalence
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor J C)
(e : C ≌ D)
:
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.
instance
CategoryTheory.Limits.Cocones.reflects_cocone_isomorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.ReflectsIsomorphisms F]
(K : CategoryTheory.Functor J C)
:
If F reflects isomorphisms, then Cocones.functoriality F reflects isomorphisms
as well.
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.mapCone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
(H.mapCone c).pt = H.obj c.pt
@[simp]
theorem
CategoryTheory.Functor.mapCone_π_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
(j : J)
:
(H.mapCone c).π.app j = H.map (c.π.app j)
def
CategoryTheory.Functor.mapCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
The image of a cone in C under a functor G : C ⥤ D is a cone in D.
Equations
- H.mapCone c = (CategoryTheory.Limits.Cones.functoriality F H).obj c
@[simp]
theorem
CategoryTheory.Functor.mapCocone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
(H.mapCocone c).pt = H.obj c.pt
@[simp]
theorem
CategoryTheory.Functor.mapCocone_ι_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
(j : J)
:
(H.mapCocone c).ι.app j = H.map (c.ι.app j)
def
CategoryTheory.Functor.mapCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.
Equations
- H.mapCocone c = (CategoryTheory.Limits.Cocones.functoriality F H).obj c
def
CategoryTheory.Functor.mapConeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cone F}
{c' : CategoryTheory.Limits.Cone F}
(f : c ⟶ c')
:
H.mapCone c ⟶ H.mapCone c'
Given a cone morphism c ⟶ c', construct a cone morphism on the mapped cones functorially.
Equations
def
CategoryTheory.Functor.mapCoconeMorphism
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(f : c ⟶ c')
:
H.mapCocone c ⟶ H.mapCocone c'
Given a cocone morphism c ⟶ c', construct a cocone morphism on the mapped cocones
functorially.
Equations
def
CategoryTheory.Functor.mapConeInv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F H))
:
If H is an equivalence, we invert H.mapCone and get a cone for F from a cone
for F ⋙ H.
Equations
def
CategoryTheory.Functor.mapConeMapConeInv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J D}
(H : CategoryTheory.Functor D C)
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F H))
:
H.mapCone (CategoryTheory.Functor.mapConeInv H c) ≅ c
mapCone is the left inverse to mapConeInv.
Equations
def
CategoryTheory.Functor.mapConeInvMapCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J D}
(H : CategoryTheory.Functor D C)
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cone F)
:
CategoryTheory.Functor.mapConeInv H (H.mapCone c) ≅ c
MapCone is the right inverse to mapConeInv.
Equations
- CategoryTheory.Functor.mapConeInvMapCone H c = (CategoryTheory.Limits.Cones.functorialityEquivalence F (CategoryTheory.Functor.asEquivalence H)).unitIso.symm.app c
def
CategoryTheory.Functor.mapCoconeInv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F H))
:
If H is an equivalence, we invert H.mapCone and get a cone for F from a cone
for F ⋙ H.
Equations
def
CategoryTheory.Functor.mapCoconeMapCoconeInv
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J D}
(H : CategoryTheory.Functor D C)
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F H))
:
H.mapCocone (CategoryTheory.Functor.mapCoconeInv H c) ≅ c
mapCocone is the left inverse to mapCoconeInv.
Equations
def
CategoryTheory.Functor.mapCoconeInvMapCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J D}
(H : CategoryTheory.Functor D C)
[CategoryTheory.IsEquivalence H]
(c : CategoryTheory.Limits.Cocone F)
:
CategoryTheory.Functor.mapCoconeInv H (H.mapCocone c) ≅ c
mapCocone is the right inverse to mapCoconeInv.
Equations
- CategoryTheory.Functor.mapCoconeInvMapCocone H c = (CategoryTheory.Limits.Cocones.functorialityEquivalence F (CategoryTheory.Functor.asEquivalence H)).unitIso.symm.app c
@[simp]
theorem
CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(X : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Functor.functorialityCompPostcompose α).hom.app X).hom = α.hom.app X.pt
@[simp]
theorem
CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(X : CategoryTheory.Limits.Cone F)
:
((CategoryTheory.Functor.functorialityCompPostcompose α).inv.app X).hom = α.inv.app X.pt
def
CategoryTheory.Functor.functorialityCompPostcompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
:
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.Cones.ext (α.app c.pt) ⋯) ⋯
@[simp]
theorem
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).hom.hom = α.hom.app c.pt
@[simp]
theorem
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).inv.hom = α.inv.app c.pt
def
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerLeft F α.hom)).obj (H.mapCone c) ≅ H'.mapCone c
For F : J ⥤ C, given a cone c : Cone F, and a natural isomorphism α : H ≅ H' for functors
H H' : C ⥤ D, the postcomposition of the cone H.mapCone using the isomorphism α is
isomorphic to the cone H'.mapCone.
@[simp]
theorem
CategoryTheory.Functor.mapConePostcompose_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConePostcompose H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapConePostcompose_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConePostcompose H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapConePostcompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cone F}
:
H.mapCone ((CategoryTheory.Limits.Cones.postcompose α).obj c) ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.whiskerRight α H)).obj (H.mapCone c)
mapCone commutes with postcompose. In particular, for F : J ⥤ C, given a cone c : Cone F, a
natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious ways of producing
a cone over G ⋙ H, and they are both isomorphic.
Equations
- CategoryTheory.Functor.mapConePostcompose H = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cones.postcompose α).obj c)).pt) ⋯
@[simp]
theorem
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cone F}
:
H.mapCone ((CategoryTheory.Limits.Cones.postcomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cones.postcomposeEquivalence (CategoryTheory.isoWhiskerRight α H)).functor.obj (H.mapCone c)
mapCone commutes with postcomposeEquivalence
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(X : CategoryTheory.Limits.Cocone F)
:
((CategoryTheory.Functor.functorialityCompPrecompose α).hom.app X).hom = α.hom.app X.pt
@[simp]
theorem
CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(X : CategoryTheory.Limits.Cocone F)
:
((CategoryTheory.Functor.functorialityCompPrecompose α).inv.app X).hom = α.inv.app X.pt
def
CategoryTheory.Functor.functorialityCompPrecompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
:
functoriality F _ ⋙ precompose (whiskerLeft F _) simplifies to functoriality F _.
Equations
- CategoryTheory.Functor.functorialityCompPrecompose α = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cocone F) => CategoryTheory.Limits.Cocones.ext (α.app c.pt) ⋯) ⋯
@[simp]
theorem
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).hom.hom = α.hom.app c.pt
@[simp]
theorem
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).inv.hom = α.inv.app c.pt
def
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor C D}
{H' : CategoryTheory.Functor C D}
(α : H ≅ H')
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerLeft F α.inv)).obj (H.mapCocone c) ≅ H'.mapCocone c
For F : J ⥤ C, given a cocone c : Cocone F, and a natural isomorphism α : H ≅ H' for functors
H H' : C ⥤ D, the precomposition of the cocone H.mapCocone using the isomorphism α is
isomorphic to the cocone H'.mapCocone.
@[simp]
theorem
CategoryTheory.Functor.mapCoconePrecompose_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cocone G}
:
(CategoryTheory.Functor.mapCoconePrecompose H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapCoconePrecompose_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cocone G}
:
(CategoryTheory.Functor.mapCoconePrecompose H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapCoconePrecompose
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
{c : CategoryTheory.Limits.Cocone G}
:
H.mapCocone ((CategoryTheory.Limits.Cocones.precompose α).obj c) ≅ (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.whiskerRight α H)).obj (H.mapCocone c)
map_cocone commutes with precompose. In particular, for F : J ⥤ C, given a cocone
c : Cocone F, a natural transformation α : F ⟶ G and a functor H : C ⥤ D, we have two obvious
ways of producing a cocone over G ⋙ H, and they are both isomorphic.
Equations
- CategoryTheory.Functor.mapCoconePrecompose H = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocones.precompose α).obj c)).pt) ⋯
@[simp]
theorem
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cocone G}
:
(CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cocone G}
:
(CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ≅ G}
{c : CategoryTheory.Limits.Cocone G}
:
H.mapCocone ((CategoryTheory.Limits.Cocones.precomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cocones.precomposeEquivalence (CategoryTheory.isoWhiskerRight α H)).functor.obj (H.mapCocone c)
mapCocone commutes with precomposeEquivalence
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.mapConeWhisker_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConeWhisker H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapConeWhisker_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cone F}
:
(CategoryTheory.Functor.mapConeWhisker H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapConeWhisker
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cone F}
:
H.mapCone (CategoryTheory.Limits.Cone.whisker E c) ≅ CategoryTheory.Limits.Cone.whisker E (H.mapCone c)
Equations
@[simp]
theorem
CategoryTheory.Functor.mapCoconeWhisker_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cocone F}
:
(CategoryTheory.Functor.mapCoconeWhisker H).inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
@[simp]
theorem
CategoryTheory.Functor.mapCoconeWhisker_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cocone F}
:
(CategoryTheory.Functor.mapCoconeWhisker H).hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
def
CategoryTheory.Functor.mapCoconeWhisker
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(H : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{E : CategoryTheory.Functor K J}
{c : CategoryTheory.Limits.Cocone F}
:
H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c) ≅ CategoryTheory.Limits.Cocone.whisker E (H.mapCocone c)
mapCocone commutes with whisker
Equations
- CategoryTheory.Functor.mapCoconeWhisker H = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c)).pt) ⋯
@[simp]
theorem
CategoryTheory.Limits.Cocone.op_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.Cocone.op c).pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.Cocone.op_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
def
CategoryTheory.Limits.Cocone.op
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
:
Change a Cocone F into a Cone F.op.
Equations
- CategoryTheory.Limits.Cocone.op c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.op c.ι }
@[simp]
theorem
CategoryTheory.Limits.Cone.op_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.Cone.op c).pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.Cone.op_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
def
CategoryTheory.Limits.Cone.op
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
:
Change a Cone F into a Cocone F.op.
Equations
- CategoryTheory.Limits.Cone.op c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.op c.π }
@[simp]
theorem
CategoryTheory.Limits.Cocone.unop_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F.op)
:
(CategoryTheory.Limits.Cocone.unop c).pt = c.pt.unop
@[simp]
theorem
CategoryTheory.Limits.Cocone.unop_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F.op)
:
def
CategoryTheory.Limits.Cocone.unop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F.op)
:
Change a Cocone F.op into a Cone F.
Equations
- CategoryTheory.Limits.Cocone.unop c = { pt := c.pt.unop, π := CategoryTheory.NatTrans.removeOp c.ι }
@[simp]
theorem
CategoryTheory.Limits.Cone.unop_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F.op)
:
@[simp]
theorem
CategoryTheory.Limits.Cone.unop_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F.op)
:
(CategoryTheory.Limits.Cone.unop c).pt = c.pt.unop
def
CategoryTheory.Limits.Cone.unop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F.op)
:
Change a Cone F.op into a Cocone F.
Equations
- CategoryTheory.Limits.Cone.unop c = { pt := c.pt.unop, ι := CategoryTheory.NatTrans.removeOp c.π }
def
CategoryTheory.Limits.coconeEquivalenceOpConeOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
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.
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_counitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
(CategoryTheory.Limits.coconeEquivalenceOpConeOp F).counitIso = CategoryTheory.NatIso.ofComponents
(fun (c : (CategoryTheory.Limits.Cone F.op)ᵒᵖ) =>
Opposite.rec'
(fun (X : CategoryTheory.Limits.Cone F.op) =>
CategoryTheory.Iso.op (CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl X.pt) ⋯))
c)
⋯
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.coconeEquivalenceOpConeOp F).functor.obj c = Opposite.op (CategoryTheory.Limits.Cocone.op c)
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_map_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
{X : (CategoryTheory.Limits.Cone F.op)ᵒᵖ}
{Y : (CategoryTheory.Limits.Cone F.op)ᵒᵖ}
(f : X ⟶ Y)
:
((CategoryTheory.Limits.coconeEquivalenceOpConeOp F).inverse.map f).hom = f.unop.hom.unop
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_unitIso
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
:
(CategoryTheory.Limits.coconeEquivalenceOpConeOp F).unitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cocone F) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_obj
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
(c : (CategoryTheory.Limits.Cone F.op)ᵒᵖ)
:
(CategoryTheory.Limits.coconeEquivalenceOpConeOp F).inverse.obj c = CategoryTheory.Limits.Cone.unop c.unop
@[simp]
theorem
CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_map
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor J C)
{X : CategoryTheory.Limits.Cocone F}
{Y : CategoryTheory.Limits.Cocone F}
(f : X ⟶ Y)
:
(CategoryTheory.Limits.coconeEquivalenceOpConeOp F).functor.map f = { hom := f.hom.op, w := ⋯ }.op
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeLeftOp_π_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F.leftOp)
(X : J)
:
(CategoryTheory.Limits.coneOfCoconeLeftOp c).π.app X = (c.ι.app (Opposite.op X)).op
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeLeftOp_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F.leftOp)
:
(CategoryTheory.Limits.coneOfCoconeLeftOp c).pt = Opposite.op c.pt
def
CategoryTheory.Limits.coneOfCoconeLeftOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F.leftOp)
:
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.ι }
@[simp]
theorem
CategoryTheory.Limits.coconeLeftOpOfCone_ι_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
(X : Jᵒᵖ)
:
(CategoryTheory.Limits.coconeLeftOpOfCone c).ι.app X = (c.π.app X.unop).unop
@[simp]
theorem
CategoryTheory.Limits.coconeLeftOpOfCone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.coconeLeftOpOfCone c).pt = c.pt.unop
def
CategoryTheory.Limits.coconeLeftOpOfCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
:
CategoryTheory.Limits.Cocone F.leftOp
Change a cone on F : J ⥤ Cᵒᵖ to a cocone on F.leftOp : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.coconeLeftOpOfCone c = { pt := c.pt.unop, ι := CategoryTheory.NatTrans.leftOp c.π }
@[simp]
theorem
CategoryTheory.Limits.coconeOfConeLeftOp_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F.leftOp)
:
(CategoryTheory.Limits.coconeOfConeLeftOp c).pt = Opposite.op c.pt
def
CategoryTheory.Limits.coconeOfConeLeftOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F.leftOp)
:
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.coconeOfConeLeftOp_ι_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F.leftOp)
(j : J)
:
(CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app j = (c.π.app (Opposite.op j)).op
@[simp]
theorem
CategoryTheory.Limits.coneLeftOpOfCocone_π_app
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
(X : Jᵒᵖ)
:
(CategoryTheory.Limits.coneLeftOpOfCocone c).π.app X = (c.ι.app X.unop).unop
@[simp]
theorem
CategoryTheory.Limits.coneLeftOpOfCocone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.coneLeftOpOfCocone c).pt = c.pt.unop
def
CategoryTheory.Limits.coneLeftOpOfCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
:
CategoryTheory.Limits.Cone F.leftOp
Change a cocone on F : J ⥤ Cᵒᵖ to a cone on F.leftOp : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.coneLeftOpOfCocone c = { pt := c.pt.unop, π := CategoryTheory.NatTrans.leftOp c.ι }
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeRightOp_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F.rightOp)
:
(CategoryTheory.Limits.coneOfCoconeRightOp c).pt = c.pt.unop
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeRightOp_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F.rightOp)
:
def
CategoryTheory.Limits.coneOfCoconeRightOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F.rightOp)
:
Change a cocone on F.rightOp : J ⥤ Cᵒᵖ to a cone on F : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.coneOfCoconeRightOp c = { pt := c.pt.unop, π := CategoryTheory.NatTrans.removeRightOp c.ι }
@[simp]
theorem
CategoryTheory.Limits.coconeRightOpOfCone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.coconeRightOpOfCone c).pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.coconeRightOpOfCone_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F)
:
def
CategoryTheory.Limits.coconeRightOpOfCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F)
:
CategoryTheory.Limits.Cocone F.rightOp
Change a cone on F : Jᵒᵖ ⥤ C to a cocone on F.rightOp : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.coconeRightOpOfCone c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.rightOp c.π }
@[simp]
theorem
CategoryTheory.Limits.coconeOfConeRightOp_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F.rightOp)
:
@[simp]
theorem
CategoryTheory.Limits.coconeOfConeRightOp_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F.rightOp)
:
(CategoryTheory.Limits.coconeOfConeRightOp c).pt = c.pt.unop
def
CategoryTheory.Limits.coconeOfConeRightOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cone F.rightOp)
:
Change a cone on F.rightOp : J ⥤ Cᵒᵖ to a cocone on F : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.coconeOfConeRightOp c = { pt := c.pt.unop, ι := CategoryTheory.NatTrans.removeRightOp c.π }
@[simp]
theorem
CategoryTheory.Limits.coneRightOpOfCocone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.coneRightOpOfCocone c).pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.coneRightOpOfCocone_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F)
:
def
CategoryTheory.Limits.coneRightOpOfCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ C}
(c : CategoryTheory.Limits.Cocone F)
:
CategoryTheory.Limits.Cone F.rightOp
Change a cocone on F : Jᵒᵖ ⥤ C to a cone on F.rightOp : J ⥤ Cᵒᵖ.
Equations
- CategoryTheory.Limits.coneRightOpOfCocone c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.rightOp c.ι }
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeUnop_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F))
:
(CategoryTheory.Limits.coneOfCoconeUnop c).pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.coneOfCoconeUnop_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F))
:
def
CategoryTheory.Limits.coneOfCoconeUnop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F))
:
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.ι }
@[simp]
theorem
CategoryTheory.Limits.coconeUnopOfCone_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
:
@[simp]
theorem
CategoryTheory.Limits.coconeUnopOfCone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.coconeUnopOfCone c).pt = c.pt.unop
def
CategoryTheory.Limits.coconeUnopOfCone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F)
:
Change a cone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cocone on F.unop : J ⥤ C.
Equations
- CategoryTheory.Limits.coconeUnopOfCone c = { pt := c.pt.unop, ι := CategoryTheory.NatTrans.unop c.π }
@[simp]
theorem
CategoryTheory.Limits.coconeOfConeUnop_ι
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F))
:
@[simp]
theorem
CategoryTheory.Limits.coconeOfConeUnop_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F))
:
(CategoryTheory.Limits.coconeOfConeUnop c).pt = Opposite.op c.pt
def
CategoryTheory.Limits.coconeOfConeUnop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F))
:
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.coneUnopOfCocone_π
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
:
@[simp]
theorem
CategoryTheory.Limits.coneUnopOfCocone_pt
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.coneUnopOfCocone c).pt = c.pt.unop
def
CategoryTheory.Limits.coneUnopOfCocone
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ}
(c : CategoryTheory.Limits.Cocone F)
:
Change a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cone on F.unop : J ⥤ C.
Equations
- CategoryTheory.Limits.coneUnopOfCocone c = { pt := c.pt.unop, π := CategoryTheory.NatTrans.unop c.ι }
@[simp]
theorem
CategoryTheory.Functor.mapConeOp_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Functor.mapConeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
@[simp]
theorem
CategoryTheory.Functor.mapConeOp_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
(t : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Functor.mapConeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
def
CategoryTheory.Functor.mapConeOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
(t : CategoryTheory.Limits.Cone F)
:
CategoryTheory.Limits.Cone.op (G.mapCone t) ≅ G.op.mapCocone (CategoryTheory.Limits.Cone.op t)
The opposite cocone of the image of a cone is the image of the opposite cocone.
Equations
- CategoryTheory.Functor.mapConeOp G t = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (CategoryTheory.Limits.Cone.op (G.mapCone t)).pt) ⋯
@[simp]
theorem
CategoryTheory.Functor.mapCoconeOp_hom_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
{t : CategoryTheory.Limits.Cocone F}
:
(CategoryTheory.Functor.mapCoconeOp G).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
@[simp]
theorem
CategoryTheory.Functor.mapCoconeOp_inv_hom
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
{t : CategoryTheory.Limits.Cocone F}
:
(CategoryTheory.Functor.mapCoconeOp G).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
def
CategoryTheory.Functor.mapCoconeOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{F : CategoryTheory.Functor J C}
(G : CategoryTheory.Functor C D)
{t : CategoryTheory.Limits.Cocone F}
:
CategoryTheory.Limits.Cocone.op (G.mapCocone t) ≅ G.op.mapCone (CategoryTheory.Limits.Cocone.op t)
The opposite cone of the image of a cocone is the image of the opposite cone.
Equations
- CategoryTheory.Functor.mapCoconeOp G = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (CategoryTheory.Limits.Cocone.op (G.mapCocone t)).pt) ⋯