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

Idea

The essentially algebraic structure of partial functions on a set SS, and specific cases for when SS is an abelian group and commutative ring 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.

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))) C:Ob(Part(S))Hom(C,(S))(-)\circ_{Part(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))

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,

()+():( 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))
():( 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)))

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.

()():( 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))
():( 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)))
  • 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)

See also

References

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