| Copyright | Guillaume Sabbagh 2022 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Math.FiniteCategories.Subcategory
Description
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.
Synopsis
- data Subcategory c m o
- unsafeSubcategory :: c -> Set o -> Set m -> Subcategory c m o
- 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)
- originalCategory :: Subcategory c m o -> c
- embeddingToSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
- 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
- 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
- data InheritedSubcategory c m o
- unsafeInheritedSubcategory :: c -> Set o -> Set m -> InheritedSubcategory c m o
- 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)
- originalCategory2 :: InheritedSubcategory c m o -> c
- embeddingToInheritedSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
- 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
- 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
Subcategory
data Subcategory c m o Source #
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) Source # | |
Defined in Math.FiniteCategories.Subcategory Methods pprint :: Int -> Subcategory c m o -> String Source # pprintWithIndentations :: Int -> Int -> String -> Subcategory c m o -> String Source # pprintIndent :: Int -> Subcategory c m o -> String Source # | |
| (Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) => Simplifiable (Subcategory c m o) Source # | |
Defined in Math.FiniteCategories.Subcategory Methods simplify :: Subcategory c m o -> Subcategory c m o # | |
| Generic (Subcategory c m o) Source # | |
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) Source # | |
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) Source # | |
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 Source # | |
Defined in Math.FiniteCategories.Subcategory Methods identity :: Subcategory c m o -> o -> m Source # ar :: Subcategory c m o -> o -> o -> Set m Source # genAr :: Subcategory c m o -> o -> o -> Set m Source # decompose :: Subcategory c m o -> m -> [m] Source # | |
| (Category c m o, Eq o, Eq m) => FiniteCategory (Subcategory c m o) m o Source # | |
Defined in Math.FiniteCategories.Subcategory Methods ob :: Subcategory c m o -> Set o Source # | |
| type Rep (Subcategory c m o) Source # | |
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 Source #
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) Source #
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 Source #
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 Source #
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 Source #
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 Source #
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 Source #
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) Source # | |
Defined in Math.FiniteCategories.Subcategory Methods pprint :: Int -> InheritedSubcategory c m o -> String Source # pprintWithIndentations :: Int -> Int -> String -> InheritedSubcategory c m o -> String Source # pprintIndent :: Int -> InheritedSubcategory c m o -> String Source # | |
| (Simplifiable c, Simplifiable o, Simplifiable m, Eq o, Eq m) => Simplifiable (InheritedSubcategory c m o) Source # | |
Defined in Math.FiniteCategories.Subcategory Methods simplify :: InheritedSubcategory c m o -> InheritedSubcategory c m o # | |
| Generic (InheritedSubcategory c m o) Source # | |
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) Source # | |
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) Source # | |
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 Source # | |
Defined in Math.FiniteCategories.Subcategory Methods identity :: InheritedSubcategory c m o -> o -> m Source # ar :: InheritedSubcategory c m o -> o -> o -> Set m Source # genAr :: InheritedSubcategory c m o -> o -> o -> Set m Source # decompose :: InheritedSubcategory c m o -> m -> [m] Source # | |
| (Category c m o, Eq o, Eq m) => FiniteCategory (InheritedSubcategory c m o) m o Source # | |
Defined in Math.FiniteCategories.Subcategory Methods ob :: InheritedSubcategory c m o -> Set o Source # | |
| type Rep (InheritedSubcategory c m o) Source # | |
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 Source #
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) Source #
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 Source #
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 Source #
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 Source #
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 Source #
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.