Idris2Doc : Control.Algebra

# Control.Algebra

(<.>) : Ringty => ty -> ty -> ty

Fixity Declaration: infixl operator, level 7
interfaceAbelianGroup : Type -> Type
`  Sets equipped with a single binary operation that is associative  and commutative, along with a neutral element for that binary  operation and inverses for all elements. Satisfies the following  laws:    + Associativity of `<+>`:  forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:  forall a b, a <+> b == b <+> a  + Neutral for `<+>`:  forall a, a <+> neutral == a  forall a, neutral <+> a == a  + Inverse for `<+>`:  forall a, a <+> inverse a == neutral  forall a, inverse a <+> a == neutral`

Parameters: ty
Constraints: Group ty
Methods:
groupOpIsCommutative : (l : ty) -> (r : ty) -> l<+>r = r<+>l
interfaceField : Type -> Type
`  Sets equipped with two binary operations – both associative,  commutative and possessing a neutral element – and distributivity  laws relating the two operations. All elements except the additive  identity should have a multiplicative inverse. Should (but may  not) satisfy the following laws:    + Associativity of `<+>`:  forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:  forall a b, a <+> b == b <+> a  + Neutral for `<+>`:  forall a, a <+> neutral == a  forall a, neutral <+> a == a  + Inverse for `<+>`:  forall a, a <+> inverse a == neutral  forall a, inverse a <+> a == neutral  + Associativity of `<.>`:  forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Unity for `<.>`:  forall a, a <.> unity == a  forall a, unity <.> a == a  + InverseM of `<.>`, except for neutral  forall a /= neutral, a <.> inverseM a == unity  forall a /= neutral, inverseM a <.> a == unity  + Distributivity of `<.>` and `<+>`:  forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)  forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: RingWithUnity ty
Methods:
inverseM : (x : ty) -> Not (x = neutral) -> ty
interfaceGroup : Type -> Type
`  Sets equipped with a single binary operation that is associative,  along with a neutral element for that binary operation and  inverses for all elements. Satisfies the following laws:    + Associativity of `<+>`:  forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Neutral for `<+>`:  forall a, a <+> neutral == a  forall a, neutral <+> a == a  + Inverse for `<+>`:  forall a, a <+> inverse a == neutral  forall a, inverse a <+> a == neutral`

Parameters: ty
Constraints: MonoidV ty
Methods:
inverse : ty -> ty
groupInverseIsInverseR : (r : ty) -> inverser<+>r = neutral

Implementations:
AbelianGroupty -> Groupty
GroupHomomorphismab -> Groupa
GroupHomomorphismab -> Groupb
Ringty -> Groupty
interfaceGroupHomomorphism : Type -> Type -> Type
`  A homomorphism is a mapping that preserves group structure.`

Parameters: a, b
Constraints: Group a, Group b
Methods:
to : a -> b
toGroup : (x : a) -> (y : a) -> to (x<+>y) = tox<+>toy
interfaceMonoidV : Type -> Type
Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:
monoidNeutralIsNeutralL : (l : ty) -> l<+>neutral = l
monoidNeutralIsNeutralR : (r : ty) -> neutral<+>r = r

Implementation:
MonoidVty => MonoidV (Identityty)
interfaceRing : Type -> Type
`  Sets equipped with two binary operations, one associative and  commutative supplied with a neutral element, and the other  associative, with distributivity laws relating the two operations.  Satisfies the following laws:    + Associativity of `<+>`:  forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:  forall a b, a <+> b == b <+> a  + Neutral for `<+>`:  forall a, a <+> neutral == a  forall a, neutral <+> a == a  + Inverse for `<+>`:  forall a, a <+> inverse a == neutral  forall a, inverse a <+> a == neutral  + Associativity of `<.>`:  forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Distributivity of `<.>` and `<+>`:  forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)  forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: Group ty
Methods:
(<.>) : ty -> ty -> ty
Fixity Declaration: infixl operator, level 7
ringOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<.>r) = (l<.>c) <.>r
ringOpIsDistributiveL : (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<+>r) = (l<.>c) <+> (l<.>r)
ringOpIsDistributiveR : (l : ty) -> (c : ty) -> (r : ty) -> (l<+>c) <.>r = (l<.>r) <+> (c<.>r)

Implementation:
RingWithUnityty -> Ringty
interfaceRingWithUnity : Type -> Type
`  Sets equipped with two binary operations, one associative and  commutative supplied with a neutral element, and the other  associative supplied with a neutral element, with distributivity  laws relating the two operations. Satisfies the following laws:    + Associativity of `<+>`:  forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:  forall a b, a <+> b == b <+> a  + Neutral for `<+>`:  forall a, a <+> neutral == a  forall a, neutral <+> a == a  + Inverse for `<+>`:  forall a, a <+> inverse a == neutral  forall a, inverse a <+> a == neutral  + Associativity of `<.>`:  forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Neutral for `<.>`:  forall a, a <.> unity == a  forall a, unity <.> a == a  + Distributivity of `<.>` and `<+>`:  forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)  forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: Ring ty
Methods:
unity : ty
unityIsRingIdL : (l : ty) -> l<.>unity = l
unityIsRingIdR : (r : ty) -> unity<.>r = r

Implementation:
Fieldty -> RingWithUnityty
interfaceSemigroupV : Type -> Type
Parameters: ty
Constraints: Semigroup ty
Methods:
semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l<+> (c<+>r) = (l<+>c) <+>r

Implementation:
SemigroupVty => SemigroupV (Identityty)
groupInverseIsInverseR : Groupty => (r : ty) -> inverser<+>r = neutral
groupOpIsCommutative : AbelianGroupty => (l : ty) -> (r : ty) -> l<+>r = r<+>l
inverse : Groupty => ty -> ty
inverseM : Fieldty => (x : ty) -> Not (x = neutral) -> ty
monoidNeutralIsNeutralL : MonoidVty => (l : ty) -> l<+>neutral = l
monoidNeutralIsNeutralR : MonoidVty => (r : ty) -> neutral<+>r = r
ringOpIsAssociative : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<.>r) = (l<.>c) <.>r
ringOpIsDistributiveL : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<+>r) = (l<.>c) <+> (l<.>r)
ringOpIsDistributiveR : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> (l<+>c) <.>r = (l<.>r) <+> (c<.>r)
semigroupOpIsAssociative : SemigroupVty => (l : ty) -> (c : ty) -> (r : ty) -> l<+> (c<+>r) = (l<+>c) <+>r
to : GroupHomomorphismab => a -> b
toGroup : GroupHomomorphismab => (x : a) -> (y : a) -> to (x<+>y) = tox<+>toy
unity : RingWithUnityty => ty
unityIsRingIdL : RingWithUnityty => (l : ty) -> l<.>unity = l
unityIsRingIdR : RingWithUnityty => (r : ty) -> unity<.>r = r