Cones and cocones #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.X and a natural transformation c.π
from the constant c.X 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.X 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
category_theory.functor.cones_map_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(_x _x_1 : Cᵒᵖ)
(f : _x ⟶ _x_1)
(ᾰ : (category_theory.yoneda.obj F).obj ((category_theory.functor.const J).op.obj _x))
(X : J) :
def
category_theory.functor.cones
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
F.cones is the functor assigning to an object X the type of
natural transformations from the constant functor with value X to F.
An object representing this functor is a limit of F.
Equations
@[simp]
theorem
category_theory.functor.cones_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : Cᵒᵖ) :
F.cones.obj X = ((category_theory.functor.const J).obj (opposite.unop X) ⟶ F)
@[simp]
theorem
category_theory.functor.cocones_map_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(_x _x_1 : C)
(f : _x ⟶ _x_1)
(ᾰ : (category_theory.coyoneda.obj (opposite.op F)).obj ((category_theory.functor.const J).obj _x))
(X : J) :
def
category_theory.functor.cocones
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
F.cocones is the functor assigning to an object X the type of
natural transformations from F to the constant functor with value X.
An object corepresenting this functor is a colimit of F.
Equations
@[simp]
theorem
category_theory.functor.cocones_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : C) :
@[simp]
theorem
category_theory.cones_map
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C]
(F G : J ⥤ C)
(f : F ⟶ G) :
@[simp]
theorem
category_theory.cones_obj
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C]
(F : J ⥤ C) :
(category_theory.cones J C).obj F = F.cones
def
category_theory.cones
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C] :
Functorially associated to each functor J ⥤ C, we have the C-presheaf consisting of
cones with a given cone point.
Equations
- category_theory.cones J C = {obj := category_theory.functor.cones _inst_3, map := λ (F G : J ⥤ C) (f : F ⟶ G), category_theory.whisker_left (category_theory.functor.const J).op (category_theory.yoneda.map f), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.cocones_map
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C]
(F G : (J ⥤ C)ᵒᵖ)
(f : F ⟶ G) :
@[simp]
theorem
category_theory.cocones_obj
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C]
(F : (J ⥤ C)ᵒᵖ) :
(category_theory.cocones J C).obj F = (opposite.unop F).cocones
def
category_theory.cocones
(J : Type u₁)
[category_theory.category J]
(C : Type u₃)
[category_theory.category C] :
Contravariantly associated to each functor J ⥤ C, we have the C-copresheaf consisting of
cocones with a given cocone point.
Equations
- category_theory.cocones J C = {obj := λ (F : (J ⥤ C)ᵒᵖ), (opposite.unop F).cocones, map := λ (F G : (J ⥤ C)ᵒᵖ) (f : F ⟶ G), category_theory.whisker_left (category_theory.functor.const J) (category_theory.coyoneda.map f), map_id' := _, map_comp' := _}
structure
category_theory.limits.cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u₁ u₃ v₃)
- X : C
- π : (category_theory.functor.const J).obj self.X ⟶ F
A c : cone F is:
- an object
c.Xand - a natural transformation
c.π : c.X ⟶ Ffrom the constantc.Xfunctor toF.
cone F is equivalent, via cone.equiv below, to Σ X, F.cones.obj X.
Instances for category_theory.limits.cone
- category_theory.limits.cone.has_sizeof_inst
- category_theory.limits.inhabited_cone
- category_theory.limits.cone.category
@[protected, instance]
def
category_theory.limits.inhabited_cone
{C : Type u₃}
[category_theory.category C]
(F : category_theory.discrete punit ⥤ C) :
Equations
- category_theory.limits.inhabited_cone F = {default := {X := F.obj {as := punit.star}, π := {app := λ (_x : category_theory.discrete punit), category_theory.limits.inhabited_cone._match_1 F _x, naturality' := _}}}
- category_theory.limits.inhabited_cone._match_1 F {as := punit.star} = 𝟙 (((category_theory.functor.const (category_theory.discrete punit)).obj (F.obj {as := punit.star})).obj {as := punit.star})
@[simp]
theorem
category_theory.limits.cone.w
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{j j' : J}
(f : j ⟶ j') :
@[simp]
theorem
category_theory.limits.cone.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{j j' : J}
(f : j ⟶ j')
{X' : C}
(f' : F.obj j' ⟶ X') :
structure
category_theory.limits.cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u₁ u₃ v₃)
- X : C
- ι : F ⟶ (category_theory.functor.const J).obj self.X
A c : cocone F is
- an object
c.Xand - a natural transformation
c.ι : F ⟶ c.XfromFto the constantc.Xfunctor.
cocone F is equivalent, via cone.equiv below, to Σ X, F.cocones.obj X.
Instances for category_theory.limits.cocone
- category_theory.limits.cocone.has_sizeof_inst
- category_theory.limits.inhabited_cocone
- category_theory.limits.cocone.category
@[protected, instance]
def
category_theory.limits.inhabited_cocone
{C : Type u₃}
[category_theory.category C]
(F : category_theory.discrete punit ⥤ C) :
Equations
- category_theory.limits.inhabited_cocone F = {default := {X := F.obj {as := punit.star}, ι := {app := λ (_x : category_theory.discrete punit), category_theory.limits.inhabited_cocone._match_1 F _x, naturality' := _}}}
- category_theory.limits.inhabited_cocone._match_1 F {as := punit.star} = 𝟙 (F.obj {as := punit.star})
@[simp]
theorem
category_theory.limits.cocone.w
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{j j' : J}
(f : j ⟶ j') :
@[simp]
theorem
category_theory.limits.cocone.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{j j' : J}
(f : j ⟶ j')
{X' : C}
(f' : ((category_theory.functor.const J).obj c.X).obj j' ⟶ X') :
@[simp]
theorem
category_theory.limits.cone.equiv_hom_snd
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cone F) :
((category_theory.limits.cone.equiv F).hom c).snd = c.π
@[simp]
theorem
category_theory.limits.cone.equiv_inv_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : Σ (X : Cᵒᵖ), F.cones.obj X) :
((category_theory.limits.cone.equiv F).inv c).X = opposite.unop c.fst
@[simp]
theorem
category_theory.limits.cone.equiv_hom_fst
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cone F) :
((category_theory.limits.cone.equiv F).hom c).fst = opposite.op c.X
def
category_theory.limits.cone.equiv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
The isomorphism between a cone on F and an element of the functor F.cones.
Equations
- category_theory.limits.cone.equiv F = {hom := λ (c : category_theory.limits.cone F), ⟨opposite.op c.X, c.π⟩, inv := λ (c : Σ (X : Cᵒᵖ), F.cones.obj X), {X := opposite.unop c.fst, π := c.snd}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.cone.equiv_inv_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : Σ (X : Cᵒᵖ), F.cones.obj X) :
((category_theory.limits.cone.equiv F).inv c).π = c.snd
@[simp]
theorem
category_theory.limits.cone.extensions_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
(X : Cᵒᵖ)
(f : (category_theory.yoneda.obj c.X ⋙ category_theory.ulift_functor).obj X) :
c.extensions.app X f = (category_theory.functor.const J).map f.down ≫ c.π
def
category_theory.limits.cone.extensions
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
A map to the vertex of a cone naturally induces a cone by composition.
Equations
- c.extensions = {app := λ (X : Cᵒᵖ) (f : (category_theory.yoneda.obj c.X ⋙ category_theory.ulift_functor).obj X), (category_theory.functor.const J).map f.down ≫ c.π, naturality' := _}
@[simp]
theorem
category_theory.limits.cone.extend_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{X : C}
(f : X ⟶ c.X) :
@[simp]
theorem
category_theory.limits.cone.extend_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{X : C}
(f : X ⟶ c.X) :
(c.extend f).π = c.extensions.app (opposite.op X) {down := f}
def
category_theory.limits.cone.extend
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{X : C}
(f : X ⟶ c.X) :
A map to the vertex of a cone induces a cone by composition.
Equations
- c.extend f = {X := X, π := c.extensions.app (opposite.op X) {down := f}}
@[simp]
theorem
category_theory.limits.cone.whisker_X
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
(category_theory.limits.cone.whisker E c).X = c.X
@[simp]
theorem
category_theory.limits.cone.whisker_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
def
category_theory.limits.cone.whisker
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
category_theory.limits.cone (E ⋙ F)
Whisker a cone by precomposition of a functor.
Equations
- category_theory.limits.cone.whisker E c = {X := c.X, π := category_theory.whisker_left E c.π}
def
category_theory.limits.cocone.equiv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
The isomorphism between a cocone on F and an element of the functor F.cocones.
Equations
- category_theory.limits.cocone.equiv F = {hom := λ (c : category_theory.limits.cocone F), ⟨c.X, c.ι⟩, inv := λ (c : Σ (X : C), F.cocones.obj X), {X := c.fst, ι := c.snd}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.cocone.extensions
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
A map from the vertex of a cocone naturally induces a cocone by composition.
Equations
- c.extensions = {app := λ (X : C) (f : (category_theory.coyoneda.obj (opposite.op c.X) ⋙ category_theory.ulift_functor).obj X), c.ι ≫ (category_theory.functor.const J).map f.down, naturality' := _}
@[simp]
theorem
category_theory.limits.cocone.extensions_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
(X : C)
(f : (category_theory.coyoneda.obj (opposite.op c.X) ⋙ category_theory.ulift_functor).obj X) :
c.extensions.app X f = c.ι ≫ (category_theory.functor.const J).map f.down
@[simp]
theorem
category_theory.limits.cocone.extend_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
@[simp]
theorem
category_theory.limits.cocone.extend_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
def
category_theory.limits.cocone.extend
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
A map from the vertex of a cocone induces a cocone by composition.
@[simp]
theorem
category_theory.limits.cocone.whisker_ι
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocone.whisker
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
Whisker a cocone by precomposition of a functor. See whiskering for a functorial
version.
Equations
- category_theory.limits.cocone.whisker E c = {X := c.X, ι := category_theory.whisker_left E c.ι}
@[simp]
theorem
category_theory.limits.cocone.whisker_X
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
(category_theory.limits.cocone.whisker E c).X = c.X
theorem
category_theory.limits.cone_morphism.ext
{J : Type u₁}
{_inst_1 : category_theory.category J}
{C : Type u₃}
{_inst_3 : category_theory.category C}
{F : J ⥤ C}
{A B : category_theory.limits.cone F}
(x y : category_theory.limits.cone_morphism A B)
(h : x.hom = y.hom) :
x = y
theorem
category_theory.limits.cone_morphism.ext_iff
{J : Type u₁}
{_inst_1 : category_theory.category J}
{C : Type u₃}
{_inst_3 : category_theory.category C}
{F : J ⥤ C}
{A B : category_theory.limits.cone F}
(x y : category_theory.limits.cone_morphism A B) :
@[ext]
structure
category_theory.limits.cone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(A B : category_theory.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.
Instances for category_theory.limits.cone_morphism
- category_theory.limits.cone_morphism.has_sizeof_inst
- category_theory.limits.inhabited_cone_morphism
@[simp]
theorem
category_theory.limits.cone_morphism.w
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{A B : category_theory.limits.cone F}
(self : category_theory.limits.cone_morphism A B)
(j : J) :
@[simp]
theorem
category_theory.limits.cone_morphism.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{A B : category_theory.limits.cone F}
(self : category_theory.limits.cone_morphism A B)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
@[protected, instance]
def
category_theory.limits.inhabited_cone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(A : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.category_comp_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(X Y Z : category_theory.limits.cone F)
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[protected, instance]
def
category_theory.limits.cone.category
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C} :
The category of cones on a given diagram.
Equations
- category_theory.limits.cone.category = {to_category_struct := {to_quiver := {hom := λ (A B : category_theory.limits.cone F), category_theory.limits.cone_morphism A B}, id := λ (B : category_theory.limits.cone F), {hom := 𝟙 B.X, w' := _}, comp := λ (X Y Z : category_theory.limits.cone F) (f : X ⟶ Y) (g : Y ⟶ Z), {hom := f.hom ≫ g.hom, w' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.limits.cone.category_id_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(B : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.ext_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.π.app j = φ.hom ≫ c'.π.app j) :
(category_theory.limits.cones.ext φ w).inv.hom = φ.inv
@[ext]
def
category_theory.limits.cones.ext
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.π.app j = φ.hom ≫ c'.π.app j) :
c ≅ c'
To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.
Equations
- category_theory.limits.cones.ext φ w = {hom := {hom := φ.hom, w' := _}, inv := {hom := φ.inv, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.cones.ext_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.π.app j = φ.hom ≫ c'.π.app j) :
(category_theory.limits.cones.ext φ w).hom.hom = φ.hom
@[simp]
theorem
category_theory.limits.cones.eta_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.eta_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
def
category_theory.limits.cones.eta
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
Eta rule for cones.
theorem
category_theory.limits.cones.cone_iso_of_hom_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{K : J ⥤ C}
{c d : category_theory.limits.cone K}
(f : c ⟶ d)
[i : category_theory.is_iso f.hom] :
Given a cone morphism whose object part is an isomorphism, produce an isomorphism of cones.
@[simp]
theorem
category_theory.limits.cones.postcompose_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ⟶ G)
(c : category_theory.limits.cone F) :
((category_theory.limits.cones.postcompose α).obj c).X = c.X
@[simp]
theorem
category_theory.limits.cones.postcompose_obj_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ⟶ G)
(c : category_theory.limits.cone F) :
def
category_theory.limits.cones.postcompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ⟶ G) :
Functorially postcompose a cone for F by a natural transformation F ⟶ G to give a cone for G.
@[simp]
theorem
category_theory.limits.cones.postcompose_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ⟶ G)
(c₁ c₂ : category_theory.limits.cone F)
(f : c₁ ⟶ c₂) :
((category_theory.limits.cones.postcompose α).map f).hom = f.hom
def
category_theory.limits.cones.postcompose_comp
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G H : J ⥤ C}
(α : F ⟶ G)
(β : G ⟶ H) :
Postcomposing a cone by the composite natural transformation α ≫ β is the same as
postcomposing by α and then by β.
Equations
@[simp]
theorem
category_theory.limits.cones.postcompose_comp_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G H : J ⥤ C}
(α : F ⟶ G)
(β : G ⟶ H)
(X : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.postcompose_comp_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G H : J ⥤ C}
(α : F ⟶ G)
(β : G ⟶ H)
(X : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.postcompose_id_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(X : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.postcompose_id_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(X : category_theory.limits.cone F) :
def
category_theory.limits.cones.postcompose_id
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C} :
Postcomposing by the identity does not change the cone up to isomorphism.
Equations
- category_theory.limits.cones.postcompose_id = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone F), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (𝟙 F)).obj s).X) _) category_theory.limits.cones.postcompose_id._proof_2
@[simp]
theorem
category_theory.limits.cones.postcompose_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.limits.cones.postcompose_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.limits.cones.postcompose_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
def
category_theory.limits.cones.postcompose_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
If F and G are naturally isomorphic functors, then they have equivalent categories of
cones.
Equations
- category_theory.limits.cones.postcompose_equivalence α = {functor := category_theory.limits.cones.postcompose α.hom, inverse := category_theory.limits.cones.postcompose α.inv, unit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone F), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone F)).obj s).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone G), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose α.inv ⋙ category_theory.limits.cones.postcompose α.hom).obj s).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cones.postcompose_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
(category_theory.limits.cones.postcompose_equivalence α).counit_iso = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone G), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose α.inv ⋙ category_theory.limits.cones.postcompose α.hom).obj s).X) _) _
@[simp]
theorem
category_theory.limits.cones.whiskering_map_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c c' : category_theory.limits.cone F)
(f : c ⟶ c') :
((category_theory.limits.cones.whiskering E).map f).hom = f.hom
def
category_theory.limits.cones.whiskering
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J) :
Whiskering on the left by E : K ⥤ J gives a functor from cone F to cone (E ⋙ F).
Equations
- category_theory.limits.cones.whiskering E = {obj := λ (c : category_theory.limits.cone F), category_theory.limits.cone.whisker E c, map := λ (c c' : category_theory.limits.cone F) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cones.whiskering_obj
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
(category_theory.limits.cones.whiskering_equivalence e).counit_iso = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone (e.functor ⋙ F)), category_theory.limits.cones.ext (category_theory.iso.refl (((category_theory.limits.cones.whiskering e.inverse ⋙ category_theory.limits.cones.postcompose (e.inv_fun_id_assoc F).hom) ⋙ category_theory.limits.cones.whiskering e.functor).obj s).X) _) _
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
def
category_theory.limits.cones.whiskering_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
Whiskering by an equivalence gives an equivalence between categories of cones.
Equations
- category_theory.limits.cones.whiskering_equivalence e = {functor := category_theory.limits.cones.whiskering e.functor, inverse := category_theory.limits.cones.whiskering e.inverse ⋙ category_theory.limits.cones.postcompose (e.inv_fun_id_assoc F).hom, unit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone F), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone F)).obj s).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone (e.functor ⋙ F)), category_theory.limits.cones.ext (category_theory.iso.refl (((category_theory.limits.cones.whiskering e.inverse ⋙ category_theory.limits.cones.postcompose (e.inv_fun_id_assoc F).hom) ⋙ category_theory.limits.cones.whiskering e.functor).obj s).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cones.equivalence_of_reindexing_functor
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
def
category_theory.limits.cones.equivalence_of_reindexing
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
The categories of cones over F and G are equivalent if F and G are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
@[simp]
theorem
category_theory.limits.cones.equivalence_of_reindexing_counit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
(category_theory.limits.cones.equivalence_of_reindexing e α).counit_iso = category_theory.iso_whisker_left (category_theory.limits.cones.postcompose α.inv) (category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone (e.functor ⋙ F)), category_theory.limits.cones.ext (category_theory.iso.refl s.X) _) _) (category_theory.limits.cones.postcompose α.hom)) ≪≫ category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone G), category_theory.limits.cones.ext (category_theory.iso.refl s.X) _) _
@[simp]
theorem
category_theory.limits.cones.equivalence_of_reindexing_unit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
(category_theory.limits.cones.equivalence_of_reindexing e α).unit_iso = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone F), category_theory.limits.cones.ext (category_theory.iso.refl s.X) _) _ ≪≫ category_theory.iso_whisker_left (category_theory.limits.cones.whiskering e.functor) (category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (s : category_theory.limits.cone (e.functor ⋙ F)), category_theory.limits.cones.ext (category_theory.iso.refl s.X) _) _) (category_theory.limits.cones.whiskering e.inverse ⋙ category_theory.limits.cones.postcompose (e.inv_fun_id_assoc F).hom))
@[simp]
theorem
category_theory.limits.cones.equivalence_of_reindexing_inverse
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
@[simp]
theorem
category_theory.limits.cones.forget_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(s t : category_theory.limits.cone F)
(f : s ⟶ t) :
(category_theory.limits.cones.forget F).map f = f.hom
@[simp]
theorem
category_theory.limits.cones.forget_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(t : category_theory.limits.cone F) :
(category_theory.limits.cones.forget F).obj t = t.X
def
category_theory.limits.cones.forget
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
Forget the cone structure and obtain just the cone point.
Equations
- category_theory.limits.cones.forget F = {obj := λ (t : category_theory.limits.cone F), t.X, map := λ (s t : category_theory.limits.cone F) (f : s ⟶ t), f.hom, map_id' := _, map_comp' := _}
def
category_theory.limits.cones.functoriality
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D) :
A functor G : C ⥤ D sends cones over F to cones over F ⋙ G functorially.
Equations
Instances for category_theory.limits.cones.functoriality
@[simp]
theorem
category_theory.limits.cones.functoriality_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(A : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.functoriality_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(X Y : category_theory.limits.cone F)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.limits.cones.functoriality_obj_π_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(A : category_theory.limits.cone F)
(j : J) :
@[protected, instance]
def
category_theory.limits.cones.functoriality_full
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.full G]
[category_theory.faithful G] :
Equations
- category_theory.limits.cones.functoriality_full F G = {preimage := λ (X Y : category_theory.limits.cone F) (t : (category_theory.limits.cones.functoriality F G).obj X ⟶ (category_theory.limits.cones.functoriality F G).obj Y), {hom := G.preimage t.hom, w' := _}, witness' := _}
@[protected, instance]
def
category_theory.limits.cones.functoriality_faithful
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.faithful G] :
@[simp]
theorem
category_theory.limits.cones.functoriality_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
(category_theory.limits.cones.functoriality_equivalence F e).inverse = category_theory.limits.cones.functoriality (F ⋙ e.functor) e.inverse ⋙ (category_theory.limits.cones.postcompose_equivalence (F.associator e.functor e.inverse ≪≫ category_theory.iso_whisker_left F e.unit_iso.symm ≪≫ F.right_unitor)).functor
@[simp]
theorem
category_theory.limits.cones.functoriality_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
def
category_theory.limits.cones.functoriality_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : 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
- category_theory.limits.cones.functoriality_equivalence F e = let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F := F.associator e.functor e.inverse ≪≫ category_theory.iso_whisker_left F e.unit_iso.symm ≪≫ F.right_unitor in {functor := category_theory.limits.cones.functoriality F e.functor, inverse := category_theory.limits.cones.functoriality (F ⋙ e.functor) e.inverse ⋙ (category_theory.limits.cones.postcompose_equivalence f).functor, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone F), category_theory.limits.cones.ext (e.unit_iso.app ((𝟭 (category_theory.limits.cone F)).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (F ⋙ e.functor)), category_theory.limits.cones.ext (e.counit_iso.app c.X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cones.functoriality_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
@[simp]
theorem
category_theory.limits.cones.functoriality_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
@[protected, instance]
def
category_theory.limits.cones.reflects_cone_isomorphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.reflects_isomorphisms F]
(K : J ⥤ C) :
If F reflects isomorphisms, then cones.functoriality F reflects isomorphisms
as well.
theorem
category_theory.limits.cocone_morphism.ext_iff
{J : Type u₁}
{_inst_1 : category_theory.category J}
{C : Type u₃}
{_inst_3 : category_theory.category C}
{F : J ⥤ C}
{A B : category_theory.limits.cocone F}
(x y : category_theory.limits.cocone_morphism A B) :
@[ext]
structure
category_theory.limits.cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(A B : category_theory.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.
Instances for category_theory.limits.cocone_morphism
- category_theory.limits.cocone_morphism.has_sizeof_inst
- category_theory.limits.inhabited_cocone_morphism
theorem
category_theory.limits.cocone_morphism.ext
{J : Type u₁}
{_inst_1 : category_theory.category J}
{C : Type u₃}
{_inst_3 : category_theory.category C}
{F : J ⥤ C}
{A B : category_theory.limits.cocone F}
(x y : category_theory.limits.cocone_morphism A B)
(h : x.hom = y.hom) :
x = y
@[protected, instance]
def
category_theory.limits.inhabited_cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(A : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone_morphism.w
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{A B : category_theory.limits.cocone F}
(self : category_theory.limits.cocone_morphism A B)
(j : J) :
@[simp]
theorem
category_theory.limits.cocone_morphism.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{A B : category_theory.limits.cocone F}
(self : category_theory.limits.cocone_morphism A B)
(j : J)
{X' : C}
(f' : B.X ⟶ X') :
@[simp]
theorem
category_theory.limits.cocone.category_comp_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(_x _x_1 _x_2 : category_theory.limits.cocone F)
(f : _x ⟶ _x_1)
(g : _x_1 ⟶ _x_2) :
@[protected, instance]
def
category_theory.limits.cocone.category
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C} :
Equations
- category_theory.limits.cocone.category = {to_category_struct := {to_quiver := {hom := λ (A B : category_theory.limits.cocone F), category_theory.limits.cocone_morphism A B}, id := λ (B : category_theory.limits.cocone F), {hom := 𝟙 B.X, w' := _}, comp := λ (_x _x_1 _x_2 : category_theory.limits.cocone F) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), {hom := f.hom ≫ g.hom, w' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.limits.cocone.category_id_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(B : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocones.ext_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cocone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.ι.app j ≫ φ.hom = c'.ι.app j) :
(category_theory.limits.cocones.ext φ w).inv.hom = φ.inv
@[ext]
def
category_theory.limits.cocones.ext
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cocone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.ι.app j ≫ φ.hom = c'.ι.app j) :
c ≅ c'
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Equations
- category_theory.limits.cocones.ext φ w = {hom := {hom := φ.hom, w' := w}, inv := {hom := φ.inv, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.cocones.ext_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c c' : category_theory.limits.cocone F}
(φ : c.X ≅ c'.X)
(w : ∀ (j : J), c.ι.app j ≫ φ.hom = c'.ι.app j) :
(category_theory.limits.cocones.ext φ w).hom.hom = φ.hom
@[simp]
theorem
category_theory.limits.cocones.eta_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocones.eta
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
Eta rule for cocones.
@[simp]
theorem
category_theory.limits.cocones.eta_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
theorem
category_theory.limits.cocones.cocone_iso_of_hom_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{K : J ⥤ C}
{c d : category_theory.limits.cocone K}
(f : c ⟶ d)
[i : category_theory.is_iso f.hom] :
Given a cocone morphism whose object part is an isomorphism, produce an isomorphism of cocones.
def
category_theory.limits.cocones.precompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ⟶ F) :
Functorially precompose a cocone for F by a natural transformation G ⟶ F to give a cocone
for G.
@[simp]
theorem
category_theory.limits.cocones.precompose_obj_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ⟶ F)
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocones.precompose_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ⟶ F)
(c₁ c₂ : category_theory.limits.cocone F)
(f : c₁ ⟶ c₂) :
((category_theory.limits.cocones.precompose α).map f).hom = f.hom
@[simp]
theorem
category_theory.limits.cocones.precompose_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ⟶ F)
(c : category_theory.limits.cocone F) :
((category_theory.limits.cocones.precompose α).obj c).X = c.X
def
category_theory.limits.cocones.precompose_comp
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G H : J ⥤ C}
(α : F ⟶ G)
(β : G ⟶ H) :
Precomposing a cocone by the composite natural transformation α ≫ β is the same as
precomposing by β and then by α.
def
category_theory.limits.cocones.precompose_id
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C} :
Precomposing by the identity does not change the cocone up to isomorphism.
Equations
- category_theory.limits.cocones.precompose_id = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone F), category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (𝟙 F)).obj s).X) _) category_theory.limits.cocones.precompose_id._proof_2
@[simp]
theorem
category_theory.limits.cocones.precompose_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
@[simp]
theorem
category_theory.limits.cocones.precompose_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
def
category_theory.limits.cocones.precompose_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
If F and G are naturally isomorphic functors, then they have equivalent categories of
cocones.
Equations
- category_theory.limits.cocones.precompose_equivalence α = {functor := category_theory.limits.cocones.precompose α.hom, inverse := category_theory.limits.cocones.precompose α.inv, unit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone F), category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cocone F)).obj s).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone G), category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose α.inv ⋙ category_theory.limits.cocones.precompose α.hom).obj s).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cocones.precompose_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
(category_theory.limits.cocones.precompose_equivalence α).counit_iso = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone G), category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose α.inv ⋙ category_theory.limits.cocones.precompose α.hom).obj s).X) _) _
@[simp]
theorem
category_theory.limits.cocones.precompose_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
def
category_theory.limits.cocones.whiskering
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J) :
Whiskering on the left by E : K ⥤ J gives a functor from cocone F to cocone (E ⋙ F).
Equations
- category_theory.limits.cocones.whiskering E = {obj := λ (c : category_theory.limits.cocone F), category_theory.limits.cocone.whisker E c, map := λ (c c' : category_theory.limits.cocone F) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cocones.whiskering_map_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c c' : category_theory.limits.cocone F)
(f : c ⟶ c') :
((category_theory.limits.cocones.whiskering E).map f).hom = f.hom
@[simp]
theorem
category_theory.limits.cocones.whiskering_obj
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocones.whiskering_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
Whiskering by an equivalence gives an equivalence between categories of cones.
Equations
- category_theory.limits.cocones.whiskering_equivalence e = {functor := category_theory.limits.cocones.whiskering e.functor, inverse := category_theory.limits.cocones.whiskering e.inverse ⋙ category_theory.limits.cocones.precompose (F.left_unitor.inv ≫ category_theory.whisker_right e.counit_iso.inv F ≫ (e.inverse.associator e.functor F).inv), unit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone F), category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cocone F)).obj s).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone (e.functor ⋙ F)), category_theory.limits.cocones.ext (category_theory.iso.refl (((category_theory.limits.cocones.whiskering e.inverse ⋙ category_theory.limits.cocones.precompose (F.left_unitor.inv ≫ category_theory.whisker_right e.counit_iso.inv F ≫ (e.inverse.associator e.functor F).inv)) ⋙ category_theory.limits.cocones.whiskering e.functor).obj s).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J) :
(category_theory.limits.cocones.whiskering_equivalence e).counit_iso = category_theory.nat_iso.of_components (λ (s : category_theory.limits.cocone (e.functor ⋙ F)), category_theory.limits.cocones.ext (category_theory.iso.refl (((category_theory.limits.cocones.whiskering e.inverse ⋙ category_theory.limits.cocones.precompose (F.left_unitor.inv ≫ category_theory.whisker_right e.counit_iso.inv F ≫ (e.inverse.associator e.functor F).inv)) ⋙ category_theory.limits.cocones.whiskering e.functor).obj s).X) _) _
@[simp]
theorem
category_theory.limits.cocones.equivalence_of_reindexing_functor_obj
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G)
(X : category_theory.limits.cocone F) :
def
category_theory.limits.cocones.equivalence_of_reindexing
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G) :
The categories of cocones over F and G are equivalent if F and G are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
def
category_theory.limits.cocones.forget
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
Forget the cocone structure and obtain just the cocone point.
Equations
- category_theory.limits.cocones.forget F = {obj := λ (t : category_theory.limits.cocone F), t.X, map := λ (s t : category_theory.limits.cocone F) (f : s ⟶ t), f.hom, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cocones.forget_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(s t : category_theory.limits.cocone F)
(f : s ⟶ t) :
(category_theory.limits.cocones.forget F).map f = f.hom
@[simp]
theorem
category_theory.limits.cocones.forget_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(t : category_theory.limits.cocone F) :
(category_theory.limits.cocones.forget F).obj t = t.X
def
category_theory.limits.cocones.functoriality
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D) :
A functor G : C ⥤ D sends cocones over F to cocones over F ⋙ G functorially.
Equations
- category_theory.limits.cocones.functoriality F G = {obj := λ (A : category_theory.limits.cocone F), {X := G.obj A.X, ι := {app := λ (j : J), G.map (A.ι.app j), naturality' := _}}, map := λ (_x _x_1 : category_theory.limits.cocone F) (f : _x ⟶ _x_1), {hom := G.map f.hom, w' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.limits.cocones.functoriality
@[simp]
theorem
category_theory.limits.cocones.functoriality_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(_x _x_1 : category_theory.limits.cocone F)
(f : _x ⟶ _x_1) :
@[simp]
theorem
category_theory.limits.cocones.functoriality_obj_ι_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(A : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.cocones.functoriality_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
(A : category_theory.limits.cocone F) :
@[protected, instance]
def
category_theory.limits.cocones.functoriality_full
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.full G]
[category_theory.faithful G] :
Equations
- category_theory.limits.cocones.functoriality_full F G = {preimage := λ (X Y : category_theory.limits.cocone F) (t : (category_theory.limits.cocones.functoriality F G).obj X ⟶ (category_theory.limits.cocones.functoriality F G).obj Y), {hom := G.preimage t.hom, w' := _}, witness' := _}
@[protected, instance]
def
category_theory.limits.cocones.functoriality_faithful
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.faithful G] :
@[simp]
theorem
category_theory.limits.cocones.functoriality_equivalence_inverse
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
(category_theory.limits.cocones.functoriality_equivalence F e).inverse = category_theory.limits.cocones.functoriality (F ⋙ e.functor) e.inverse ⋙ (category_theory.limits.cocones.precompose_equivalence (F.associator e.functor e.inverse ≪≫ category_theory.iso_whisker_left F e.unit_iso.symm ≪≫ F.right_unitor).symm).functor
@[simp]
theorem
category_theory.limits.cocones.functoriality_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
def
category_theory.limits.cocones.functoriality_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : 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
- category_theory.limits.cocones.functoriality_equivalence F e = let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F := F.associator e.functor e.inverse ≪≫ category_theory.iso_whisker_left F e.unit_iso.symm ≪≫ F.right_unitor in {functor := category_theory.limits.cocones.functoriality F e.functor, inverse := category_theory.limits.cocones.functoriality (F ⋙ e.functor) e.inverse ⋙ (category_theory.limits.cocones.precompose_equivalence f.symm).functor, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cocone F), category_theory.limits.cocones.ext (e.unit_iso.app ((𝟭 (category_theory.limits.cocone F)).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cocone (F ⋙ e.functor)), category_theory.limits.cocones.ext (e.counit_iso.app c.X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cocones.functoriality_equivalence_counit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
@[simp]
theorem
category_theory.limits.cocones.functoriality_equivalence_unit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : J ⥤ C)
(e : C ≌ D) :
@[protected, instance]
def
category_theory.limits.cocones.reflects_cocone_isomorphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.reflects_isomorphisms F]
(K : J ⥤ C) :
If F reflects isomorphisms, then cocones.functoriality F reflects isomorphisms
as well.
@[simp]
theorem
category_theory.functor.map_cone_π_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cone F)
(j : J) :
def
category_theory.functor.map_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cone F) :
category_theory.limits.cone (F ⋙ H)
The image of a cone in C under a functor G : C ⥤ D is a cone in D.
Equations
- H.map_cone c = (category_theory.limits.cones.functoriality F H).obj c
@[simp]
theorem
category_theory.functor.map_cone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.functor.map_cocone_ι_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.functor.map_cocone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cocone F) :
(H.map_cocone c).X = H.obj c.X
def
category_theory.functor.map_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
(c : category_theory.limits.cocone F) :
The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.
Equations
- H.map_cocone c = (category_theory.limits.cocones.functoriality F H).obj c
def
category_theory.functor.map_cone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{c c' : category_theory.limits.cone F}
(f : c ⟶ c') :
Given a cone morphism c ⟶ c', construct a cone morphism on the mapped cones functorially.
Equations
def
category_theory.functor.map_cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{c c' : category_theory.limits.cocone F}
(f : c ⟶ c') :
H.map_cocone c ⟶ H.map_cocone c'
Given a cocone morphism c ⟶ c', construct a cocone morphism on the mapped cocones
functorially.
Equations
def
category_theory.functor.map_cone_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
[category_theory.is_equivalence H]
(c : category_theory.limits.cone (F ⋙ H)) :
If H is an equivalence, we invert H.map_cone and get a cone for F from a cone
for F ⋙ H.
Equations
def
category_theory.functor.map_cone_map_cone_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ D}
(H : D ⥤ C)
[category_theory.is_equivalence H]
(c : category_theory.limits.cone (F ⋙ H)) :
H.map_cone (H.map_cone_inv c) ≅ c
map_cone is the left inverse to map_cone_inv.
Equations
def
category_theory.functor.map_cone_inv_map_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ D}
(H : D ⥤ C)
[category_theory.is_equivalence H]
(c : category_theory.limits.cone F) :
H.map_cone_inv (H.map_cone c) ≅ c
map_cone is the right inverse to map_cone_inv.
Equations
def
category_theory.functor.map_cocone_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
[category_theory.is_equivalence H]
(c : category_theory.limits.cocone (F ⋙ H)) :
If H is an equivalence, we invert H.map_cone and get a cone for F from a cone
for F ⋙ H.
Equations
def
category_theory.functor.map_cocone_map_cocone_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ D}
(H : D ⥤ C)
[category_theory.is_equivalence H]
(c : category_theory.limits.cocone (F ⋙ H)) :
H.map_cocone (H.map_cocone_inv c) ≅ c
map_cocone is the left inverse to map_cocone_inv.
def
category_theory.functor.map_cocone_inv_map_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ D}
(H : D ⥤ C)
[category_theory.is_equivalence H]
(c : category_theory.limits.cocone F) :
H.map_cocone_inv (H.map_cocone c) ≅ c
map_cocone is the right inverse to map_cocone_inv.
Equations
@[simp]
theorem
category_theory.functor.functoriality_comp_postcompose_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(X : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.functor.functoriality_comp_postcompose_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(X : category_theory.limits.cone F) :
def
category_theory.functor.functoriality_comp_postcompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H') :
functoriality F _ ⋙ postcompose (whisker_left F _) simplifies to functoriality F _.
Equations
@[simp]
theorem
category_theory.functor.postcompose_whisker_left_map_cone_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.functor.postcompose_whisker_left_map_cone_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cone F) :
def
category_theory.functor.postcompose_whisker_left_map_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cone F) :
(category_theory.limits.cones.postcompose (category_theory.whisker_left F α.hom)).obj (H.map_cone c) ≅ H'.map_cone 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.map_cone using the isomorphism α is
isomorphic to the cone H'.map_cone.
def
category_theory.functor.map_cone_postcompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cone F} :
map_cone 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
@[simp]
theorem
category_theory.functor.map_cone_postcompose_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cone F} :
@[simp]
theorem
category_theory.functor.map_cone_postcompose_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cone F} :
@[simp]
theorem
category_theory.functor.map_cone_postcompose_equivalence_functor_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cone F} :
def
category_theory.functor.map_cone_postcompose_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cone F} :
map_cone commutes with postcompose_equivalence
@[simp]
theorem
category_theory.functor.map_cone_postcompose_equivalence_functor_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cone F} :
def
category_theory.functor.functoriality_comp_precompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H') :
functoriality F _ ⋙ precompose (whisker_left F _) simplifies to functoriality F _.
Equations
@[simp]
theorem
category_theory.functor.functoriality_comp_precompose_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(X : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.functor.functoriality_comp_precompose_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(X : category_theory.limits.cocone F) :
def
category_theory.functor.precompose_whisker_left_map_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cocone F) :
(category_theory.limits.cocones.precompose (category_theory.whisker_left F α.inv)).obj (H.map_cocone c) ≅ H'.map_cocone 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.map_cocone using the isomorphism α is
isomorphic to the cocone H'.map_cocone.
@[simp]
theorem
category_theory.functor.precompose_whisker_left_map_cocone_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.functor.precompose_whisker_left_map_cocone_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{H H' : C ⥤ D}
(α : H ≅ H')
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.functor.map_cocone_precompose_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cocone G} :
@[simp]
theorem
category_theory.functor.map_cocone_precompose_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cocone G} :
def
category_theory.functor.map_cocone_precompose
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ⟶ G}
{c : category_theory.limits.cocone G} :
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
@[simp]
theorem
category_theory.functor.map_cocone_precompose_equivalence_functor_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cocone G} :
@[simp]
theorem
category_theory.functor.map_cocone_precompose_equivalence_functor_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cocone G} :
def
category_theory.functor.map_cocone_precompose_equivalence_functor
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F G : J ⥤ C}
(H : C ⥤ D)
{α : F ≅ G}
{c : category_theory.limits.cocone G} :
map_cocone commutes with precompose_equivalence
def
category_theory.functor.map_cone_whisker
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cone F} :
map_cone commutes with whisker
Equations
@[simp]
theorem
category_theory.functor.map_cone_whisker_hom_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cone F} :
@[simp]
theorem
category_theory.functor.map_cone_whisker_inv_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cone F} :
@[simp]
theorem
category_theory.functor.map_cocone_whisker_inv_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cocone F} :
def
category_theory.functor.map_cocone_whisker
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cocone F} :
map_cocone commutes with whisker
Equations
@[simp]
theorem
category_theory.functor.map_cocone_whisker_hom_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(H : C ⥤ D)
{E : K ⥤ J}
{c : category_theory.limits.cocone F} :
@[simp]
theorem
category_theory.limits.cocone.op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
c.op.X = opposite.op c.X
@[simp]
theorem
category_theory.limits.cocone.op_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocone.op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
Change a cocone F into a cone F.op.
Equations
- c.op = {X := opposite.op c.X, π := category_theory.nat_trans.op c.ι}
def
category_theory.limits.cone.op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
Change a cone F into a cocone F.op.
Equations
- c.op = {X := opposite.op c.X, ι := category_theory.nat_trans.op c.π}
@[simp]
theorem
category_theory.limits.cone.op_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
c.op.X = opposite.op c.X
@[simp]
theorem
category_theory.limits.cocone.unop_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F.op) :
@[simp]
theorem
category_theory.limits.cocone.unop_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F.op) :
c.unop.X = opposite.unop c.X
def
category_theory.limits.cocone.unop
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F.op) :
Change a cocone F.op into a cone F.
Equations
- c.unop = {X := opposite.unop c.X, π := category_theory.nat_trans.remove_op c.ι}
def
category_theory.limits.cone.unop
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F.op) :
Change a cone F.op into a cocone F.
Equations
- c.unop = {X := opposite.unop c.X, ι := category_theory.nat_trans.remove_op c.π}
@[simp]
theorem
category_theory.limits.cone.unop_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F.op) :
@[simp]
theorem
category_theory.limits.cone.unop_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F.op) :
c.unop.X = opposite.unop c.X
def
category_theory.limits.cocone_equivalence_op_cone_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
The category of cocones on F
is equivalent to the opposite category of
the category of cones on the opposite of F.
Equations
- category_theory.limits.cocone_equivalence_op_cone_op F = {functor := {obj := λ (c : category_theory.limits.cocone F), opposite.op c.op, map := λ (X Y : category_theory.limits.cocone F) (f : X ⟶ Y), quiver.hom.op {hom := f.hom.op, w' := _}, map_id' := _, map_comp' := _}, inverse := {obj := λ (c : (category_theory.limits.cone F.op)ᵒᵖ), (opposite.unop c).unop, map := λ (X Y : (category_theory.limits.cone F.op)ᵒᵖ) (f : X ⟶ Y), {hom := f.unop.hom.unop, w' := _}, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cocone F), category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cocone F)).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : (category_theory.limits.cone F.op)ᵒᵖ), opposite.rec (λ (c : category_theory.limits.cone F.op), id (category_theory.limits.cones.ext (category_theory.iso.refl c.X) _).op) c) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_functor_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_inverse_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : (category_theory.limits.cone F.op)ᵒᵖ) :
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_counit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_inverse_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X Y : (category_theory.limits.cone F.op)ᵒᵖ)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_functor_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X Y : category_theory.limits.cocone F)
(f : X ⟶ Y) :
(category_theory.limits.cocone_equivalence_op_cone_op F).functor.map f = quiver.hom.op {hom := f.hom.op, w' := _}
@[simp]
theorem
category_theory.limits.cocone_equivalence_op_cone_op_unit_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
def
category_theory.limits.cone_of_cocone_left_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.left_op) :
Change a cocone on F.left_op : Jᵒᵖ ⥤ C to a cocone on F : J ⥤ Cᵒᵖ.
Equations
@[simp]
theorem
category_theory.limits.cone_of_cocone_left_op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.left_op) :
@[simp]
theorem
category_theory.limits.cone_of_cocone_left_op_π_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.left_op)
(X : J) :
(category_theory.limits.cone_of_cocone_left_op c).π.app X = (c.ι.app (opposite.op X)).op
@[simp]
theorem
category_theory.limits.cocone_left_op_of_cone_ι_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F)
(X : Jᵒᵖ) :
(category_theory.limits.cocone_left_op_of_cone c).ι.app X = (c.π.app (opposite.unop X)).unop
@[simp]
theorem
category_theory.limits.cocone_left_op_of_cone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F) :
def
category_theory.limits.cocone_left_op_of_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F) :
Change a cone on F : J ⥤ Cᵒᵖ to a cocone on F.left_op : Jᵒᵖ ⥤ C.
Equations
@[simp]
theorem
category_theory.limits.cocone_of_cone_left_op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.left_op) :
def
category_theory.limits.cocone_of_cone_left_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.left_op) :
Change a cone on F.left_op : Jᵒᵖ ⥤ C to a cocone on F : J ⥤ Cᵒᵖ.
Equations
@[simp]
theorem
category_theory.limits.cocone_of_cone_left_op_ι_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.left_op)
(j : J) :
(category_theory.limits.cocone_of_cone_left_op c).ι.app j = (c.π.app (opposite.op j)).op
@[simp]
theorem
category_theory.limits.cone_left_op_of_cocone_π_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F)
(X : Jᵒᵖ) :
(category_theory.limits.cone_left_op_of_cocone c).π.app X = (c.ι.app (opposite.unop X)).unop
@[simp]
theorem
category_theory.limits.cone_left_op_of_cocone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cone_left_op_of_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F) :
Change a cocone on F : J ⥤ Cᵒᵖ to a cone on F.left_op : Jᵒᵖ ⥤ C.
Equations
def
category_theory.limits.cone_of_cocone_right_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F.right_op) :
Change a cocone on F.right_op : J ⥤ Cᵒᵖ to a cone on F : Jᵒᵖ ⥤ C.
Equations
@[simp]
theorem
category_theory.limits.cone_of_cocone_right_op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F.right_op) :
@[simp]
theorem
category_theory.limits.cone_of_cocone_right_op_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F.right_op) :
@[simp]
theorem
category_theory.limits.cocone_right_op_of_cone_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cocone_right_op_of_cone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F) :
def
category_theory.limits.cocone_right_op_of_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F) :
Change a cone on F : Jᵒᵖ ⥤ C to a cocone on F.right_op : Jᵒᵖ ⥤ C.
Equations
def
category_theory.limits.cocone_of_cone_right_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F.right_op) :
Change a cone on F.right_op : J ⥤ Cᵒᵖ to a cocone on F : Jᵒᵖ ⥤ C.
Equations
@[simp]
theorem
category_theory.limits.cocone_of_cone_right_op_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F.right_op) :
@[simp]
theorem
category_theory.limits.cocone_of_cone_right_op_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cone F.right_op) :
@[simp]
theorem
category_theory.limits.cone_right_op_of_cocone_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cone_right_op_of_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F) :
Change a cocone on F : Jᵒᵖ ⥤ C to a cone on F.right_op : J ⥤ Cᵒᵖ.
Equations
@[simp]
theorem
category_theory.limits.cone_right_op_of_cocone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ C}
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cone_of_cocone_unop_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.unop) :
def
category_theory.limits.cone_of_cocone_unop
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.unop) :
Change a cocone on F.unop : J ⥤ C into a cone on F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
@[simp]
theorem
category_theory.limits.cone_of_cocone_unop_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.unop) :
@[simp]
theorem
category_theory.limits.cocone_unop_of_cone_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F) :
def
category_theory.limits.cocone_unop_of_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F) :
Change a cone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cocone on F.unop : J ⥤ C.
Equations
@[simp]
theorem
category_theory.limits.cocone_unop_of_cone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F) :
def
category_theory.limits.cocone_of_cone_unop
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.unop) :
Change a cone on F.unop : J ⥤ C into a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
@[simp]
theorem
category_theory.limits.cocone_of_cone_unop_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.unop) :
@[simp]
theorem
category_theory.limits.cocone_of_cone_unop_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F.unop) :
def
category_theory.limits.cone_unop_of_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F) :
Change a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ into a cone on F.unop : J ⥤ C.
Equations
@[simp]
theorem
category_theory.limits.cone_unop_of_cocone_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cone_unop_of_cocone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : Jᵒᵖ ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.functor.map_cone_op_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
(t : category_theory.limits.cone F) :
(G.map_cone_op t).hom.hom = (category_theory.iso.refl (G.map_cone t).op.X).hom
def
category_theory.functor.map_cone_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
(t : category_theory.limits.cone F) :
The opposite cocone of the image of a cone is the image of the opposite cocone.
Equations
@[simp]
theorem
category_theory.functor.map_cone_op_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
(t : category_theory.limits.cone F) :
(G.map_cone_op t).inv.hom = (category_theory.iso.refl (G.map_cone t).op.X).inv
def
category_theory.functor.map_cocone_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
{t : category_theory.limits.cocone F} :
The opposite cone of the image of a cocone is the image of the opposite cone.
Equations
@[simp]
theorem
category_theory.functor.map_cocone_op_hom_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
{t : category_theory.limits.cocone F} :
G.map_cocone_op.hom.hom = (category_theory.iso.refl (G.map_cocone t).op.X).hom
@[simp]
theorem
category_theory.functor.map_cocone_op_inv_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
(G : C ⥤ D)
{t : category_theory.limits.cocone F} :
G.map_cocone_op.inv.hom = (category_theory.iso.refl (G.map_cocone t).op.X).inv