Frexlet.Monoid.Commutative.Free

An inductive construction of the free commutative monoid over a
finite set.

Reexports

import public Frexlet.Monoid.Commutative.NatSemiLinear
import public Frexlet.Monoid.Commutative.Nat
import public Decidable.Equality
import public Data.Vect.Extra

Definitions

Model : Nat -> CommutativeMonoid

Totality: total
Visibility: public export

unit : (n : Nat) -> Fin n -> U (Model n)

  Monadic unit

Totality: total
Visibility: public export

FreeCommutativeMonoidOver : (n : Nat) -> ModelOver CommutativeMonoidTheory (cast (Fin n))

Totality: total
Visibility: public export

FreeModelZeroRepresentation : (n : Nat) -> (Model n) .sem Neutral = replicate n 0

Totality: total
Visibility: export

pointwiseSum : (n : Nat) -> (xss : Vect m (U (Model n))) -> (i : Fin n) -> index i ((Model n) .sum xss) = Additive .sum (map (index i) xss)

Totality: total
Visibility: export

pointwiseMult : (n : Nat) -> (m : Nat) -> (xs : U (Model n)) -> (i : Fin n) -> index i (m *. xs) = m * index i xs

Totality: total
Visibility: export

diracPointMass : (i : Fin n) -> (j : Fin n) -> Either (i = j, index j (unit n i) = 1) (index j (unit n i) = 0)

Totality: total
Visibility: export

normalForm : (n : Nat) -> (xs : U (Model n)) -> (Model n) .sum (tabulate (\i => index i xs *. unit n i)) = xs

Totality: total
Visibility: export

FreeExtenderFunction : ExtenderFunction

Totality: total
Visibility: public export

FreeExtenderSetoidHomomorphism : ExtenderSetoidHomomorphism

Totality: total
Visibility: public export

extenderPreservesZero : (other : ModelOver CommutativeMonoidTheory (cast (Fin n))) -> Preserves ((Model n) .Algebra) ((other .Model) .Algebra) (FreeExtenderFunction other) Zero

Totality: total
Visibility: public export

extenderPreservesPlus : (other : ModelOver CommutativeMonoidTheory (cast (Fin n))) -> Preserves ((Model n) .Algebra) ((other .Model) .Algebra) (FreeExtenderFunction other) Plus

Totality: total
Visibility: public export

FreeExtenderHomomorphism : ExtenderAlgebraHomomorphism

Totality: total
Visibility: public export

extenderIsMorphism : (other : ModelOver CommutativeMonoidTheory (cast (Fin n))) -> PreservesEnv (FreeCommutativeMonoidOver n) other (FreeExtenderSetoidHomomorphism other)

Totality: total
Visibility: public export

Extender : Extender

Totality: total
Visibility: public export

uniqueExtender : (other : ModelOver CommutativeMonoidTheory (cast (Fin n))) -> (extend : FreeCommutativeMonoidOver n ~> other) -> (xs : U (Model n)) -> (other .Model) .rel (((extend .H) .H) .H xs) (FreeExtenderFunction other xs)

Totality: total
Visibility: public export

Uniqueness : Uniqueness

Totality: total
Visibility: public export

Free : Free CommutativeMonoidTheory (cast (Fin n))

Totality: total
Visibility: public export