Finite Character for Sets of Mappings

This article needs to be linked to other articles. In particular: Links to Finite Character to be reviewed following a refactor of those definitions. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

This page has been identified as a candidate for refactoring of medium complexity. In particular: This should be crafted as an equivalence proof between two different definitions of Definition:Finite Character, where those definitions should be crafted in e.g. the style of /Definition 1, /Definition 2, etc. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Theorem

Let $S$ and $T$ be sets.

Let $\FF$ be a set of mappings from subsets of $S$ to $T$.

That is, let $\FF$ be a set of partial mappings from $S$ to $T$.

Then the following are equivalent:

\((1)\)	$:$							$\FF$ has finite character in the sense of Definition:Finite Character/Mappings.
\((2)\)	$:$							$\FF$ has finite character as a set of subsets of $S \times T$ in the sense of Definition:Finite Character.

Proof

$(1)$ implies $(2)$

Let $\FF$ have finite character in the sense of Definition:Finite Character/Mappings.

That is, suppose that for each partial mapping $f \subseteq S \times T$:

$f \in \FF$ if and only if for each finite subset $K$ of the domain of $f$, the restriction of $f$ to $K$ is in $\FF$.

Let $q \subseteq S \times T$.

First suppose that $q \in \FF$.

Let $r$ be a finite subset of $q$.

Then $r$ is a partial mapping from its domain into $T$.

Since $r$ is finite, its domain, $\Dom r$, is a finite subset of the domain of $q$.

Since $\FF$ is of finite character as a set of mappings, $q \restriction \Dom r$ is in $\FF$.

But $q \restriction \Dom r = r$.

Therefore $r \in \FF$.

This article, or a section of it, needs explaining. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code.

Suppose instead that for each finite subset $r$ of $q$, $r \in \FF$.

Then for each finite subset $r$ of $q$, $r$ is a partial mapping from $S$ to $T$.

Let $x \in \Dom q$.

Let $y_1, y_2 \in T$.

Suppose that $\tuple {x, y_1}, \tuple {x, y_2} \in q$.

Then $\set {\tuple {x, y_1}, \tuple {x, y_2} }$ is a finite subset of $q$.

Therefore it must be a partial mapping.

Thus $y_1 = y_2$.

As this holds for all such $x, y_1, y_2$, $q$ is a partial mapping.

Let $K$ be a finite subset of $\Dom q$.

Then the restriction of $q$ to $K$ is a finite subset of $q$.

Thus $q \restriction K \in \FF$.

As this holds for all finite subsets $K$ of $\Dom q$, $q \in \FF$.

So we see that $\FF$ has finite character in the sense of Definition:Finite Character.

$\Box$

$(2)$ implies $(1)$

Let $\FF$ have finite character in the sense of Definition:Finite Character.

This needs considerable tedious hard slog to complete it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Finish}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.