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
.
Equations
- F.cones = (CategoryTheory.Functor.const J).op.comp (CategoryTheory.yoneda.obj 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
.
Equations
- F.cocones = (CategoryTheory.Functor.const J).comp (CategoryTheory.coyoneda.obj (Opposite.op F))
Instances For
Functorially associated to each functor J ⥤ C
, we have the C
-presheaf consisting of
cones with a given cone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Contravariantly associated to each functor J ⥤ C
, we have the C
-copresheaf consisting of
cocones with a given cocone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A c : Cone F
is:
Example: if J
is a category coming from a poset then the data required to make
a term of type Cone F
is morphisms πⱼ : c.pt ⟶ F j
for all j : J
and,
for all i ≤ j
in J
, morphisms πᵢⱼ : F i ⟶ F j
such that πᵢ ≫ πᵢⱼ = πᵢ
.
Cone F
is equivalent, via cone.equiv
below, to Σ X, F.cones.obj X
.
- pt : C
An object of
C
- π : (CategoryTheory.Functor.const J).obj self.pt ⟶ F
A natural transformation from the constant functor at
X
toF
Instances For
Equations
- One or more equations did not get rendered due to their size.
A c : Cocone F
is
For example, if the source J
of F
is a partially ordered set, then to give
c : Cocone F
is to give a collection of morphisms ιⱼ : F j ⟶ c.pt
and, for
all j ≤ k
in J
, morphisms ιⱼₖ : F j ⟶ F k
such that Fⱼₖ ≫ Fₖ = Fⱼ
for all j ≤ k
.
Cocone F
is equivalent, via Cone.equiv
below, to Σ X, F.cocones.obj X
.
- pt : C
An object of
C
- ι : F ⟶ (CategoryTheory.Functor.const J).obj self.pt
A natural transformation from
F
to the constant functor atpt
Instances For
Equations
- One or more equations did not get rendered due to their size.
The isomorphism between a cone on F
and an element of the functor F.cones
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A map to the vertex of a cone naturally induces a cone by composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A map to the vertex of a cone induces a cone by composition.
Equations
- c.extend f = { pt := X, π := c.extensions.app (Opposite.op X) { down := f } }
Instances For
Whisker a cone by precomposition of a functor.
Equations
- CategoryTheory.Limits.Cone.whisker E c = { pt := c.pt, π := CategoryTheory.whiskerLeft E c.π }
Instances For
The isomorphism between a cocone on F
and an element of the functor F.cocones
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A map from the vertex of a cocone naturally induces a cocone by composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A map from the vertex of a cocone induces a cocone by composition.
Equations
- c.extend f = { pt := Y, ι := c.extensions.app Y { down := f } }
Instances For
Whisker a cocone by precomposition of a functor. See whiskering
for a functorial
version.
Equations
- CategoryTheory.Limits.Cocone.whisker E c = { pt := c.pt, ι := CategoryTheory.whiskerLeft E c.ι }
Instances For
A cone morphism between two cones for the same diagram is a morphism of the cone points which commutes with the cone legs.
- hom : A.pt ⟶ B.pt
A morphism between the two vertex objects of the cones
- w : ∀ (j : J), CategoryTheory.CategoryStruct.comp self.hom (B.π.app j) = A.π.app j
The triangle consisting of the two natural transformations and
hom
commutes
Instances For
Equations
- CategoryTheory.Limits.inhabitedConeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
The category of cones on a given diagram.
Equations
- CategoryTheory.Limits.Cone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.
Equations
- CategoryTheory.Limits.Cones.ext φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Eta rule for cones.
Equations
Instances For
Given a cone morphism whose object part is an isomorphism, produce an isomorphism of cones.
There is a morphism from an extended cone to the original cone.
Equations
- CategoryTheory.Limits.Cones.extend s f = { hom := f, w := ⋯ }
Instances For
Extending a cone by the identity does nothing.
Equations
- CategoryTheory.Limits.Cones.extendId s = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.id s.pt)).pt) ⋯
Instances For
Extending a cone by a composition is the same as extending the cone twice.
Equations
- CategoryTheory.Limits.Cones.extendComp s f g = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.comp f g)).pt) ⋯
Instances For
A cone extended by an isomorphism is isomorphic to the original cone.
Equations
- CategoryTheory.Limits.Cones.extendIso s f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Functorially postcompose a cone for F
by a natural transformation F ⟶ G
to give a cone for G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Postcomposing a cone by the composite natural transformation α ≫ β
is the same as
postcomposing by α
and then by β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Postcomposing by the identity does not change the cone up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If F
and G
are naturally isomorphic functors, then they have equivalent categories of
cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whiskering on the left by E : K ⥤ J
gives a functor from Cone F
to Cone (E ⋙ F)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whiskering by an equivalence gives an equivalence between categories of cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categories of cones over F
and G
are equivalent if F
and G
are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
Equations
Instances For
Forget the cone structure and obtain just the cone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor G : C ⥤ D
sends cones over F
to cones over F ⋙ G
functorially.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If e : C ≌ D
is an equivalence of categories, then functoriality F e.functor
induces an
equivalence between cones over F
and cones over F ⋙ e.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If F
reflects isomorphisms, then Cones.functoriality F
reflects isomorphisms
as well.
A cocone morphism between two cocones for the same diagram is a morphism of the cocone points which commutes with the cocone legs.
- hom : A.pt ⟶ B.pt
A morphism between the (co)vertex objects in
C
- w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) self.hom = B.ι.app j
The triangle made from the two natural transformations and
hom
commutes
Instances For
Equations
- CategoryTheory.Limits.inhabitedCoconeMorphism A = { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
Equations
- CategoryTheory.Limits.Cocone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Equations
- CategoryTheory.Limits.Cocones.ext φ w = { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Eta rule for cocones.
Equations
Instances For
Given a cocone morphism whose object part is an isomorphism, produce an isomorphism of cocones.
There is a morphism from a cocone to its extension.
Equations
- CategoryTheory.Limits.Cocones.extend s f = { hom := f, w := ⋯ }
Instances For
Extending a cocone by the identity does nothing.
Equations
Instances For
Extending a cocone by a composition is the same as extending the cone twice.
Equations
- CategoryTheory.Limits.Cocones.extendComp s f g = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.comp f g)).pt) ⋯
Instances For
A cocone extended by an isomorphism is isomorphic to the original cone.
Equations
- CategoryTheory.Limits.Cocones.extendIso s f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Functorially precompose a cocone for F
by a natural transformation G ⟶ F
to give a cocone
for G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Precomposing a cocone by the composite natural transformation α ≫ β
is the same as
precomposing by β
and then by α
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Precomposing by the identity does not change the cocone up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If F
and G
are naturally isomorphic functors, then they have equivalent categories of
cocones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whiskering on the left by E : K ⥤ J
gives a functor from Cocone F
to Cocone (E ⋙ F)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whiskering by an equivalence gives an equivalence between categories of cones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categories of cocones over F
and G
are equivalent if F
and G
are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
Equations
Instances For
Forget the cocone structure and obtain just the cocone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor G : C ⥤ D
sends cocones over F
to cocones over F ⋙ G
functorially.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If e : C ≌ D
is an equivalence of categories, then functoriality F e.functor
induces an
equivalence between cocones over F
and cocones over F ⋙ e.functor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- H.mapCone c = (CategoryTheory.Limits.Cones.functoriality F H).obj c
Instances For
The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.
Equations
- H.mapCocone c = (CategoryTheory.Limits.Cocones.functoriality F H).obj c
Instances For
Given a cone morphism c ⟶ c'
, construct a cone morphism on the mapped cones functorially.
Equations
- H.mapConeMorphism f = (CategoryTheory.Limits.Cones.functoriality F H).map f
Instances For
Given a cocone morphism c ⟶ c'
, construct a cocone morphism on the mapped cocones
functorially.
Equations
- H.mapCoconeMorphism f = (CategoryTheory.Limits.Cocones.functoriality F H).map f
Instances For
If H
is an equivalence, we invert H.mapCone
and get a cone for F
from a cone
for F ⋙ H
.
Equations
- H.mapConeInv c = (CategoryTheory.Limits.Cones.functorialityEquivalence F H.asEquivalence).inverse.obj c
Instances For
mapCone
is the left inverse to mapConeInv
.
Equations
- CategoryTheory.Functor.mapConeMapConeInv H c = (CategoryTheory.Limits.Cones.functorialityEquivalence F H.asEquivalence).counitIso.app c
Instances For
MapCone
is the right inverse to mapConeInv
.
Equations
- CategoryTheory.Functor.mapConeInvMapCone H c = (CategoryTheory.Limits.Cones.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c
Instances For
If H
is an equivalence, we invert H.mapCone
and get a cone for F
from a cone
for F ⋙ H
.
Equations
- H.mapCoconeInv c = (CategoryTheory.Limits.Cocones.functorialityEquivalence F H.asEquivalence).inverse.obj c
Instances For
mapCocone
is the left inverse to mapCoconeInv
.
Equations
- CategoryTheory.Functor.mapCoconeMapCoconeInv H c = (CategoryTheory.Limits.Cocones.functorialityEquivalence F H.asEquivalence).counitIso.app c
Instances For
mapCocone
is the right inverse to mapCoconeInv
.
Equations
- CategoryTheory.Functor.mapCoconeInvMapCocone H c = (CategoryTheory.Limits.Cocones.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c
Instances For
functoriality F _ ⋙ postcompose (whisker_left F _)
simplifies to functoriality F _
.
Equations
- CategoryTheory.Functor.functorialityCompPostcompose α = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cone F) => CategoryTheory.Limits.Cones.ext (α.app c.pt) ⋯) ⋯
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
.
Equations
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.
Equations
- H.mapConePostcompose = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cones.postcompose α).obj c)).pt) ⋯
Instances For
mapCone
commutes with postcomposeEquivalence
Equations
- H.mapConePostcomposeEquivalenceFunctor = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cones.postcomposeEquivalence α).functor.obj c)).pt) ⋯
Instances For
functoriality F _ ⋙ precompose (whiskerLeft F _)
simplifies to functoriality F _
.
Equations
- CategoryTheory.Functor.functorialityCompPrecompose α = CategoryTheory.NatIso.ofComponents (fun (c : CategoryTheory.Limits.Cocone F) => CategoryTheory.Limits.Cocones.ext (α.app c.pt) ⋯) ⋯
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
.
Equations
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.
Equations
- H.mapCoconePrecompose = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocones.precompose α).obj c)).pt) ⋯
Instances For
mapCocone
commutes with precomposeEquivalence
Equations
- H.mapCoconePrecomposeEquivalenceFunctor = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocones.precomposeEquivalence α).functor.obj c)).pt) ⋯
Instances For
Equations
- H.mapConeWhisker = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (H.mapCone (CategoryTheory.Limits.Cone.whisker E c)).pt) ⋯
Instances For
mapCocone
commutes with whisker
Equations
- H.mapCoconeWhisker = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c)).pt) ⋯
Instances For
Change a Cocone F
into a Cone F.op
.
Equations
- c.op = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.op c.ι }
Instances For
Change a Cone F
into a Cocone F.op
.
Equations
- c.op = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.op c.π }
Instances For
Change a Cocone F.op
into a Cone F
.
Equations
- c.unop = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeOp c.ι }
Instances For
Change a Cone F.op
into a Cocone F
.
Equations
- c.unop = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeOp c.π }
Instances For
The category of cocones on F
is equivalent to the opposite category of
the category of cones on the opposite of F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Change a cocone on F.leftOp : Jᵒᵖ ⥤ C
to a cocone on F : J ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.coneOfCoconeLeftOp c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeLeftOp c.ι }
Instances For
Change a cone on F : J ⥤ Cᵒᵖ
to a cocone on F.leftOp : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.coconeLeftOpOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.leftOp c.π }
Instances For
Change a cone on F.leftOp : Jᵒᵖ ⥤ C
to a cocone on F : J ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.coconeOfConeLeftOp c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeLeftOp c.π }
Instances For
Change a cocone on F : J ⥤ Cᵒᵖ
to a cone on F.leftOp : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.coneLeftOpOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.leftOp c.ι }
Instances For
Change a cocone on F.rightOp : J ⥤ Cᵒᵖ
to a cone on F : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.coneOfCoconeRightOp c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeRightOp c.ι }
Instances For
Change a cone on F : Jᵒᵖ ⥤ C
to a cocone on F.rightOp : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.coconeRightOpOfCone c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.rightOp c.π }
Instances For
Change a cone on F.rightOp : J ⥤ Cᵒᵖ
to a cocone on F : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.coconeOfConeRightOp c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeRightOp c.π }
Instances For
Change a cocone on F : Jᵒᵖ ⥤ C
to a cone on F.rightOp : J ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.coneRightOpOfCocone c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.rightOp c.ι }
Instances For
Change a cocone on F.unop : J ⥤ C
into a cone on F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.coneOfCoconeUnop c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeUnop c.ι }
Instances For
Change a cone on F : Jᵒᵖ ⥤ Cᵒᵖ
into a cocone on F.unop : J ⥤ C
.
Equations
- CategoryTheory.Limits.coconeUnopOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.unop c.π }
Instances For
Change a cone on F.unop : J ⥤ C
into a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.coconeOfConeUnop c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeUnop c.π }
Instances For
Change a cocone on F : Jᵒᵖ ⥤ Cᵒᵖ
into a cone on F.unop : J ⥤ C
.
Equations
- CategoryTheory.Limits.coneUnopOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.unop c.ι }
Instances For
The opposite cocone of the image of a cone is the image of the opposite cocone.
Equations
- CategoryTheory.Functor.mapConeOp G t = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (G.mapCone t).op.pt) ⋯
Instances For
The opposite cone of the image of a cocone is the image of the opposite cone.
Equations
- CategoryTheory.Functor.mapCoconeOp G = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (G.mapCocone t).op.pt) ⋯