Copyright	Guillaume Sabbagh 2021
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Math.Categories.ConeCategory

Contents

Cone
- Cone construcion
- Helper functions
Cone Morphism
- Helper function
Cone Category
- Helper functions
Cocone
- Cocone construction
- Helper functions
Cocone Morphism
- Helper function
Cocone Category
- Helper functions

Description

Category of Cones of a Diagram.

This module allows to find the (co)limits of a Diagram. Note that the functions limits and colimits scan the entire ConeCategory to find the limits and colimits of a Diagram. It is therefore quite slow, if you work with a Category where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of SetValued and the function colimitOfCompositionGraphs.

Synopsis

type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
cone :: (Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2, FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
unsafeCone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
completeCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
apex :: Cone c1 m1 o1 c2 m2 o2 -> o2
baseCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
legsCone :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
universeCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cone c1 m1 o1 c2 m2 o2 -> c2
indexingCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cone c1 m1 o1 c2 m2 o2 -> c1
precomposeConeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> m2 -> Cone c1 m1 o1 c2 m2 o2
postcomposeConeWithFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3) => Cone c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c3 m3 o3 -> Cone c1 m1 o1 c3 m3 o3
topInjectionsCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cone c1 m1 o1 c3 m3 o3 -> Cone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
bindingMorphismCone :: ConeMorphism c1 m1 o1 c2 m2 o2 -> m2
type ConeCategory c1 m1 o1 c2 m2 o2 = CommaCategory c2 m2 o2 One One One (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
coneCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
limits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
cocone :: (Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2, FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
unsafeCocone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
completeCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
nadir :: Cocone c1 m1 o1 c2 m2 o2 -> o2
baseCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
legsCocone :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
universeCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cocone c1 m1 o1 c2 m2 o2 -> c2
indexingCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cocone c1 m1 o1 c2 m2 o2 -> c1
precomposeCoconeWithFunctor :: (Category c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cocone c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c3 m3 o3
postcomposeCoconeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> m2 -> Cocone c1 m1 o1 c2 m2 o2
bottomInjectionsCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cocone c1 m1 o1 c3 m3 o3 -> Cocone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
bindingMorphismCocone :: CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2
type CoconeCategory c1 m1 o1 c2 m2 o2 = CommaCategory One One One c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
coconeCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
colimits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)

Cone

type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2) Source #

A Cone is a CommaObject in the CommaCategory (D|1_F) where D is the diagonalFunctor and F is the Diagram of interest.

Intuitively, a Cone is an apex, a base and a set of legs indexed by the indexing objects of F such that the legs commute with every arrow in the base of the Cone.

See "Categories for the working mathematician", Saunders Mac Lane, P.67.

Cone construcion

cone :: (Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2, FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2) Source #

Constructs a Cone from an apex and a NaturalTransformation. Return nothing if the source of the NaturalTransformation is not a constant diagram on the apex.

unsafeCone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2 Source #

Constructs a Cone from an apex and a NaturalTransformation. Does NOT check if the source of the NaturalTransformation is a constant diagram on the apex. You may use this function at your own risk, consider using cone if you are not sure.

If you give an incomplete natural transformation to this function, you can use completeCone to complete the natural transformation.

completeCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2 Source #

Given a cone with a partial underlying natural transformation, tries to complete it. You can use 'checkNaturalTransformation.legsCone' to check that the cone was correctly completed.

Helper functions

apex :: Cone c1 m1 o1 c2 m2 o2 -> o2 Source #

Return the apex of a Cone.

baseCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 Source #

Return the base of a Cone.

legsCone :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 Source #

Return the legs of a Cone as a NaturalTransformation.

universeCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cone c1 m1 o1 c2 m2 o2 -> c2 Source #

Return the category in which a Cone lives.

indexingCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cone c1 m1 o1 c2 m2 o2 -> c1 Source #

Return the indexing category of a Cone.

precomposeConeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> m2 -> Cone c1 m1 o1 c2 m2 o2 Source #

Precompose a cone with a morphism going to the apex. (Does not check that the morphism has the apex as target.)

postcomposeConeWithFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3) => Cone c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c3 m3 o3 -> Cone c1 m1 o1 c3 m3 o3 Source #

Postcompose a cone with a functor going from the universe category.

topInjectionsCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cone c1 m1 o1 c3 m3 o3 -> Cone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2) Source #

