7 Super-Algebras

Definition 7.1 (Super-Signature)

A super-signature (𝕊, 𝔽, rt) consists of

• a set of sorts 𝕊 and

• an 𝕊-sorted family 𝔽 = (𝔽_{s})_{s∈𝕊∗} of sets 𝔽_{s} of function symbols with argument sort s, and

• a result-type function rt: ∐_{s∈𝕊∗} 𝔽_{s} → � IN_{+}(𝕊).

Example 7.2 (Super-Signature)

Set 𝕊 := {1, zero, posnat, emptylist, nonemptylist}.

Note that 1 is included in 𝕊 in order to model the range of “undefined” function applications.

Set 𝔽_{∅} := {0, nil}; 𝔽_{zero} := {s}; 𝔽_{posnat} := {s, p};

𝔽_{emptylist} := {length}; 𝔽_{nonemptylist} := {length, car, cdr}; 𝔽_{zero zero} := 𝔽_{zero posnat} := 𝔽_{posnat posnat} := {+, –}; 𝔽_{posnat zero} :=

𝔽_{emptylist emptylist} := 𝔽_{emptylist nonemptylist} := 𝔽_{nonemptylist emptylist} := 𝔽_{nonemptylist nonemptylist} := {+}; 𝔽_{zero emptylist} := 𝔽_{zero nonemptylist} := 𝔽_{posnat emptylist} := 𝔽_{posnat nonemptylist} := {cons}; and 𝔽_{s} := ∅ for any other s ∈ 𝕊∗.

Set rt(∅, 0) := rt(emptylist, length) := rt(zero zero, +) := rt(zero zero, –) := {zero}; rt(zero, s) := rt(posnat, s) := rt(nonemptylist, length) := rt(zero posnat, +) :=

rt(posnat zero, +) := rt(posnat posnat, +) := rt(posnat zero, –) := {posnat};

rt(posnat, p) := rt(nonemptylist, car) := {zero, posnat}; rt(posnat posnat, –) := {zero, posnat, 1}; rt(∅, nil) := rt(emptylist emptylist, +) := {emptylist}; rt(emptylist nonemptylist, +) := rt(nonemptylist emptylist, +) :=

rt(nonemptylist nonemptylist, +) := rt(zero emptylist, cons) := rt(zero nonemptylist, cons) := rt(posnat emptylist, cons) :=

rt(posnat nonemptylist, cons) := {nonemptylist}; and

rt(nonemptylist, cdr) := {emptylist, nonemptylist}.

Definition 7.3 ((𝕊, 𝔽, rt)-Super-Algebra)

Let (𝕊, 𝔽, rt) be a super-signature.

A (𝕊, 𝔽, rt)-super-algebra consists of

• a family A = (A_{s})_{s∈𝕊} of non-empty sets (“universes”) and,

• for each (s, f) ∈ ∐_{s∈𝕊} 𝔽_{s}, a function

(s, f)^{A}: ∏_{i≺ |s|} A_{s_{i}} → ∐_{s′∈rt(s,f)} A_{s′}.

Example 7.4

Let (𝕊, 𝔽, rt) be the super-signature of Ex. 7.2.

Set A_{1} := {ω}; A_{zero} := {0}; A_{posnat} := IN_{+}; A_{emptylist} := {∅}; A_{nonemptylist} := IN^{+}.

For x, y ∈ IN and k, l ∈ IN∗ define:

(∅, 0)^{A}(ω) := (posnat, p)^{A}(1) := (emptylist, length)^{A}(∅) := (zero zero, +)^{A}(0, 0) :=

(zero zero, –)^{A}(0, 0) := (posnat posnat, –)^{A}(x, x) := (nonemptylist, car)^{A}(0l) := (zero, 0); (∅, nil)^{A}(ω) := (emptylist emptylist, +)^{A}(∅, ∅) := (nonemptylist, cdr)^{A}(x) := (emptylist, ∅); (zero, s)^{A}(x) := (posnat, s)^{A}(x) := (posnat, x+1); (nonemptylist, length)^{A}(l) := (posnat, |l|); (zero posnat, +)^{A}(x, y) := (posnat zero, +)^{A}(x, y) := (posnat posnat, +)^{A}(x, y) :=

(posnat, x+y);

(posnat, p)^{A}(x+1) := (posnat zero, –)^{A}(x, 0) := (nonemptylist, car)^{A}(xl) :=

(posnat, x) for x ∈ IN_{+};

(posnat posnat, –)^{A}(x, y) := (posnat, x−y) for x ≻ y; (posnat posnat, –)^{A}(x, y) := (1, ω) for x ≺ y; (emptylist nonemptylist, +)^{A}(k, l) := (nonemptylist emptylist, +)^{A}(k, l) :=

(nonemptylist nonemptylist, +)^{A}(k, l) := (nonemptylist, kl);

(s, cons)^{A}(x, l) := (nonemptylist, xl); and (nonemptylist, cdr)^{A}(xl) := (nonemptylist, l) for l ∈ IN^{+}.

