Control.Algebra

Definitions

interface SemigroupV : Type -> Type

Parameters: ty
Constraints: Semigroup ty
Methods:

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

Implementations:

SemigroupV ty => SemigroupV (Identity ty)

SemigroupV ty => SemigroupV (Identity ty)

semigroupOpIsAssociative : {auto __con : SemigroupV ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r

Visibility: public export

interface MonoidV : Type -> Type

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

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

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

Implementations:

MonoidV ty => MonoidV (Identity ty)

MonoidV ty => MonoidV (Identity ty)

monoidNeutralIsNeutralL : {auto __con : MonoidV ty} -> (l : ty) -> l <+> neutral = l

Visibility: public export

monoidNeutralIsNeutralR : {auto __con : MonoidV ty} -> (r : ty) -> neutral <+> r = r

Visibility: public export

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

inverse : Group ty => ty -> ty

Visibility: public export

groupInverseIsInverseR : {auto __con : Group ty} -> (r : ty) -> inverse r <+> r = neutral

Visibility: public export

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

groupOpIsCommutative : {auto __con : AbelianGroup ty} -> (l : ty) -> (r : ty) -> l <+> r = r <+> l

Visibility: public export

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

to : GroupHomomorphism a b => a -> b

Visibility: public export

toGroup : {auto __con : GroupHomomorphism a b} -> (x : a) -> (y : a) -> to (x <+> y) = to x <+> to y

Visibility: public export

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

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

Visibility: public export
Fixity Declaration: infixl operator, level 7

ringOpIsAssociative : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <.> r) = (l <.> c) <.> r

Visibility: public export

ringOpIsDistributiveL : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

Visibility: public export

ringOpIsDistributiveR : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

Visibility: public export

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

unity : RingWithUnity ty => ty

Visibility: public export

unityIsRingIdL : {auto __con : RingWithUnity ty} -> (l : ty) -> l <.> unity = l

Visibility: public export

unityIsRingIdR : {auto __con : RingWithUnity ty} -> (r : ty) -> unity <.> r = r

Visibility: public export

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

inverseM : {auto __con : Field ty} -> (x : ty) -> Not (x = neutral) -> ty

Visibility: public export