Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Hom.Multiplicative

Contents

Disjunctive
Covariant
Dualisable
X
Proposition

Description

definition of homomorphisms between Multiplicative structures.

Synopsis

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) Mlt) => HomMultiplicativeDisjunctive (h :: Type -> Type -> Type)
toDualOpMlt :: Multiplicative x => Variant2 'Contravariant (IsoO Mlt Op) x (Op x)
homDisjOpMlt :: HomMultiplicative h => h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
class (HomOriented h, Transformable (ObjectClass h) Mlt) => HomMultiplicative (h :: Type -> Type -> Type)
class (DualisableOriented s o, Transformable s Mlt) => DualisableMultiplicative s (o :: Type -> Type)
data XHomMlt x
xMltHomMlt :: XMlt x -> XHomMlt x
xosHomMlt :: forall x (d :: Site). Multiplicative x => XOrtSite d x -> XHomMlt x
prpHomMultiplicativeDisjunctive :: HomMultiplicativeDisjunctive h => h x y -> XHomMlt x -> Statement
prpHomMultiplicative :: HomMultiplicative h => h x y -> XHomMlt x -> Statement
prpHomDisjMultiplicative :: forall (h :: Type -> Type -> Type) s (o :: Type -> Type) x y. (HomMultiplicative h, DualisableMultiplicative s o) => Struct MltX x -> HomDisj s o h x y -> Statement
prpHomDisjOpMlt :: Statement
prpDualisableMultiplicativeOne :: forall s (o :: Type -> Type) q x. DualisableMultiplicative s o => q o -> Struct s x -> X (Point x) -> Statement
prpDualisableMultiplicativeMlt :: forall s (o :: Type -> Type) q x. DualisableMultiplicative s o => q o -> Struct s x -> X (Mltp2 x) -> Statement
relMapMltOne :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> (Point x -> Point y) -> X (Point x) -> Statement
relMapMltCov :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCnt :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement

Disjunctive

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) Mlt) => HomMultiplicativeDisjunctive (h :: Type -> Type -> Type) Source #

disjunctive family of homomorphisms between Multiplicative structures.

Propoerty Let HomMultiplicativeDisjunctive h, then for all a, b and h in h a b holds:

If variant2 h == Covariant then holds:
1. For all p in Point a holds: amap h (one p) == one (pmap h p).
2. For all x, y in a with start x == end y holds: amap h (x * y) == amap h x * amap h y.
If variant2 h == Contravariant then holds:
1. For all p in Point a holds: amap h (one p) == one (pmap h p).
2. For all x, y in a with start x == end y holds: amap h (x * y) == amap h y * amap h x.

Instances

Instances details

(CategoryDisjunctive h, HomMultiplicativeDisjunctive h) => HomMultiplicativeDisjunctive (Inv2 h) Source #
Instance details Defined in OAlg.Hom.Multiplicative
(TransformableMlt s, HomMultiplicativeDisjunctive h) => HomMultiplicativeDisjunctive (Sub s h) Source #
Instance details Defined in OAlg.Hom.Multiplicative
(DualisableDistributive s o, TransformableGRefl o s, TransformableGRefl Matrix s, TransformableDst s) => HomMultiplicativeDisjunctive (HomCo Matrix s o) Source #
Instance details Defined in OAlg.Entity.Matrix.Definition
(HomMultiplicative h, DualisableMultiplicative s o) => HomMultiplicativeDisjunctive (HomDisj s o h) Source #
Instance details Defined in OAlg.Hom.Multiplicative

toDualOpMlt :: Multiplicative x => Variant2 'Contravariant (IsoO Mlt Op) x (Op x) Source #

the canonical Contravariant isomorphism on Multiplicative structures between x and Op x.

homDisjOpMlt :: HomMultiplicative h => h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y Source #

embedding a multiplicative homomorphism into a covariant HomDisj Mlt Op.

Covariant

class (HomOriented h, Transformable (ObjectClass h) Mlt) => HomMultiplicative (h :: Type -> Type -> Type) Source #

