Lesson (II)
Table of contents
Isomorphisms
An isomorphism between two sets $A$ and $B$ is a pair of functions \[ f \maps A \to B \,\,\, \text{and} \,\,\,\, g \maps B \to A \] such that $g\circ f = \id_A$, and $f\circ g = \id_B$.
In such a situation, we call $f$ an inverse of $g$ and $g$ and inverse of $f$.
We can think of functions $f$ and $g$ above as no data-loss ``processes’’, e.g. conversion of files to different format without data being lost.
The sets $A$ and $B$ are said to be isomorphic in case there exists an isomorphism between them. In this case, we use the notation $A \iso B$. We say sets $A$ and $B$ are uniquely isomorphic if there is a unique pair of mutually inverse functions $f$ and $g$ which witness this isomorphism.
For exmaple, any two singletons are uniquely isomorphic. If we have sets $\set{🥕}$ and $\set{⛄}$ then they are isomorphic since we can find functions $f\maps \set{🥕} \to \set{⛄}$ defined by $f(🥕) = ⛄$ and $g(⛄) = 🥕$. This pair of function is an isomorphism since $f(g(⛄)) = f(🥕) = ⛄$ and $g(f(🥕)) = g(⛄) = 🥕$. Moreover, $f$ and $g$ are uniquely determined.
Isomorphisms are revetible processes and they let us to go back and forth between two different sets without loss of information. In fact, there is a sense in which somorphisms, rather than equality of sets is the correct notion of sameness of sets: For instance in the example of $\set{⛄}$ and $\set{🥕}$ both sets Since all the singletons are isomorphic
Challenge
We also have a function $\set{🥕} \to \set{🥕,⛄}$ which assigns 🥕 to 🥕. Does this function have an inverse? Why not?
Theorem (Inverses are Unique)
An inverse of a function, if it exists, is unique.
Let us give a less trivial exmaple of isomorphism of sets: Previously, we defined the cartesian product $A \times B$ of two sets $A$ and $B$ to consists of all the pairs $(a,b)$ where $a \in A$ and $b \in B$. Now, we show that the order of forming products does not matter, the sets $A\times B$ and $B \times A$ are isomorphic. To show this, we need to construct a pair of inverse functions \[ f\maps A \times B \to B \times A \quad \text{ and } \quad g\maps B\times A \to A\times B \, .\] We define $f$ by the assignemnt $(a,b) \maps (b,a)$ and $g$ by the assignemnt $(b,a) \maps (a,b)$. Now, \[ f \circ g (b,a) = f(a,b) = (b,a) \quad \text{ and } \quad g \circ f (a,b) = g(b,a) = (a,b) \, , \] for all $a \in A$ and $b \in B$. Therefore, by function extensionality, we have $ g\circ f = \id_{A \times B}$, and $f\circ g = \id_{B\times A}$. We conclude that \[ A \times B \iso B \times A \, .\]
Challenge
- Show that for all sets $A$, we have $A \times 1 \iso A$.
- Show that for all sets $A,B,C$ we have $A \times (B \times C) \iso (A\times B) \times C$.
- Show that for all sets $A,B,C$ we have $(A \times B) \times C \iso C \times (B\times A)$.
Challenge (Commutativity and Associativity of Disjoint Unions)
- Show that for all sets $A,B$ we have \[ A + B \iso B + A \, \]
- Show that for all sets $A,B,C$ we have \[ A + (B + C) \iso (A + B) + C \, .\]
Challenge
Is it true for all sets that $1 + A \iso A$? If not, find a condition about $A$ which forces $1 + A \iso A$ to be true.
Weaker Notions
The inverse functions we introduced above are sometimes called two-sided inverses; the reason behind it is clear, it does not matter in which order we compose the functions $f$ and $g$, whether $f$ appears to the right of $g$ or to the left of it, the result is identity. There are however weaker notions of inverse which are quite useful. Here are the two most important ones:
- A retract (aka left inverse) of a function $f \maps A \to B$ is a morphism $r \maps B \to A$ such that $r \circ f = \id_A$. In this case we also say $A$ is a retract of $B$.
- A section (aka right inverse) of function $f \maps A \to B$ is a morphism $s \maps B \to A$ such that $f \circ s = \id_B$.
Challenge (Canonical Function From Sum to Union)
There is a canonical function $A + B \to A \cup B$ which takes $(a,0)$ to $a$ and $(b,1)$ to $b$.
- Is this function an isomorphism?
- Does this function have a section?
Bijections
A function $f \maps A \to B$ is injective (also called one-to-one) whenever the following sentence holds. \[ \forall a,b \in A,\, f(a) = f(b) \Rightarrow a=b \] An injective function is said to be an injection.
Theorem (Sections are injective.)
Every function with a retract is injective.
Proof
Suppose $f \maps A \to B$ is function with a retract $r \maps B \to A$. Therefore, $r \circ f = \id_A$. Suppose $f(a) = f(\pr{a})$. It follows that \[ a = \id_A (a) = r \circ f (a) = r (f(a)) = r(f(\pr{a})) = r \circ f (\pr{a}) = \id_A (\pr{a}) = \pr{a} \, .\]
Challenge
Is the converse of the above theorem also true?
Theorem
Let $f \maps A \to B$ be a function. If $f$ is injective and $X$ is inhabited, then $f$ has a retract.
The dual concept to injection is surjection. A function $f \maps X \to Y$ is surjective (aka onto) whenever \[ \forall y \in Y,\ \exists x \in X,\ f(x) = y \] holds. A surjective function is said to be a surjection.
Challenge (Surjectivity and Inhabitedness)
Show that the function $\cons{X} \maps X \to 1$ is surjective if and only if $X$ is inhabited.
Theorem (Retractions are surjective.)
Every function with a section is surjective.
Challenge
Prove that the canonical function $A + B \to A \cup B$ is a surjection.
A function which is both injective and surjective is said to be bijective. An injective function is said to be an bijection.
Theorem
Every isomorphism of sets is a bijection.
Proof
Suppose $f \maps A \to B$ is an isomorphism. Then $f$ has an inverse $g \maps B \to A$. The function $g$ serves both as a section and as a retraction for $f$. Therefore, by theorems above $f$ is both injective and surjective, and hence it is bijective.
Challenge
Does the converse of the last theorem hold as well? If yes, give a proof, and if no, supply a counter-example.
Challenge
Show that if $A$ and $B$ are disjoint sets (i.e. their intersection $A \cap B$ is empty) then the canonical function $A + B \to A \cup B$ is in fact an isomorphism.
Set of Functions
Given two sets $A$ and $B$ we denote the set of functions from $A$ to $B$ by $B^A$. Thus, $f \in B^A$ if and only if $f \maps A \to B$ is a function. Similar to the terminology for numbers, the set $B^A$ is sometimes called “$B$ to the power of $A$” (or the “exponentiation of $A$ to $B$”).
By the definition of functions as functional relations, \[ B^A = \set{R \subseteq A \times B \mid R \text{ is a functional relation} }\] Therefore, $B^A \subseteq \powerset{A \times B}$.
We can reformulate some of the operation on functions, such as composition and evaluations,in terms of functions on the sets of functions.
Theorem (Composition as Function)
The composition operation is a function $\circ \maps B^A \times C^B \to C^A$. If $(f,g) \in B^A \times C^B$ then $f \maps A \to B$ and $g \maps B \to C$ are functions and therefore their composition $g \circ f$ is a function from $A$ to $C$ and hence $g \circ f \in C^A$. What remains to prove is to show that the assignment $(f,g) \mapsto g \circ f$ is well-defined (i.e. it is a total and deterministic assignment). Suppose $(f,g) = (f’,g’)$. We want to show that $g \circ f = g’ \circ f’$. We use function extensionality to prove that. Take an arbitrary $a \in A$. Since $(f,g) = (f’,g’)$, we have $f=f’$ and $g=g’$. We have $g \circ f (a) = g(f(a)) = g(f’(a)) = g’(f’(a)) = g’ \circ f’ (a)$. The first equality in the this chain of equalities holds by the definition of $g \circ f$, the second by our assumption that $f=f’$, the third by by our assumption that $g=g’$, and finally the last equality by the definition of $g’ \circ f’$. Since $a$ was arbitrary, by function extensionality, we conclude that $g \circ f = g’ \circ f’$.
Challenge (Evaluation as Function)
For a function $f \maps A \to B$ and an element $a \in A$, we can evaluate $f$ at $a$ simply by applying $f$ at $a$. Therefore, the result of evaluation of $f$ at $a$ (aka application of $f$ at $a$) is the element $f(a)$ in $B$. Find a function which evaluates a function at an element of its domain.
Theorem (Properties of Function Sets)
Suppose $X, Y, Z$ are sets. We have
- $ X^\emptyset \iso 1 $.
- $\emptyset^X \iso 1 $ if and only if $X = \emptyset$. In particular $\emptyset^\emptyset \iso 1$.
- $X^{Y + Z} \iso X^Y \times X^Z $.
Revisiting Functions of Many Arguments
In section Functions of Many Arguments we observed that a function of many arguments can be obtained by iteration of application of a function of a single argument. Now, we make this observation into a function. As we saw, a function $f \maps X \times Y \to Z$ can be alternatively thought of as $F \maps X \to Z^Y$ (where $F(x)$ is a function from $Y$ to $Z$ taking $y$ to $f(x,y)$). In other words, $f$ and $F$ are interchangeable.
Theorem (Frege-Schönfinkel-Curry)
- For all sets $X,Y,Z$ there is an isomorphism \[ X^{Y \times Z} \iso (X^Y)^Z \ \, \]
Proof
We construct a pair of functions $\mathsf{curry} \maps Z^{X \times Y} \to (Z^Y)^X$ and $\mathsf{uncurry} \maps (Z^Y)^X \to Z^{X \times Y}$ and prove they are inverses of each other. We define them by \[ \mathsf{curry} \, f \defeq \lambda x \, . \lambda y. \, f(x,y) \] and \[ \mathsf{uncurry} \, g \defeq \lambda a \, . (g \pi_1(a)) \pi_2(a) \]
Remark (Currying)
Recall that in the lesson on natural deductions we saw a form of currying for propositions; in Lean it was
theorem curry
(P Q R : Prop) : (P ∧ Q → R) → (P → (Q → R) :=
begin
intro h,
intro hp,
intro hq,
have hpq : P ∧ Q, from and.intro hp hq,
exact h hpq,
end
theorem uncurry
(P Q R : Prop) :
(P → (Q → R)) → (P ∧ Q → R) :=
begin
intro h,
intro hpq,
have h₁, from h hpq.left,
exact h₁ hpq.right,
end
The elegant relationship between logic and set theory gets even more elegant when we discover in section that the currying for propositions and the currying for sets are basically the same thing!
Theorem 5.1 Consider the core theory given by the axioms of extensionality, separation, emptyset, and pair with intuitionistic logic. The axiom of foundation in the form of a minimal ∈-element: ∀x [∃u ∈ x ⇒ ∃y (y ∈ x ∧ ∀z (z ∈ y ⇒ z ∈ x))], implies the law of excluded middle. Moreover, if separation is limited to bounded formulae, excluded middle for bounded formulae can be derived.
Propositions as Sets
Let us denote by $\pf{P}$ the set of proofs a proposition $P$. In set-builder notation \[ \pf{P} = \set{p \mid p \text{ is a proof of } P } \]
For a moment let’s travel back in time and have a recall of propositional connectives here. How soon things escalated!
Recall that
- a proof of a conjunction $P\land Q$ is pair consisting of a proof of $P$ and a proof of $Q$. Therefore, we have \[ \pf{P \land Q } = \pf{P} \times \pf{Q} ]]
- a proof of implication $P \To Q$ gives for every proof of $P$ a proof of $Q$. Therefore $\pf{P \To Q} \subseteq (\pf{P} \to \pf{Q})$ where $\pf{P} \to \pf{Q}$ is the set of functions from $\pf{P}$ to $\pf{Q}$. Also, if we have a function $\pf{P} \to \pf{Q}$ then we have a specification which specifies a proof of $P$ to a proof of $Q$. But, this specification is a proof of $P \To Q$. Altogeher, we have \[ \pf{P \To Q} = (\pf{P} \to \pf{Q}) \]
- a proof of a negation $\neg P$ is
Choice
Choice