def
category_theory.functor.cones
{J : Type v}
[category_theory.small_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
theorem
category_theory.functor.cones_obj
{J : Type v}
[category_theory.small_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)
def
category_theory.functor.cocones
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
C ⥤ Type v
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
theorem
category_theory.functor.cocones_obj
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
(X : C) :
@[simp]
theorem
category_theory.functor.cocones_map_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{X₁ X₂ : C}
(f : X₁ ⟶ X₂)
(t : F.cocones.obj X₁)
(j : J) :
@[simp]
theorem
category_theory.cones_map
(J : Type v)
[category_theory.small_category J]
(C : Type u)
[category_theory.category C]
(F G : J ⥤ C)
(f : F ⟶ G) :
@[simp]
theorem
category_theory.cones_obj
(J : Type v)
[category_theory.small_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 v)
[category_theory.small_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_2, 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 v)
[category_theory.small_category J]
(C : Type u)
[category_theory.category C]
(F G : (J ⥤ C)ᵒᵖ)
(f : F ⟶ G) :
@[simp]
theorem
category_theory.cocones_obj
(J : Type v)
[category_theory.small_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 v)
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u v)
- X : C
- π : (category_theory.functor.const J).obj c.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.
@[simp]
theorem
category_theory.limits.cone.w
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u v)
- X : C
- ι : F ⟶ (category_theory.functor.const J).obj c.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.
@[simp]
theorem
category_theory.limits.cocone.w
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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') :
def
category_theory.limits.cone.equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
category_theory.limits.cone F ≅ Σ (X : Cᵒᵖ), F.cones.obj X
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]
def
category_theory.limits.cone.extensions
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
category_theory.yoneda.obj c.X ⟶ F.cones
Equations
- c.extensions = {app := λ (X : Cᵒᵖ) (f : (category_theory.yoneda.obj c.X).obj X), (category_theory.functor.const J).map f ≫ c.π, naturality' := _}
@[simp]
def
category_theory.limits.cone.extend
{J : Type v}
[category_theory.small_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) f}
@[simp]
theorem
category_theory.limits.cone.extend_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F)
{X : Cᵒᵖ}
(f : opposite.unop X ⟶ c.X) :
(c.extend f).π = c.extensions.app X f
@[simp]
theorem
category_theory.limits.cone.whisker_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
def
category_theory.limits.cone.whisker
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
category_theory.limits.cocone F ≅ Σ (X : C), F.cocones.obj X
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' := _}
@[simp]
def
category_theory.limits.cocone.extensions
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
Equations
- c.extensions = {app := λ (X : C) (f : (category_theory.coyoneda.obj (opposite.op c.X)).obj X), c.ι ≫ (category_theory.functor.const J).map f, naturality' := _}
@[simp]
def
category_theory.limits.cocone.extend
{J : Type v}
[category_theory.small_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.extend_ι
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
(c.extend f).ι = c.extensions.app X f
@[simp]
theorem
category_theory.limits.cocone.whisker_ι
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocone.whisker
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
{_inst_1 : category_theory.small_category J}
{C : Type u}
{_inst_2 : 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 v}
{_inst_1 : category_theory.small_category J}
{C : Type u}
{_inst_2 : 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 v}
[category_theory.small_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.
@[simp]
theorem
category_theory.limits.cone.category_to_category_struct_comp_hom
{J : Type v}
[category_theory.small_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) :
@[simp]
theorem
category_theory.limits.cone.category_to_category_struct_to_has_hom_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(A B : category_theory.limits.cone F) :
(A ⟶ B) = category_theory.limits.cone_morphism A B
@[simp]
theorem
category_theory.limits.cone.category_to_category_struct_id_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(B : category_theory.limits.cone F) :
@[instance]
def
category_theory.limits.cone.category
{J : Type v}
[category_theory.small_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_has_hom := {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.cones.ext_inv_hom
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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
def
category_theory.limits.cones.cone_iso_of_hom_iso
{J : Type v}
[category_theory.small_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.
Equations
- category_theory.limits.cones.cone_iso_of_hom_iso f = {inv := {hom := category_theory.is_iso.inv f.hom i, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.cones.postcompose_obj_X
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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
def
category_theory.limits.cones.postcompose_id
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G) :
def
category_theory.limits.cones.postcompose_equivalence
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(E : K ⥤ J)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_counit_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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.inverse.associator e.functor F).inv ≫ category_theory.whisker_right e.counit_iso.hom F ≫ F.left_unitor.hom)) ⋙ category_theory.limits.cones.whiskering e.functor).obj s).X) _) _
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_inverse
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cones.whiskering_equivalence_unit_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
def
category_theory.limits.cones.whiskering_equivalence
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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.inverse.associator e.functor F).inv ≫ category_theory.whisker_right e.counit_iso.hom F ≫ F.left_unitor.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.inverse.associator e.functor F).inv ≫ category_theory.whisker_right e.counit_iso.hom F ≫ F.left_unitor.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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
def
category_theory.limits.cones.equivalence_of_reindexing
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
{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_functor_obj
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.forget_map
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D) :
Equations
@[simp]
theorem
category_theory.limits.cones.functoriality_obj_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
(A : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cones.functoriality_map_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
(X Y : category_theory.limits.cone F)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.limits.cones.functoriality_obj_π_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
(A : category_theory.limits.cone F)
(j : J) :
@[instance]
def
category_theory.limits.cones.functoriality_full
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(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' := _}
@[instance]
def
category_theory.limits.cones.functoriality_faithful
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.faithful G] :
@[instance]
def
category_theory.limits.cones.reflects_cone_isomorphism
{J : Type v}
[category_theory.small_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.
Equations
- category_theory.limits.cones.reflects_cone_isomorphism F K = {reflects := λ (A B : category_theory.limits.cone K) (f : A ⟶ B) (_inst_3_1 : category_theory.is_iso ((category_theory.limits.cones.functoriality K F).map f)), category_theory.limits.cones.cone_iso_of_hom_iso f}
theorem
category_theory.limits.cocone_morphism.ext_iff
{J : Type v}
{_inst_1 : category_theory.small_category J}
{C : Type u}
{_inst_2 : 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 v}
[category_theory.small_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.
theorem
category_theory.limits.cocone_morphism.ext
{J : Type v}
{_inst_1 : category_theory.small_category J}
{C : Type u}
{_inst_2 : 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
@[simp]
theorem
category_theory.limits.cocone.category_to_category_struct_comp_hom
{J : Type v}
[category_theory.small_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) :
@[simp]
theorem
category_theory.limits.cocone.category_to_category_struct_to_has_hom_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(A B : category_theory.limits.cocone F) :
(A ⟶ B) = category_theory.limits.cocone_morphism A B
@[simp]
theorem
category_theory.limits.cocone.category_to_category_struct_id_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(B : category_theory.limits.cocone F) :
@[instance]
def
category_theory.limits.cocone.category
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C} :
Equations
- category_theory.limits.cocone.category = {to_category_struct := {to_has_hom := {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.cocones.ext_inv_hom
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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
def
category_theory.limits.cocones.cocone_iso_of_hom_iso
{J : Type v}
[category_theory.small_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.
Equations
- category_theory.limits.cocones.cocone_iso_of_hom_iso f = {inv := {hom := category_theory.is_iso.inv f.hom i, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.cocones.precompose
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
def
category_theory.limits.cocones.precompose_equivalence
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : G ≅ F) :
def
category_theory.limits.cocones.whiskering
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(E : K ⥤ J)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocones.whiskering_equivalence
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_unit_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_functor
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(e : K ≌ J) :
@[simp]
theorem
category_theory.limits.cocones.whiskering_equivalence_counit_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
(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) _) _
def
category_theory.limits.cocones.equivalence_of_reindexing
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
{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).
@[simp]
theorem
category_theory.limits.cocones.equivalence_of_reindexing_functor_obj
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{K : Type v}
[category_theory.small_category K]
{G : K ⥤ C}
(e : K ≌ J)
(α : e.functor ⋙ F ≅ G)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocones.forget
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D) :
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' := _}
@[simp]
theorem
category_theory.limits.cocones.functoriality_map_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
(A : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.cocones.functoriality_obj_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
(A : category_theory.limits.cocone F) :
@[instance]
def
category_theory.limits.cocones.functoriality_full
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(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' := _}
@[instance]
def
category_theory.limits.cocones.functoriality_faithful
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.faithful G] :
@[instance]
def
category_theory.limits.cocones.reflects_cocone_isomorphism
{J : Type v}
[category_theory.small_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.
Equations
- category_theory.limits.cocones.reflects_cocone_isomorphism F K = {reflects := λ (A B : category_theory.limits.cocone K) (f : A ⟶ B) (_inst_3_1 : category_theory.is_iso ((category_theory.limits.cocones.functoriality K F).map f)), category_theory.limits.cocones.cocone_iso_of_hom_iso f}
def
category_theory.functor.map_cone
{J : Type v}
[category_theory.small_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
def
category_theory.functor.map_cocone
{J : Type v}
[category_theory.small_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
@[simp]
theorem
category_theory.functor.map_cone_X
{J : Type v}
[category_theory.small_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_X
{J : Type v}
[category_theory.small_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
@[simp]
theorem
category_theory.functor.map_cone_inv_X
{J : Type v}
[category_theory.small_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)) :
@[simp]
theorem
category_theory.functor.map_cone_inv_π
{J : Type v}
[category_theory.small_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)) :
(H.map_cone_inv c).π = ((category_theory.cones J C).map (category_theory.whisker_left F H.fun_inv_id.hom ≫ F.right_unitor.hom)).app (opposite.op (H.inv.map_cone c).X) (H.inv.map_cone c).π
def
category_theory.functor.map_cone_inv
{J : Type v}
[category_theory.small_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 an original cone for F from a cone
for F ⋙ H.
Equations
- H.map_cone_inv c = let t : category_theory.limits.cone ((F ⋙ H) ⋙ H.inv) := H.inv.map_cone c, α : (F ⋙ H) ⋙ H.inv ⟶ F := category_theory.whisker_left F H.fun_inv_id.hom ≫ F.right_unitor.hom in {X := t.X, π := ((category_theory.cones J C).map α).app (opposite.op t.X) t.π}
def
category_theory.functor.map_cone_morphism
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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
@[simp]
theorem
category_theory.functor.map_cone_π
{J : Type v}
[category_theory.small_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) :
@[simp]
theorem
category_theory.functor.map_cocone_ι
{J : Type v}
[category_theory.small_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) :
def
category_theory.functor.map_cone_map_cone_inv
{J : Type v}
[category_theory.small_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
- H.map_cone_map_cone_inv c = category_theory.limits.cones.ext (H.inv_fun_id.app c.X) _
def
category_theory.functor.map_cone_inv_map_cone
{J : Type v}
[category_theory.small_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
- H.map_cone_inv_map_cone c = category_theory.limits.cones.ext (H.fun_inv_id.app c.X) _
def
category_theory.limits.cone_of_cocone_left_op
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F.left_op)
(j : J) :
(category_theory.limits.cone_of_cocone_left_op c).π.app j = (c.ι.app (opposite.op j)).op
@[simp]
theorem
category_theory.limits.cocone_left_op_of_cone_X
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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_left_op_of_cone_ι_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cone F)
(j : Jᵒᵖ) :
(category_theory.limits.cocone_left_op_of_cone c).ι.app j = (c.π.app (opposite.unop j)).unop
@[simp]
theorem
category_theory.limits.cocone_of_cone_left_op_X
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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 v}
[category_theory.small_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_X
{J : Type v}
[category_theory.small_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 v}
[category_theory.small_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
@[simp]
theorem
category_theory.limits.cone_left_op_of_cocone_π_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ Cᵒᵖ}
(c : category_theory.limits.cocone F)
(j : Jᵒᵖ) :
(category_theory.limits.cone_left_op_of_cocone c).π.app j = (c.ι.app (opposite.unop j)).unop