| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
OAlg.Hom.Multiplicative.Definition
Contents
Description
definition of homomorphisms between Multiplicative structures.
Synopsis
- class (EmbeddableMorphism h Mlt, HomOriented h) => HomMultiplicative h
- type IsoMultiplicative h = (FunctorialHomOriented h, Cayleyan2 h, HomMultiplicative h)
- isoFromOpOpMlt :: Multiplicative a => IsoOp Mlt (Op (Op a)) a
- isoOppositeMlt :: Entity p => IsoOp Mlt (Op (Orientation p)) (Orientation p)
Multiplicative
class (EmbeddableMorphism h Mlt, HomOriented h) => HomMultiplicative h Source #
type family of homomorphisms between Multiplicative structures.
Propoerty Let h be a type instance of the class HomMultiplicative, then
for all a, b and f in h a b holds:
- For all
pinPointaamapf (onep)==one(pmapf p) - For all
x,yinawithstartx==endyamapf (x*y)==amapf x*amapf y
Such a h will be called a
family of homomorphisms between multiplicative structures and an entity f of
h a b a multiplicative homomorphism between a and
b.
Note If we interpret the types a and b as small categories (see note at
Multiplicative) then we can interpret the type family h as a family of covariant
functors.
Instances
type IsoMultiplicative h = (FunctorialHomOriented h, Cayleyan2 h, HomMultiplicative h) Source #
isomorphisms between Multiplicative structures.
OpHom
isoFromOpOpMlt :: Multiplicative a => IsoOp Mlt (Op (Op a)) a Source #
the induced isomorphism of Multiplicative structures given by FromOpOp.
isoOppositeMlt :: Entity p => IsoOp Mlt (Op (Orientation p)) (Orientation p) Source #