Control.Algebra

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

Fixity Declaration: infixl operator, level 7

interface AbelianGroup : 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

interface Field : 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

interface Group : 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) -> inverse r <+> r = neutral

Implementations:

AbelianGroup ty -> Group ty
GroupHomomorphism a b -> Group a
GroupHomomorphism a b -> Group b
Ring ty -> Group ty

interface GroupHomomorphism : 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) = to x <+> to y

interface MonoidV : Type -> Type

Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:

monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral = l
monoidNeutralIsNeutralR : (r : ty) -> neutral <+> r = r

Implementation:

MonoidV ty => MonoidV (Identity ty)

interface Ring : 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:

RingWithUnity ty -> Ring ty

interface RingWithUnity : 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:

Field ty -> RingWithUnity ty

interface SemigroupV : Type -> Type

Parameters: ty
Constraints: Semigroup ty
Methods:

semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r

Implementation:

SemigroupV ty => SemigroupV (Identity ty)

groupInverseIsInverseR : Group ty => (r : ty) -> inverse r <+> r = neutral

groupOpIsCommutative : AbelianGroup ty => (l : ty) -> (r : ty) -> l <+> r = r <+> l

inverse : Group ty => ty -> ty

inverseM : Field ty => (x : ty) -> Not (x = neutral) -> ty

monoidNeutralIsNeutralL : MonoidV ty => (l : ty) -> l <+> neutral = l

monoidNeutralIsNeutralR : MonoidV ty => (r : ty) -> neutral <+> r = r

ringOpIsAssociative : Ring ty => (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <.> r) = (l <.> c) <.> r

ringOpIsDistributiveL : Ring ty => (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

ringOpIsDistributiveR : Ring ty => (l : ty) -> (c : ty) -> (r : ty) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

semigroupOpIsAssociative : SemigroupV ty => (l : ty) -> (c : ty) -> (r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r

to : GroupHomomorphism a b => a -> b

toGroup : GroupHomomorphism a b => (x : a) -> (y : a) -> to (x <+> y) = to x <+> to y

unity : RingWithUnity ty => ty

unityIsRingIdL : RingWithUnity ty => (l : ty) -> l <.> unity = l

unityIsRingIdR : RingWithUnity ty => (r : ty) -> unity <.> r = r