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 PEquivOn
s 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
.
A inverse system indexed by a preorder is a contravariant functor from the preorder
to another category. It is dual to DirectedSystem
.
- map_self : ∀ ⦃i : ι⦄ (x : F i), f ⋯ x = x
Instances
The inverse limit of an inverse system of types.
Equations
Instances For
For a family of types X
indexed by an preorder ι
and an element i : ι
,
piLT X i
is the product of all the types indexed by elements below i
.
Equations
- InverseSystem.piLT X i = ((l : ↑(Set.Iio i)) → X ↑l)
Instances For
The projection from a Pi type to the Pi type over an initial segment of its indexing type.
Equations
- InverseSystem.piLTProj h f l = f ⟨↑l, ⋯⟩
Instances For
The predicate that says a family of equivalences between F j
and piLT X j
is a natural transformation.
Equations
- InverseSystem.IsNatEquiv f equiv = ∀ ⦃j k : ι⦄ (hj : j ∈ s) (hk : k ∈ s) (h : k ≤ j) (x : F j), (equiv ⟨k, hk⟩) (f h x) = InverseSystem.piLTProj h ((equiv ⟨j, hj⟩) x)
Instances For
If i
is a limit in a well-ordered type indexing a family of types,
then piLT X i
is the limit of all piLT X j
for j < i
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Splitting off the X i
factor from the Pi type over {j | j ≤ i}
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extend a family of bijections to piLT
by one step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A natural family of bijections below a limit ordinal induces a bijection at the limit ordinal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extend a natural family of bijections to a limit ordinal.
Equations
- InverseSystem.piEquivLim nat equivLim hi = InverseSystem.piSplitLE (equiv, equivLim.trans ((InverseSystem.invLimEquiv nat).trans (InverseSystem.piLTLim hi).symm))
Instances For
A natural partial family of bijections to piLT
satisfying a compatibility condition.
- equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i
A partial family of bijections between
F
andpiLT X
defined on some set inι
. - nat : InverseSystem.IsNatEquiv f self.equiv
It is a natural family of bijections.
- compat : ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩), (self.equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
It is compatible with a family of bijections relating
F i⁺
toF i
.
Instances For
Restrict a partial family of bijections to a smaller set.
Equations
- e.restrict h = { equiv := fun (i : ↑s) => e.equiv ⟨↑i, ⋯⟩, nat := ⋯, compat := ⋯ }
Instances For
Extend a partial family of bijections by one step.
Equations
- InverseSystem.pEquivOnSucc hi e H = { equiv := InverseSystem.piEquivSucc e.equiv (equivSucc hi) hi, nat := ⋯, compat := ⋯ }
Instances For
Glue partial families of bijections at a limit ordinal, obtaining a partial family over a right-open interval.
Equations
- InverseSystem.pEquivOnGlue hi e = { equiv := (InverseSystem.piLTLim hi).symm ⟨fun (j : ↑(Set.Iio i)) => ((e j).restrict ⋯).equiv, ⋯⟩, nat := ⋯, compat := ⋯ }
Instances For
Extend pEquivOnGlue
by one step, obtaining a partial family over a right-closed interval.
Equations
- InverseSystem.pEquivOnLim hi e equivLim H = { equiv := InverseSystem.piEquivLim ⋯ equivLim hi, nat := ⋯, compat := ⋯ }
Instances For
Over a well-ordered type, construct a family of bijections by transfinite recursion.
Equations
- InverseSystem.globalEquiv equivSucc equivLim i = (InverseSystem.globalEquivAux✝ equivSucc equivLim i).equiv ⟨i, ⋯⟩