Frexlet.Monoid.Commutative.NatSemiLinear.Sum

Properties to do with sums

Definitions

sumHomomorphism : (a : CommutativeMonoid) -> SetoidHomomorphism (VectSetoid n (cast a)) (cast a) (a .sum)

Totality: total
Visibility: public export

.sum : (a : CommutativeMonoid) -> VectSetoid n (cast a) ~> cast a

Totality: total
Visibility: public export

sumTabulateExtensional : (a : CommutativeMonoid) -> (f : (Fin n -> U a)) -> (g : (Fin n -> U a)) -> ((cast (Fin n) ~~> cast a) .equivalence) .relation (mate f) (mate g) -> a .rel (a .sum (tabulate f)) (a .sum (tabulate g))

Totality: total
Visibility: public export

sumZeroZero : (a : CommutativeMonoid) -> (n : Nat) -> ((cast a) .equivalence) .relation (a .sum (replicate n O1)) O1

Totality: total
Visibility: public export

sumDegenerate : (a : CommutativeMonoid) -> (xs : Vect n (U a)) -> (i : Fin n) -> ((j : Fin n) -> Either (i = j) (((cast a) .equivalence) .relation (index j xs) O1)) -> ((cast a) .equivalence) .relation (a .sum xs) (index i xs)

Totality: total
Visibility: public export

interchange : (a : CommutativeMonoid) -> (x : U a) -> (y : U a) -> (z : U a) -> (w : U a) -> a .rel ((x .+. y) .+. (z .+. w)) ((x .+. z) .+. (y .+. w))

Totality: total
Visibility: public export

sumCommutative : (a : CommutativeMonoid) -> (f : (Fin n -> U a)) -> (g : (Fin n -> U a)) -> a .rel (a .sum (tabulate (\i => f i .+. g i))) (a .sum (tabulate f) .+. a .sum (tabulate g))

Totality: total
Visibility: public export

sumPreservation : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (h : a ~> b) -> (xs : Vect n (U a)) -> b .rel ((h .H) .H (a .sum xs)) (b .sum (map ((h .H) .H) xs))

  NB: a,b are explicit since we can't recover them from the
  homomorphism between them as algebras alone.

Totality: total
Visibility: public export