Note that the super -signature of Ex. 7.2 is rather fine because the problems with the signature of Ex. 5.2 and the problems with the co-signature of Ex. 6.2 are both overcome. On the one hand, s(p(s(s(0)))) is a term because p(s(s(0))) has the sort posnat. On the other hand, we can now add three natural numbers: The super-signature does know that the result of the first addition can be paired with a natural number in order to add it.

While the notion of a super-algebra given in Def. 7.3 is nice, it is not very well suited for category theory. The first step for coming to the categorical definition of a super-algebra is to encode (𝕊, 𝔽, rt) into the following two functors (Γ_{Obj}, Γ_{Mor}, SORT(𝕊), SORT(𝕊∗)) and (Δ_{Obj}, Δ_{Mor}, SORT(𝕊), SORT(𝕊∗)) from the category SORT(𝕊) of 𝕊-sorted sets into the category SORT(𝕊∗) of 𝕊∗-sorted sets:

(AΓ)_{s} := ∏_{i≺ |s|} A_{s_{i}}

(AΔ)_{s} := ∏_{f∈𝔽_{s}}  ∐_{s′∈rt(s,f)} A_{s′}
(_{h}Γ)_{s}( (a_{i})_{i≺ |s|} ) := (h_{s_{i}}(a_{i}))_{i≺ |s|}
(_{h}Δ)_{s}( (s′_{f}, a′_{f})_{f∈𝔽_{s}} ) := (s′_{f}, h_{s′_{f}} (a′_{f}))_{f∈𝔽_{s}}

for A ∈_{SORT(𝕊)}Obj; h::A→B in SORT(𝕊); s ∈ 𝕊∗, ∀i ≺ |s|: a_{i} ∈ A_{s_{i}}; and ∀f ∈ 𝔽_{s}: (s′_{f} ∈ rt(s, f) ∧ a′_{f} ∈ A_{s′_{f}}).

Now we can categorically represent the above super-algebra over (𝔽, 𝕊, rt) using the morphism α::AΓ→AΔ in SORT(𝕊∗) given by α_{s}(a)_{f} := (s, f)^{A}(a) for a ∈ A_{s} and f ∈ 𝔽_{s}.

While the definition of a Σ-algebra is standard and the definition of a Γ-co-algebra is its dual, the definition of a (Γ, Δ)-super-algebra below is our invention.

Definition 7.5 ((Γ, Δ)-Super-Algebras and (Γ, Δ)-Super-Homomorphisms) Let Γ, Δ: SORT(𝕊) ↠ SORT(𝕊∗). A (Γ, Δ)-super-algebra is a pair (A, α) with A ∈_{SORT(𝕊)}Obj; ∀s ∈ 𝕊: A_{s} ≠ ∅; and α::AΓ→AΔ in SORT(𝕊∗). Let (A, α) and (B, β) be (Γ, Δ)-super-algebras. A (Γ, Δ)-super-homomorphism from (A, α) to (B, β) is a morphism h::A→B in SORT(𝕊) such that h is compatible with (Γ, Δ) in the sense that α _{SORT(𝕊∗)}⋄ _{h}Δ = _{h}Γ _{SORT(𝕊∗)}⋄ β.

AΓ \overline{_{_{_{h}Γ} >}} BΓ

=

AΔ^{∨^{α}}  \overline{_{_{_{h}Δ} >}} BΔ^{∨^{β}}

Note that for (Γ, Δ) defined from (𝕊, 𝔽, rt) as above, the latter condition means that for s ∈ 𝕊; f ∈ 𝔽_{s}; ∀i ≺ |s|: a_{i} ∈ A_{s_{i}}; and

for (s′, a′) := α_{s}( (a_{i})_{i≺ |s|} )_{f}: ( s′, h_{s′}(a′) ) = β_{s}( (h_{s_{i}}(a)_{i})_{i≺ |s|} )_{f},

i.e.

for (s′, a′) := (s, f)^{A}( (a_{i})_{i≺ |s|} ): ( s′, h_{s′}(a′) ) = (s, f)^{B}( (h_{s_{i}}(a_{i}))_{i≺ |s|} ).

Definition 7.6 (SUALG)

The (Γ, Δ)-super-homomorphism category SUALG of (Γ, Δ)-super-algebras is given as follows:

SUALGObj is the class of all (Γ, Δ)-super-algebras.

SUALGMor_{(A,α),(B,β)} is the class of all (Γ, Δ)-super-homomorphisms h::A→B.

h _{SUALG}⋄ k := h _{SORT(𝕊)}⋄ k for h ∈ _{SUALG}Mor_{(A,α),(B,β)} and h ∈ _{SUALG}Mor_{(B,β),(C,γ)}.

SUALGId_{(A,α)} := _{SORT(𝕊)}Id_{A}.

Note that, while the morphisms of SUALG are also morphisms of SORT(𝕊) and their composition is the same, SUALG is no sub-category of SORT(𝕊) because the objects of SUALG are no objects of SORT(𝕊).