FC01 Appendix I — Cartesian Products and Zorn’s Lemma
FC01 — Dummit & Foote, Abstract Algebra.
This chapter contains 6 definitions, 4 theorems, 1 proposition, 1 convention and 1 other statements.
Nobody has checked this chapter against Lean yet, so the statements below say nothing about whether they are formalized.
convention: An indexing set is a set whose elements index a family ({AiiI}).
An indexing set is a set whose elements index a family ({A_iiI}).
definition: For a family ({Ai}{iI}), a choice function is (f:IAi) with…
For a family ({A_i}_{iI}), a choice function is (f:I_i A_i) with (f(i)A_i) for every (i).
definition: The Cartesian product (Ai) is the set of all choice functions
The Cartesian product (_{iI}A_i) is the set of all choice functions; it is empty if (I) or any component is empty.
definition: For (jI), (Aj) is the (j)-th component, (aj) the (j)-th coordinate, and…
For (jI), (A_j) is the (j)-th component, (a_j) the (j)-th coordinate, and the (j)-th projection sends ((a_i)_ia_j).
comparison
For (I={1,,n}), choice functions are canonically bijective with ordered (n)-tuples; for (I=Z^+), they are infinite sequences.
proposition
For nonempty countable \(I\), \(\lvert\prod_{i\in I}A_i\rvert=\prod_{i\in I}\lvert A_i\rvert\); in particular finite Cartesian-product cardinalities multiply.
definition: A partial order on nonempty (A) is a reflexive, antisymmetric, transitive…
A partial order on nonempty (A) is a reflexive, antisymmetric, transitive relation; (A) with such a relation is a partially ordered set.
definition: In a poset
In a poset: a chain is a pairwise comparable subset; an upper bound of (BA) is (u) with (bu) for all (bB); a maximal element (m) satisfies (mxm=x).
theorem: Zorn’s Lemma: if a nonempty poset has an upper bound for every chain, then…
Zorn’s Lemma: if a nonempty poset has an upper bound for every chain, then it has a maximal element.
theorem: Axiom of Choice: the Cartesian product of any nonempty family of nonempty…
Axiom of Choice: the Cartesian product of any nonempty family of nonempty sets is nonempty, equivalently a choice function exists.
definition: A well ordering is a total order in which every nonempty subset has a minimum.
A well ordering is a total order in which every nonempty subset has a minimum.
theorem: Well Ordering Principle: every nonempty set admits a well ordering.
Well Ordering Principle: every nonempty set admits a well ordering.
theorem: Under Zermelo–Fraenkel set theory, Zorn’s Lemma, the Axiom of Choice, and…
Under Zermelo–Fraenkel set theory, Zorn’s Lemma, the Axiom of Choice, and the Well Ordering Principle are equivalent.