covariant family of homomorphisms between Multiplicative structures.

Propoerty Let HomMultiplicative h, then for all a, b and h in h a b holds:

For all p in Point a holds: amap h (one p) == one (pmap h p).
For all x, y in a with start x == end y holds: amaph (x * y) == amap h x * amap h y.

Instances

Instances details

HomMultiplicative GLApp Source #
Instance details Defined in OAlg.Entity.Matrix.GeneralLinearGroup
HomMultiplicative h => HomMultiplicative (Inv2 h) Source #
Instance details Defined in OAlg.Hom.Multiplicative
HomMultiplicative h => HomMultiplicative (Path h) Source #
Instance details Defined in OAlg.Hom.Multiplicative
TransformableMlt s => HomMultiplicative (Ornt s) Source #
Instance details Defined in OAlg.Data.Ornt
HomMultiplicative (SliceFactorDrop s) Source #
Instance details Defined in OAlg.Entity.Slice.Definition
TransformableMlt s => HomMultiplicative (HomEmpty s) Source #
Instance details Defined in OAlg.Hom.Multiplicative
(Distributive d, Sliced i d, Conic c) => HomMultiplicative (SliceAdjunction i c d) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
HomMultiplicativeDisjunctive h => HomMultiplicative (Variant2 'Covariant h) Source #
Instance details Defined in OAlg.Hom.Multiplicative

Dualisable

class (DualisableOriented s o, Transformable s Mlt) => DualisableMultiplicative s (o :: Type -> Type) Source #

duality according to o on s-structured Multiplicative types,

Properties Let DualisableMultiplicative o s then for all x and s in Struct s x holds:

For all p in Point x holds: toDualArw q s (one p) == one (toDualPnt q s p).
For all x, y in x with start x == end y holds: toDualArw q s (x * y) == toDualArw q s y * toDualArw q s x.

where q is any proxy for o.

Instances

Instances details

(TransformableOrt s, TransformableMlt s, TransformableOp s, TransformableType s) => DualisableMultiplicative s Op Source #
Instance details Defined in OAlg.Hom.Multiplicative

X

data XHomMlt x Source #

random variable for testing multiplicative homomorphisms.

xMltHomMlt :: XMlt x -> XHomMlt x Source #

the underlying XHomMlt.

xosHomMlt :: forall x (d :: Site). Multiplicative x => XOrtSite d x -> XHomMlt x Source #

the XHomMlt given by a XOrtSite d

Proposition

prpHomMultiplicativeDisjunctive :: HomMultiplicativeDisjunctive h => h x y -> XHomMlt x -> Statement Source #

validity according to HomMultiplicativeDisjunctive.

prpHomMultiplicative :: HomMultiplicative h => h x y -> XHomMlt x -> Statement Source #

validity according to HomMultiplicative.

prpHomDisjMultiplicative :: forall (h :: Type -> Type -> Type) s (o :: Type -> Type) x y. (HomMultiplicative h, DualisableMultiplicative s o) => Struct MltX x -> HomDisj s o h x y -> Statement Source #

validity according to HomMultiplicativeDisjunctive.

prpHomDisjOpMlt :: Statement Source #

validity for HomDisjEmpty MltX Op beeing HomMultiplicativeDisjunctive.

prpDualisableMultiplicativeOne :: forall s (o :: Type -> Type) q x. DualisableMultiplicative s o => q o -> Struct s x -> X (Point x) -> Statement Source #

validity according to DualisableMultiplicative, property 1.

prpDualisableMultiplicativeMlt :: forall s (o :: Type -> Type) q x. DualisableMultiplicative s o => q o -> Struct s x -> X (Mltp2 x) -> Statement Source #

validity according to DualisableMultiplicative, property 2.

relMapMltOne :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> (Point x -> Point y) -> X (Point x) -> Statement Source #

validity that one maps to one according to the given mapplings.

relMapMltCov :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement Source #

validity of * as covariant operation according to the given mapping.

relMapMltCnt :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement Source #

validity of * as contravariant operation according to the given mapping.