Definition of direct systems, inverse systems, and cardinalities in specific inverse systems #

In this file we compute the cardinality of each node in an inverse system F i indexed by a well-order in which every map between successive nodes has constant fiber X i, and every limit node is the limit of the inverse subsystem formed by all previous nodes. (To avoid importing Cardinal, we in fact construct a bijection rather than stating the result in terms of Cardinal.mk.)

The most tricky part of the whole argument happens at limit nodes: if i : ι is a limit, what we have in hand is a family of bijections F j ≃ ∀ l : Iio j, X l for every j < i, which we would like to "glue" up to a bijection F i ≃ ∀ l : Iio i, X l. We denote ∀ l : Iio i, X l by PiLT X i, and they form an inverse system just like the F i. Observe that at a limit node i, PiLT X i is actually the inverse limit of PiLT X j over all j < i (piLTLim). If the family of bijections F j ≃ PiLT X j is natural (IsNatEquiv), we immediately obtain a bijection between the limits limit F i ≃ PiLT X i (invLimEquiv), and we just need an additional bijection F i ≃ limit F i to obtain the desired extension F i ≃ PiLT X i to the limit node i. (We do have such a bijection, for example, when we consider a directed system of algebraic structures (say fields) K i, and F is the inverse system of homomorphisms K i ⟶ K into a specific field K.)

Now our task reduces to the recursive construction of a natural family of bijections for each i. We can prove that a natural family over all l ≤ i (Iic i) extends to a natural family over Iic i⁺ (where i⁺ = succ i), but at a limit node, recursion stops working: we have natural families over all Iic j for each j < i, but we need to know that they glue together to form a natural family over all l < i (Iio i). This intricacy did not occur to the author when he thought he had a proof and set out to formalize it. Fortunately he was able to figure out an additional compat condition (compatibility with the bijections F i⁺ ≃ F i × X i in the X component) that guarantees uniqueness (unique_pEquivOn) and hence gluability (well-definedness): see pEquivOnGlue. Instead of just a family of natural families, we actually construct a family of the stronger PEquivOns that bundles the compat condition, in order for the inductive argument to work.

It is possible to circumvent the introduction of the compat condition using Zorn's lemma; if there is a chain of natural families (i.e. for any two families in the chain, one is an extension of the other) over lowersets (which are all of the form Iic, Iio, or univ), we can clearly take the union to get a natural family that extends them all. If a maximal natural family has domain Iic i or Iio i (i a limit), we already know how to extend it one step further to Iic i⁺ or Iic i respectively, so it must be the case that the domain is everything. However, the author chose the compat approach in the end because it constructs the distinguished bijection that is compatible with the projections to all X i.