Homotopy Type Theory category of partial functions in a set > history (Rev #3)

Contents

Idea

The essentially algebraic structure of partial functions on a set SS, and specific cases for when SS is an abelian group, commutative ring, and field respectively.

Definition

In a set

Given a set SS, the category of partial functions in SS is the concrete category Part(S)Part(S) with objects called subsets A:Ob(Part(S))A:Ob(Part(S)) with the set of elements for each subset El(A)El(A), and the set of morphisms consist of functions Hom(A,(S))(AS)Hom(A, \Im(S)) \coloneqq (A \to S) for each subset A:Ob(Part(S))A:Ob(Part(S)), where (S)\Im(S) is the improper subset, as well as the set of monomorphisms Hom(A,B)Hom(A, B) consisting of the subset inclusions for subsets A:Ob(Part(S))A:Ob(Part(S)) and B:Ob(Part(S))B:Ob(Part(S)).

There exist a global operator representing composition of partial functions

() Part(S)(): A:Ob(Part(S)) B:Ob(Part(S))Hom(A,(S))×Hom(B,(S))Hom(AB,(S))(-)\circ_{Part(S)}(-): \sum_{A:Ob(Part(S))} \sum_{B:Ob(Part(S))} Hom(A, \Im(S)) \times Hom(B, \Im(S)) \to Hom(A \cap B, \Im(S))

where

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)), g:Hom(B,(S))g:Hom(B, \Im(S)), and h:Hom(C,(S))h:Hom(C, \Im(S)), given the canonical isomorphism i a:Hom(A(BC),(AB)C)i_a:Hom(A \cap (B \cap C), (A \cap B) \cap C), i a(f Part(S)(g Part(S)h))=((f Part(S)g) Part(S)h)i_a \circ (f \circ_{Part(S)} (g \circ_{Part(S)} h)) = ((f \circ_{Part(S)} g) \circ_{Part(S)} h)

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)) and subset BAB \subseteq A, there is a function g:Hom(B,(S))g:Hom(B, \Im(S)) such that g=f Part(S)i B,Ag = f \circ_{Part(S)} i_{B,A} for canonical injection i B,A:Hom(B,A)i_{B,A}:Hom(B,A),

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)) and superset BAB \supseteq A, there is a function h:Hom(B,(S))h:Hom(B, \Im(S)) such that h Part(S)i A,B=fh \circ_{Part(S)} i_{A,B} = f for canonical injection i A,B:Hom(A,B)i_{A,B}:Hom(A,B),

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)), f=f Part(S)id Sf = f \circ_{Part(S)} id_S and f=id S Part(S)ff = id_S \circ_{Part(S)} f for the identity function id S:Hom((S),(S))id_S:Hom(\Im(S), \Im(S))

In an abelian group

If SS is a abelian group, then for every subset A:Ob(Part(S))A:Ob(Part(S)), Hom(A,(S))Hom(A, \Im(S)) is a abelian group, and in addition to the global operators corresponding to composition of partial functions, there exist global operators representing addition of partial functions and negation of partial functions,

()+(): A:Ob(Part(S)) B:Ob(Part(S))Hom(A,(S))×Hom(B,(S))Hom(AB,(S))(-)+(-): \sum_{A:Ob(Part(S))} \sum_{B:Ob(Part(S))} Hom(A, \Im(S)) \times Hom(B, \Im(S)) \to Hom(A \cap B, \Im(S))
(): A:Ob(Part(S))Hom(A,(S))Hom(A,(S)))-(-): \sum_{A:Ob(Part(S))} Hom(A, \Im(S)) \to Hom(A, \Im(S)))

where

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)) and g:Hom(B,(S))g:Hom(B, \Im(S)) there is a partial function f+g:Hom(AB,(S))f + g:Hom(A \cap B, \Im(S)) and a partial function g+f:Hom(BA,(S))g + f:Hom(B \cap A, \Im(S)) such that given the canonical isomorphism i c:Hom(AB,BA)i_c:Hom(A \cap B, B \cap A), i c(f+g)=(g+f)i_c \circ (f + g) = (g + f)

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)), g:Hom(B,(S))g:Hom(B, \Im(S)), and h:Hom(C,(S))h:Hom(C, \Im(S)), given the canonical isomorphism i a:Hom(A(BC),(AB)C)i_a:Hom(A \cap (B \cap C), (A \cap B) \cap C), i a(f+(g+h))=((f+g)+h)i_a \circ (f + (g + h)) = ((f + g) + h)

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)), and supersets BAB \supseteq A for B:Ob(Part(S))B:Ob(Part(S)), given the local additive unit 0 B,S:Hom(B,(S)0_{B,\Im{S}}:Hom(B, \Im(S), f+0 B,S=ff + 0_{B,\Im{S}} = f and 0 B,S+f=f0_{B,\Im{S}} + f = f

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)), there is a partial function f:Hom(A,(S))-f:Hom(A, \Im(S)) representing negation where the negation of FF is the local additive inverse of ff: f= A,Sf-f = -_{A,S}f

