Cones and cocones #
We define Cone F
, a cone over a functor F
,
and F.cones : Cᵒᵖ ⥤ Type
, the functor associating to X
the cones over F
with cone point X
.
A cone c
is defined by specifying its cone point c.pt
and a natural transformation c.π
from the constant c.pt
valued functor to F
.
We provide c.w f : c.π.app j ≫ F.map f = c.π.app j'
for any f : j ⟶ j'
as a wrapper for c.π.naturality f
avoiding unneeded identity morphisms.
We define c.extend f
, where c : cone F
and f : Y ⟶ c.pt
for some other Y
,
which replaces the cone point by Y
and inserts f
into each of the components of the cone.
Similarly we have c.whisker F
producing a Cone (E ⋙ F)
We define morphisms of cones, and the category of cones.
We define Cone.postcompose α : cone F ⥤ cone G
for α
a natural transformation F ⟶ G
.
And, of course, we dualise all this to cocones as well.
For more results about the category of cones, see cone_category.lean
.
If F : J ⥤ C
then F.cones
is the functor assigning to an object X : C
the
type of natural transformations from the constant functor with value X
to F
.
An object representing this functor is a limit of F
.
Instances For
If F : J ⥤ C
then F.cocones
is the functor assigning to an object (X : C)
the type of natural transformations from F
to the constant functor with value X
.
An object corepresenting this functor is a colimit of F
.
Instances For
Functorially associated to each functor J ⥤ C
, we have the C
-presheaf consisting of
cones with a given cone point.
Instances For
Contravariantly associated to each functor J ⥤ C
, we have the C
-copresheaf consisting of
cocones with a given cocone point.
Instances For
- pt : C
An object of
C
- π : (CategoryTheory.Functor.const J).obj s.pt ⟶ F
A natural transformation from the constant functor at
X
toF
A c : Cone F
is:
Example: if J
is a category coming from a poset then the data required to make
a term of type Cone F
is morphisms πⱼ : c.pt ⟶ F j
for all j : J
and,
for all i ≤ j
in J
, morphisms πᵢⱼ : F i ⟶ F j
such that πᵢ ≫ πᵢⱼ = πᵢ
.
Cone F
is equivalent, via cone.equiv
below, to Σ X, F.cones.obj X
.
Instances For
- pt : C
An object of
C
- ι : F ⟶ (CategoryTheory.Functor.const J).obj s.pt
A natural transformation from
F
to the constant functor atpt
A c : Cocone F
is
For example, if the source J
of F
is a partially ordered set, then to give
c : Cocone F
is to give a collection of morphisms ιⱼ : F j ⟶ c.pt
and, for
all j ≤ k
in J
, morphisms ιⱼₖ : F j ⟶ F k
such that Fⱼₖ ≫ Fₖ = Fⱼ
for all j ≤ k
.
Cocone F
is equivalent, via Cone.equiv
below, to Σ X, F.cocones.obj X
.
Instances For
The isomorphism between a cone on F
and an element of the functor F.cones
.
Instances For
A map to the vertex of a cone naturally induces a cone by composition.
Instances For
A map to the vertex of a cone induces a cone by composition.
Instances For
Whisker a cone by precomposition of a functor.
Instances For
The isomorphism between a cocone on F
and an element of the functor F.cocones
.
Instances For
A map from the vertex of a cocone naturally induces a cocone by composition.
Instances For
A map from the vertex of a cocone induces a cocone by composition.
Instances For
Whisker a cocone by precomposition of a functor. See whiskering
for a functorial
version.
Instances For
- hom : A.pt ⟶ B.pt
A morphism between the two vertex objects of the cones
- w : ∀ (j : J), CategoryTheory.CategoryStruct.comp s.hom (B.π.app j) = A.π.app j
The triangle consisting of the two natural transformations and
hom
commutes
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
The category of cones on a given diagram.
To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.
Instances For
Eta rule for cones.
Instances For
Given a cone morphism whose object part is an isomorphism, produce an isomorphism of cones.
Functorially postcompose a cone for F
by a natural transformation F ⟶ G
to give a cone for G
.
Instances For
Postcomposing a cone by the composite natural transformation α ≫ β
is the same as
postcomposing by α
and then by β
.
Instances For
Postcomposing by the identity does not change the cone up to isomorphism.
Instances For
If F
and G
are naturally isomorphic functors, then they have equivalent categories of
cones.
Instances For
Whiskering on the left by E : K ⥤ J
gives a functor from Cone F
to Cone (E ⋙ F)
.
Instances For
Whiskering by an equivalence gives an equivalence between categories of cones.
Instances For
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).
Instances For
Forget the cone structure and obtain just the cone point.
Instances For
A functor G : C ⥤ D
sends cones over F
to cones over F ⋙ G
functorially.
Instances For
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
.
Instances For
If F
reflects isomorphisms, then Cones.functoriality F
reflects isomorphisms
as well.
- hom : A.pt ⟶ B.pt
A morphism between the (co)vertex objects in
C
- w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) s.hom = B.ι.app j
The triangle made from the two natural transformations and
hom
commutes
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
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Instances For
Eta rule for cocones.
Instances For
Given a cocone morphism whose object part is an isomorphism, produce an isomorphism of cocones.
Functorially precompose a cocone for F
by a natural transformation G ⟶ F
to give a cocone
for G
.
Instances For
Precomposing a cocone by the composite natural transformation α ≫ β
is the same as
precomposing by β
and then by α
.
Instances For
Precomposing by the identity does not change the cocone up to isomorphism.
Instances For
If F
and G
are naturally isomorphic functors, then they have equivalent categories of
cocones.
Instances For
Whiskering on the left by E : K ⥤ J
gives a functor from Cocone F
to Cocone (E ⋙ F)
.
Instances For
Whiskering by an equivalence gives an equivalence between categories of cones.
Instances For
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).
Instances For
Forget the cocone structure and obtain just the cocone point.
Instances For
A functor G : C ⥤ D
sends cocones over F
to cocones over F ⋙ G
functorially.
Instances For
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
.
Instances For
If F
reflects isomorphisms, then cocones.functoriality F
reflects isomorphisms
as well.
The image of a cone in C under a functor G : C ⥤ D is a cone in D.
Instances For
The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.
Instances For
Given a cone morphism c ⟶ c'
, construct a cone morphism on the mapped cones functorially.
Instances For
Given a cocone morphism c ⟶ c'
, construct a cocone morphism on the mapped cocones
functorially.
Instances For
If H
is an equivalence, we invert H.mapCone
and get a cone for F
from a cone
for F ⋙ H
.
Instances For
mapCone
is the left inverse to mapConeInv
.
Instances For
MapCone
is the right inverse to mapConeInv
.
Instances For
If H
is an equivalence, we invert H.mapCone
and get a cone for F
from a cone
for F ⋙ H
.
Instances For
mapCocone
is the left inverse to mapCoconeInv
.
Instances For
mapCocone
is the right inverse to mapCoconeInv
.
Instances For
functoriality F _ ⋙ postcompose (whisker_left F _)
simplifies to functoriality F _
.
Instances For
For F : J ⥤ C
, given a cone c : Cone F
, and a natural isomorphism α : H ≅ H'
for functors
H H' : C ⥤ D
, the postcomposition of the cone H.mapCone
using the isomorphism α
is
isomorphic to the cone H'.mapCone
.
Instances For
mapCone
commutes with postcompose
. In particular, for F : J ⥤ C
, given a cone c : Cone F
, a
natural transformation α : F ⟶ G
and a functor H : C ⥤ D
, we have two obvious ways of producing
a cone over G ⋙ H
, and they are both isomorphic.
Instances For
mapCone
commutes with postcomposeEquivalence
Instances For
functoriality F _ ⋙ precompose (whiskerLeft F _)
simplifies to functoriality F _
.
Instances For
For F : J ⥤ C
, given a cocone c : Cocone F
, and a natural isomorphism α : H ≅ H'
for functors
H H' : C ⥤ D
, the precomposition of the cocone H.mapCocone
using the isomorphism α
is
isomorphic to the cocone H'.mapCocone
.
Instances For
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.
Instances For
mapCocone
commutes with precomposeEquivalence
Instances For
Instances For
mapCocone
commutes with whisker
Instances For
Change a Cocone F
into a Cone F.op
.
Instances For
Change a Cone F
into a Cocone F.op
.
Instances For
Change a Cocone F.op
into a Cone F
.
Instances For
Change a Cone F.op
into a Cocone F
.
Instances For
The category of cocones on F
is equivalent to the opposite category of
the category of cones on the opposite of F
.
Instances For
Change a cocone on F.leftOp : Jᵒᵖ ⥤ C
to a cocone on F : J ⥤ Cᵒᵖ
.
Instances For
Change a cone on F : J ⥤ Cᵒᵖ
to a cocone on F.leftOp : Jᵒᵖ ⥤ C
.
Instances For
Change a cone on F.leftOp : Jᵒᵖ ⥤ C
to a cocone on F : J ⥤ Cᵒᵖ
.
Instances For
Change a cocone on F : J ⥤ Cᵒᵖ
to a cone on F.leftOp : Jᵒᵖ ⥤ C
.
Instances For
Change a cocone on F.rightOp : J ⥤ Cᵒᵖ
to a cone on F : Jᵒᵖ ⥤ C
.
Instances For
Change a cone on F : Jᵒᵖ ⥤ C
to a cocone on F.rightOp : Jᵒᵖ ⥤ C
.
Instances For
Change a cone on F.rightOp : J ⥤ Cᵒᵖ
to a cocone on F : Jᵒᵖ ⥤ C
.
Instances For
Change a cocone on F : Jᵒᵖ ⥤ C
to a cone on F.rightOp : J ⥤ Cᵒᵖ
.
Instances For
Change a cocone on F.unop : J ⥤ C
into a cone on F : Jᵒᵖ ⥤ Cᵒᵖ
.
Instances For
Change a cone on F : Jᵒᵖ ⥤ Cᵒᵖ
into a cocone on F.unop : J ⥤ C
.
Instances For
Change a cone on F.unop : J ⥤ C
into a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ
.
Instances For
Change a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ
into a cone on F.unop : J ⥤ C
.
Instances For
The opposite cocone of the image of a cone is the image of the opposite cocone.
Instances For
The opposite cone of the image of a cocone is the image of the opposite cone.