10/07/2019, 23:33
record Semigroup (a : Set) : Set where
field
_o_ : a → a → a
assoc : ∀ a b c → (a o b) o c ≡ a o (b o c)
record Monoid (a : Set) : Set where
field
semigroup : Semigroup a
open Semigroup semigroup
field
z : a
lId : ∀ x → z o x ≡ x
rId : ∀ x → x o z ≡ x
record Semiring (a : Set) : Set where
field
monoid : Monoid a
semigroup : Semigroup a
field
_⊕_ : a → a → a
_o_ : a → a → a
12/07/2019, 23:27
module MyAlgebra where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
-- properties
Commutative :
∀ {a} →
(a → a → a) → Set
Commutative f =
∀ x → ∀ y → f x y ≡ f y x
Associative :
∀ {a} →
(a → a → a) → Set
Associative f =
∀ x y z → f (f x y) z ≡ f x (f y z)
_distributesOver_ :
∀ {a} →
(a → a → a) →
(a → a → a) → Set
f distributesOver g =
∀ a b c → f a (g b c) ≡ g (f a b) (f a c)
-- structures
record IsSemigroup
(a : Set)
(_o_ : a → a → a) : Set where
field
assoc : Associative (_o_)
record Semigroup : Set₁ where
field
a : Set
_o_ : a → a → a
isSemigroup : IsSemigroup a (_o_)
record HasIdentity
(a : Set)
(_o_ : a → a → a)
(z : a) : Set where
field
lId : ∀ a → z o a ≡ a
rId : ∀ a → a o z ≡ a
record HasInverses
(a : Set)
(_o_ : a → a → a)
(z : a)
(inv : a → a) : Set where
field
rInv : ∀ x → x o (inv x) ≡ z
lInv : ∀ x → (inv x) o x ≡ z
record IsMonoid
(a : Set)
(_o_ : a → a → a)
(z : a) : Set where
field
isSemigroup : IsSemigroup a (_o_)
hasIdentity : HasIdentity a (_o_) z
record IsGroup
(a : Set)
(_o_ : a → a → a)
(z : a)
(i : a → a) : Set where
field
isMonoid : IsMonoid a (_o_) z
hasInverses : HasInverses a (_o_) z i
record IsAbelianMonoid
(a : Set)
(_o_ : a → a → a)
(z : a) : Set where
field
isMonoid : IsMonoid a (_o_) z
isAbelian : Commutative (_o_)
record IsAbelianGroup
(a : Set)
(_o_ : a → a → a)
(z : a)
(i : a → a) : Set where
field
isGroup : IsGroup a (_o_) z i
isCommutativeCirc : Commutative (_o_)
record IsRing
(a : Set)
(_o_ : a → a → a)
(_⊕_ : a → a → a)
(z : a)
(i : a → a) : Set where
field
isAbelianGroup : IsAbelianGroup a (_o_) z i
isMonoid : IsMonoid a (_o_) z
isRing : (_o_) distributesOver (_⊕_)
record IsUnitaryRing
(a : Set)
(_o_ : a → a → a)
(_⊕_ : a → a → a)
(z : a)
(i : a → a)
(u : a) : Set where
field
isRing : IsRing a (_o_) (_⊕_) z i
isUnitary : IsMonoid a (_o_) u
record IsCommutativeRing
(a : Set)
(_o_ : a → a → a)
(_⊕_ : a → a → a)
(z : a)
(i : a → a)
(u : a) : Set where
field
isUnitaryRing : IsUnitaryRing a (_o_) (_⊕_) z i u
isCommutativeCirc : IsAbelianMonoid a (_o_) z
12/07/2019, 23:29
Skuola.net News è una testata giornalistica iscritta al Registro degli Operatori della Comunicazione.
Registrazione: n° 20792 del 23/12/2010.
©2000—
Skuola Network s.r.l. Tutti i diritti riservati. — P.I. 10404470014.
Powered by phpBB © phpBB Group - Privacy policy - Cookie privacy
phpBB Mobile / SEO by Artodia.