In a commutative ring

If SS is a commutative ring, then for every subset A:Ob(Part(S))A:Ob(Part(S)), Hom(A,(Part(S)))Hom(A, \Im(Part(S))) is a SS-commutative algebra, and in addition to the global operators corresponding to composition, addition, and negation of partial functions, there exist a global operator representing multiplication of partial functions

()(): A:Ob(Part(S)) B:Ob(Part(S))Hom(A,(S))×Hom(B,(S))Hom(AB,(S))(-)\cdot(-): \sum_{A:Ob(Part(S))} \sum_{B:Ob(Part(S))} Hom(A, \Im(S)) \times Hom(B, \Im(S)) \to Hom(A \cap B, \Im(S))

where

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)) and g:Hom(B,(S))g:Hom(B, \Im(S)) there is a partial function fg:Hom(AB,(S))f \cdot g:Hom(A \cap B, \Im(S)) and a partial function gf:Hom(BA,(S))g \cdot f:Hom(B \cap A, \Im(S)) such that given the canonical isomorphism i c:Hom(AB,BA)i_c:Hom(A \cap B, B \cap A), i c(fg)=(gf)i_c \circ (f \cdot g) = (g \cdot f)

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)), g:Hom(B,(S))g:Hom(B, \Im(S)), and h:Hom(C,(S))h:Hom(C, \Im(S)), given the canonical isomorphism i a:Hom(A(BC),(AB)C)i_a:Hom(A \cap (B \cap C), (A \cap B) \cap C), i a(f(gh))=((fg)h)i_a \circ (f \cdot (g \cdot h)) = ((f \cdot g) \cdot h)

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)), and supersets BAB \supseteq A for B:Ob(Part(S))B:Ob(Part(S)), given the local multiplicative unit 1 B,S:Hom(B,(S)1_{B,\Im{S}}:Hom(B, \Im(S), f1 B,S=ff \cdot 1_{B,\Im{S}} = f and 1 B,Sf=f1_{B,\Im{S}} \cdot f = f

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)), and supersets BAB \supseteq A for B:Ob(Part(S))B:Ob(Part(S)), given the local additive unit 0 B,S:Hom(B,(S)0_{B,\Im{S}}:Hom(B, \Im(S), f0 B,S=0 A,Sf \cdot 0_{B,\Im{S}} = 0_{A,\Im{S}} and 0 B,Sf=0 A,S0_{B,\Im{S}} \cdot f = 0_{A,\Im{S}}

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)), g:Hom(B,(S))g:Hom(B, \Im(S)), and h:Hom(C,(S))h:Hom(C, \Im(S)), given the canonical isomorphism i l:Hom(A(BC),(AB)(AC)i_l:Hom(A \cap (B \cap C), (A \cap B) \cap (A \cap C), i a(f(g+h))=(fg)+(fh)i_a \circ (f \cdot (g + h)) = (f \cdot g) + (f \cdot h)

  • for partial functions f:Hom(A,(S))f:Hom(A, \Im(S)), g:Hom(B,(S))g:Hom(B, \Im(S)), and h:Hom(C,(S))h:Hom(C, \Im(S)), given the canonical isomorphism i r:Hom((AB)C,(AC)(BC)i_r:Hom((A \cap B) \cap C, (A \cap C) \cap (B \cap C), i a((f+g)h))=(fh)+(gh)i_a \circ ((f + g) \cdot h)) = (f \cdot h) + (g \cdot h)

In a field

If SS is a Heyting field, then for every subset A:Ob(Part(S))A:Ob(Part(S)), Hom(A,(Part(S)))Hom(A, \Im(Part(S))) is a SS-commutative algebra, with global operators corresponding to composition, addition, negation, and multiplication of partial functions. Let

Hom #0(A,im(S)) f:Hom(A,(S)) x:El(A)(f(x)#0)Hom_{\#0}(A, \im(S)) \coloneqq \sum_{f:Hom(A, \Im(S))} \prod_{x:El(A)} (f(x) # 0)

be the type of all functions whose evaluations at each element are apart from zero on the entire domain. There exists a global operator representing the reciprocal of partial functions:

1(): A:Ob(Part(S))Hom(A,(S))Hom #0(A,(S))\frac{1}{(-)}: \sum_{A:Ob(Part(S))} Hom(A, \Im(S)) \to Hom_{\#0}(A, \Im(S))

where

  • for partial function f:Hom(A,(S))f:Hom(A, \Im(S)),
    1f11f1f=1f\frac{1}{f} \cdot \frac{1}{\frac{1}{f}} \cdot \frac{1}{f} = \frac{1}{f}

See also

References

Revision on April 23, 2022 at 14:52:25 by Anonymous?. See the history of this page for a list of all contributions to it.