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

OAlg.Hom.Additive

Contents

Additive
Duality
Proposition

Description

homomorphisms between Additive structures

Synopsis

class (HomFibred h, Transformable (ObjectClass h) Add) => HomAdditive (h :: Type -> Type -> Type)
class (DualisableFibred s o, Transformable s Add) => DualisableAdditive s (o :: Type -> Type)
prpHomAdditive :: (HomAdditive h, Show2 h) => h x y -> XAdd x -> Statement
prpHomAdd1 :: (HomAdditive h, Show2 h) => h a b -> Root a -> Statement
prpHomAdd2 :: (HomAdditive h, Show2 h) => h a b -> Adbl2 a -> Statement
prpDualisableAdditiveAdd1 :: forall s (o :: Type -> Type) q x. DualisableAdditive s o => q o -> Struct s x -> Root x -> Statement
prpDualisableAdditiveAdd2 :: forall s (o :: Type -> Type) q x. DualisableAdditive s o => q o -> Struct s x -> Adbl2 x -> Statement
prpHomDisjOpAdd :: Statement

Additive

class (HomFibred h, Transformable (ObjectClass h) Add) => HomAdditive (h :: Type -> Type -> Type) Source #

type family of homomorphisms between Additive structures.

Property Let h be a type instance of the class HomAdditive, then for all a, b and f in h a b holds:

For all r in Root a holds: amap f (zero r) == zero (rmap f r).
For all x and y in a with root x == root y holds: amap f (x + y) ) == amap f x + amap f y.

Such a h will be called a family of homomorphisms between additive structures and an entity f of h a b a additive homomorphism between a and b.

Instances

Instances details

HomAdditive h => HomAdditive (Inv2 h) Source #
Instance details Defined in OAlg.Hom.Additive
HomAdditive h => HomAdditive (Path h) Source #
Instance details Defined in OAlg.Hom.Additive
(TransformableFbrOrt s, TransformableAdd s) => HomAdditive (Ornt s) Source #
Instance details Defined in OAlg.Data.Ornt
(Semiring r, Commutative r) => HomAdditive (HomSymbol r) Source #
Instance details Defined in OAlg.Entity.Matrix.Vector
(TransformableFbr s, TransformableAdd s) => HomAdditive (HomEmpty s) Source #
Instance details Defined in OAlg.Hom.Additive
(TransformableAdd s, HomAdditive h) => HomAdditive (Sub s h) Source #
Instance details Defined in OAlg.Hom.Additive
(DualisableDistributive s o, TransformableGRefl o s, TransformableGRefl Matrix s, TransformableDst s) => HomAdditive (HomCo Matrix s o) Source #
Instance details Defined in OAlg.Entity.Matrix.Definition
(HomAdditive h, DualisableAdditive s o) => HomAdditive (HomDisj s o h) Source #
Instance details Defined in OAlg.Hom.Additive
(HomAdditive h, Disjunctive2 h) => HomAdditive (Variant2 v h) Source #
Instance details Defined in OAlg.Hom.Additive

Duality

class (DualisableFibred s o, Transformable s Add) => DualisableAdditive s (o :: Type -> Type) Source #

duality according to o on Additive-structures

Properties Let DualisableAdditive s o_ then for all x and s in Struct s x holds:

For all r in Root x holds: toDualStk q s (zero r) == zero (toDualRt q s r),
For all a, b in x with root a == root b holds: toDualStk q s (a + b) == toDualStk q s a + toDualStk q s b.

where q is any proxy for o.

Note Dualisable s Op holds, because + is commutative.

Instances

Instances details

(TransformableType s, TransformableFbrOrt s, TransformableOp s, TransformableAdd s) => DualisableAdditive s Op Source #
Instance details Defined in OAlg.Hom.Additive

Proposition

prpHomAdditive :: (HomAdditive h, Show2 h) => h x y -> XAdd x -> Statement Source #

validity according to HomAdditive.

prpHomAdd1 :: (HomAdditive h, Show2 h) => h a b -> Root a -> Statement Source #

validity according to OAlg.Hom.Additive.

prpHomAdd2 :: (HomAdditive h, Show2 h) => h a b -> Adbl2 a -> Statement Source #

validity according to OAlg.Hom.Additive.

prpDualisableAdditiveAdd1 :: forall s (o :: Type -> Type) q x. DualisableAdditive s o => q o -> Struct s x -> Root x -> Statement Source #

validity according to DualisableAdditive, property 1.

prpDualisableAdditiveAdd2 :: forall s (o :: Type -> Type) q x. DualisableAdditive s o => q o -> Struct s x -> Adbl2 x -> Statement Source #

validity according to DualisableAdditive, property 2.

prpHomDisjOpAdd :: Statement Source #

validity of HomDisjEmpty Add Op according to HomAdditive.