Idris2Doc : Control.Algebra

# Control.Algebra

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

Fixity Declaration: infixl operator, level 7
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) -> _
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 _ -> ty
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) -> _

Implementations:
AbelianGroupty -> Groupty
GroupHomomorphismab -> Groupa
GroupHomomorphismab -> Groupb
Ringty -> Groupty
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) -> _
MonoidV : Type -> Type
Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:
monoidNeutralIsNeutralL : (l : ty) -> _
monoidNeutralIsNeutralR : (r : ty) -> _

Implementation:
MonoidVty => MonoidV (Identityty)
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
ringOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> _
ringOpIsDistributiveL : (l : ty) -> (c : ty) -> (r : ty) -> _
ringOpIsDistributiveR : (l : ty) -> (c : ty) -> (r : ty) -> _

Implementation:
RingWithUnityty -> Ringty
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) -> _
unityIsRingIdR : (r : ty) -> _

Implementation:
Fieldty -> RingWithUnityty
SemigroupV : Type -> Type
Parameters: ty
Constraints: Semigroup ty
Methods:
semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> _

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