Math.FiniteCategories.Subcategory

A Subcategory of a category C is a category D whose objects are objects in C and whose morphisms are morphisms in C with the same identities and composition of morphisms.

We have to forget the generating set of morphisms of the original Category as the generators are not always inheritable (see for example the full subcategory of Square containing the objects A and D).

If the generators are inheritable, you can use the constructor InheritedSubcategory to inherit the generators of the original Category.

Subcategory

data Subcategory c m o

A Subcategory needs an original category, a set of objects and a set of morphisms selected in the category.

The generators are forgotten, use InheritedSubcategory if the generators are inheritable.

Subcategory is private because the subset of morphisms might not yield a valid FiniteCategory if a composite morphism does not belong in the subset.

Use the smart constructor subcategory instead.

Instances

(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) => PrettyPrint (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

pprint :: Int -> Subcategory c m o -> String

pprintWithIndentations :: Int -> Int -> String -> Subcategory c m o -> String

pprintIndent :: Int -> Subcategory c m o -> String

(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) => Simplifiable (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

simplify :: Subcategory c m o -> Subcategory c m o

Generic (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Associated Types

type Rep (Subcategory c m o) :: Type -> Type

Methods

from :: Subcategory c m o -> Rep (Subcategory c m o) x

to :: Rep (Subcategory c m o) x -> Subcategory c m o

(Show c, Show m, Show o) => Show (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

showsPrec :: Int -> Subcategory c m o -> ShowS

show :: Subcategory c m o -> String

showList :: [Subcategory c m o] -> ShowS

(Eq c, Eq o, Eq m) => Eq (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

(==) :: Subcategory c m o -> Subcategory c m o -> Bool

(/=) :: Subcategory c m o -> Subcategory c m o -> Bool

(Category c m o, Eq o, Eq m) => Category (Subcategory c m o) m o

Defined in Math.FiniteCategories.Subcategory

Methods

identity :: Subcategory c m o -> o -> m

ar :: Subcategory c m o -> o -> o -> Set m

genAr :: Subcategory c m o -> o -> o -> Set m

decompose :: Subcategory c m o -> m -> [m]

(Category c m o, Eq o, Eq m) => FiniteCategory (Subcategory c m o) m o

Defined in Math.FiniteCategories.Subcategory

Methods

ob :: Subcategory c m o -> Set o

type Rep (Subcategory c m o)

Defined in Math.FiniteCategories.Subcategory

type Rep (Subcategory c m o) = D1 ('MetaData "Subcategory" "Math.FiniteCategories.Subcategory" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "Subcategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set o)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set m)))))

Smart constructors

unsafeSubcategory :: c -> Set o -> Set m -> Subcategory c m o

Unsafe version of subcategory which does not check the structure of the Subcategory constructed.

subcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m -> Either (FiniteCategoryError m o) (Subcategory c m o)

Smart constructor of Subcategory.

If the Subcategory constructed is valid, return Right the subcategory, otherwise return Left a FiniteCategoryError.

Getter

originalCategory :: Subcategory c m o -> c

Return the original category the Subcategory was taken from.

Interaction with Diagram

embeddingToSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2

Return the image Subcategory of an embedding.

An embedding is a faithful Diagram injective on objects.

Does not check that the Diagram is an embedding.

fullDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2

Extracts a full and faithful diagram out of a faithful Diagram injective on objects.

Does not check that the Diagram is an embedding.

fullNaturalTransformation :: (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) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (Subcategory c2 m2 o2) m2 o2

Extracts full and faithful diagrams out of the source and target Diagrams of a NaturalTransformation. The Diagrams should be a faithful and injective on objects.

Does not check that the Diagrams are embeddings.

InheritedSubcategory

data InheritedSubcategory c m o

An InheritedSubcategory needs an original category, a set of objects and a set of morphisms selected in the category.

The generators are inherited.

InheritedSubcategory is private because the subset of morphisms might not yield a valid FiniteCategory if a composite morphism does not belong in the subset.

Use the smart constructor inheritedSubcategory instead.

Instances

(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) => PrettyPrint (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

pprint :: Int -> InheritedSubcategory c m o -> String

pprintWithIndentations :: Int -> Int -> String -> InheritedSubcategory c m o -> String

pprintIndent :: Int -> InheritedSubcategory c m o -> String

(Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) => Simplifiable (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

simplify :: InheritedSubcategory c m o -> InheritedSubcategory c m o

Generic (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Associated Types

type Rep (InheritedSubcategory c m o) :: Type -> Type

Methods

from :: InheritedSubcategory c m o -> Rep (InheritedSubcategory c m o) x

to :: Rep (InheritedSubcategory c m o) x -> InheritedSubcategory c m o

(Show c, Show m, Show o) => Show (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

showsPrec :: Int -> InheritedSubcategory c m o -> ShowS

show :: InheritedSubcategory c m o -> String

showList :: [InheritedSubcategory c m o] -> ShowS

(Eq c, Eq o, Eq m) => Eq (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

Methods

(==) :: InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool

(/=) :: InheritedSubcategory c m o -> InheritedSubcategory c m o -> Bool

(Category c m o, Eq o, Eq m) => Category (InheritedSubcategory c m o) m o

Defined in Math.FiniteCategories.Subcategory

Methods

identity :: InheritedSubcategory c m o -> o -> m

ar :: InheritedSubcategory c m o -> o -> o -> Set m

genAr :: InheritedSubcategory c m o -> o -> o -> Set m

decompose :: InheritedSubcategory c m o -> m -> [m]

(Category c m o, Eq o, Eq m) => FiniteCategory (InheritedSubcategory c m o) m o

Defined in Math.FiniteCategories.Subcategory

Methods

ob :: InheritedSubcategory c m o -> Set o

type Rep (InheritedSubcategory c m o)

Defined in Math.FiniteCategories.Subcategory

type Rep (InheritedSubcategory c m o) = D1 ('MetaData "InheritedSubcategory" "Math.FiniteCategories.Subcategory" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "InheritedSubcategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set o)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set m)))))

Smart constructors

unsafeInheritedSubcategory :: c -> Set o -> Set m -> InheritedSubcategory c m o

Unsafe version of inheritedSubcategory which does not check the structure of the InheritedSubcategory constructed.

inheritedSubcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m -> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)

Smart constructor of InheritedSubcategory.

If the InheritedSubcategory constructed is valid, return Right the subcategory, otherwise return Left a FiniteCategoryError.

Getter

originalCategory2 :: InheritedSubcategory c m o -> c

Return the original category the InheritedSubcategory was taken from.

Interaction with Diagram

embeddingToInheritedSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2

Return the image InheritedSubcategory of an embedding.

An embedding is a faithful Diagram injective on objects.

Does not check that the Diagram is an embedding.

fullDiagram2 :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2

Extracts a full and faithful diagram out of a faithful Diagram injective on objects. The target subcategory is inherited (see InheritedFullSubcategory).

Does not check that the Diagram is an embedding.

fullNaturalTransformation2 :: (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) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2

Extracts full and faithful diagrams out of the source and target Diagrams of a NaturalTransformation. The Diagrams should be a faithful and injective on objects. The target subcategory is inherited (see InheritedFullSubcategory).

Does not check that the Diagrams are embeddings.