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

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Idea

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

Definition

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 only consist of functions Hom(A,(S))(AS)Hom(A, \Im(S)) \coloneqq (A \to S), where (S)\Im(S) is the improper subset, as well as injections Hom(A,B)Hom(A, B) representing the subset inclusions.

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))) A:Ob(Part(S)) B:Ob(Part(S))Hom(A,(S))×Hom(B,(S)) C:Ob(Part(S))Hom( C AB,(S)) (-)\circ_{Part(S)}(-): \left(\sum_{A:Ob(Part(S))} \sum_{A:Ob(Part(S))} \sum_{B:Ob(Part(S))} Hom(A, \Im(S)) \times Hom(B, \Im(S))\right) \Im(S)) \to \sum_{C:Ob(Part(S))} Hom(A Hom(C, \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))

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,

In an abelian group

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

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))Hom(A,(S)))( A:Ob(Part(S))Hom(A,(S)))-(-): \left(\sum_{A:Ob(Part(S))} Hom(A, \Im(S)) \right) \to \sum(\sum_{A:Ob(Part(S))} Hom(A, \Im(S)))
()+(): 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

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.

In a commutative ring

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

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))Hom(A,(S)))×( A:Ob(Part(S))Hom(A,(S)))-(-): \left(\sum_{A:Ob(Part(S))} Hom(A, \Im(S)) \right) \times \mathbb{N} \to \sum(\sum_{A:Ob(Part(S))} Hom(A, \Im(S)))
()(): 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))
  • 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(A(BC),(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)

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)),
    11f1f=1f\frac{1}{\frac{1}{f}} \cdot \frac{1}{f} = \frac{1}{f}

    and

    1f11f=1f\frac{1}{f} \cdot \frac{1}{\frac{1}{f}} = \frac{1}{f}

See also

References

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