A Cone c1 is top contained in another Cone c2 if every top leg of c1 is a leg of c2 in an injective manner.

Cone Morphism

type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2) Source #

A ConeMorphism is a morphism binding two Cones. Formally, it is a CommaMorphism in the CommaCategory (D|1_F) where D is the diagonalFunctor and F is the Diagram of interest.

Helper function

bindingMorphismCone :: ConeMorphism c1 m1 o1 c2 m2 o2 -> m2 Source #

Return the binding morphism between the two Cones of a 'ConeMorphism.

Cone Category

type ConeCategory c1 m1 o1 c2 m2 o2 = CommaCategory c2 m2 o2 One One One (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) Source #

A ConeCategory is the category of Cones of a given Diagram, it is a CommaCategory (D|1_F) where D is the diagonalFunctor and F is the Diagram of interest.

Helper functions

coneCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2 Source #

Construct the category of cones of a Diagram.

limits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2) Source #

Returns limits of a diagram (terminal cones).

Note that the functions limits and colimits scan the entire ConeCategory to find the limits and colimits of a Diagram. It is therefore quite slow, if you work with a Category where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of SetValued and the function colimitOfCompositionGraphs.

Cocone

type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2) Source #

A Cocone is a CommaObject in the CommaCategory (1_F|D) where D is the diagonalFunctor and F is the Diagram of interest.

Intuitively, a Cocone is a nadir, a base and a set of legs indexed by the indexing objects of F such that the legs commute with every arrow in the base of the Cocone.

A Cocone is simply the dual of a Cone.

Cocone construction

cocone :: (Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2, FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2) Source #

Constructs a Cocone from a nadir and a NaturalTransformation. Return nothing if the target of the NaturalTransformation is not a constant diagram on the nadir.

unsafeCocone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2 Source #

Constructs a Cocone from a nadir and a NaturalTransformation. Does NOT check if the target of the NaturalTransformation is a constant diagram on the nadir. You may use this function at your own risk, consider using cocone if you are not sure.

If you give an incomplete natural transformation to this function, you can use completeCocone to complete the natural transformation.

completeCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2 Source #

Given a cocone with a partial underlying natural transformation, tries to complete it. You can use 'checkNaturalTransformation.legsCocone' to check that the cocone was correctly completed.

Helper functions

nadir :: Cocone c1 m1 o1 c2 m2 o2 -> o2 Source #

Return the nadir of a Cocone.

baseCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 Source #

Return the base of a Cocone.

legsCocone :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 Source #

Return the legs of a Cocone as a NaturalTransformation.

universeCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cocone c1 m1 o1 c2 m2 o2 -> c2 Source #

Return the category in which a Cocone lives.

indexingCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Cocone c1 m1 o1 c2 m2 o2 -> c1 Source #

Return the indexing category of a Cocone.

precomposeCoconeWithFunctor :: (Category c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cocone c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c3 m3 o3 Source #

postcomposeCoconeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Category c2 m2 o2, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> m2 -> Cocone c1 m1 o1 c2 m2 o2 Source #

Postcompose a cone with a morphism going from the nadir. (Does not check that the morphism has the nadir as source.)

bottomInjectionsCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) => Cocone c1 m1 o1 c3 m3 o3 -> Cocone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2) Source #

A Cocone c1 is bottom contained in another Cocone c2 if every bottom leg of c1 is a leg of c2 in an injective manner.

Cocone Morphism

type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2) Source #

A CoconeMorphism is a morphism binding two Cocones. Formally, it is a CommaMorphism in the CommaCategory (1_F|D) where D is the diagonalFunctor and F is the Diagram of interest.

Helper function

bindingMorphismCocone :: CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2 Source #

Return the binding morphism between the two Cocones of a 'CoconeMorphism.

Cocone Category

type CoconeCategory c1 m1 o1 c2 m2 o2 = CommaCategory One One One c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) Source #

A CoconeCategory is the category of Cocones of a given Diagram, it is a CommaCategory (1_F|D) where D is the diagonalFunctor and F is the Diagram of interest.

Helper functions

coconeCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2 Source #

Construct the category of cocones of a Diagram.

colimits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2) Source #

Returns colimits of a diagram (initial cocones).

Note that the functions limits and colimits scan the entire ConeCategory to find the limits and colimits of a Diagram. It is therefore quite slow, if you work with a Category where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of SetValued and the function colimitOfCompositionGraphs.