OAlg.Hom.Additive

homomorphisms between Additive structures

Additive

class (EmbeddableMorphism h Add, HomFibred h) => HomAdditive h

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:

1. For all r in Root a holds: amap f (zero r) == zero (rmap f r).
2. 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

HomAdditive h => HomAdditive (Path h)

Defined in OAlg.Hom.Additive

(Semiring r, Commutative r) => HomAdditive (HomSymbol r)

Defined in OAlg.Entity.Matrix.Vector

(TransformableOp s, ForgetfulFbrOrt s, ForgetfulAdd s, ForgetfulTyp s, Typeable s) => HomAdditive (HomOp s)

Defined in OAlg.Hom.Additive

(ForgetfulAdd s, ForgetfulTyp s, Typeable s) => HomAdditive (IdHom s)

Defined in OAlg.Hom.Additive

(TransformableOp s, ForgetfulFbrOrt s, ForgetfulAdd s, ForgetfulTyp s, Typeable s) => HomAdditive (IsoOp s)

Defined in OAlg.Hom.Additive

(HomAdditive h, HomFibredOriented h) => HomAdditive (OpHom h)

Defined in OAlg.Hom.Additive

(TransformableOp s, ForgetfulDst s, ForgetfulTyp s, Typeable s) => HomAdditive (IsoOpMap Matrix s)

Defined in OAlg.Entity.Matrix.Definition

(TransformableOp s, ForgetfulDst s, ForgetfulTyp s, Typeable s) => HomAdditive (OpMap Matrix s)

Defined in OAlg.Entity.Matrix.Definition

Proposition

prpHomAdd1 :: HomAdditive h => h a b -> Root a -> Statement

validity according to OAlg.Hom.Additive.

prpHomAdd2 :: HomAdditive h => h a b -> Adbl2 a -> Statement

validity according to OAlg.Hom.Additive.